feat: Effective potential for Weyl fermions (Stacked on #1404)

Physlib.lean

@@ -121,13 +121,18 @@ public import Physlib.Mathematics.LinearPMap
 public import Physlib.Mathematics.List
 public import Physlib.Mathematics.List.InsertIdx
 public import Physlib.Mathematics.List.InsertionSort
+public import Physlib.Mathematics.MvPolynomialTranslation
+public import Physlib.Mathematics.MvPowerSeriesDerivative
 public import Physlib.Mathematics.OrthogonalMatrix
 public import Physlib.Mathematics.PiTensorProduct
+public import Physlib.Mathematics.PolynomialEval
 public import Physlib.Mathematics.RatComplexNum
 public import Physlib.Mathematics.Resolvent
 public import Physlib.Mathematics.SO3.Basic
 public import Physlib.Mathematics.SchurTriangulation
 public import Physlib.Mathematics.SpecialFunctions.PhysHermite
+public import Physlib.Mathematics.SymmetricAlgebra
+public import Physlib.Mathematics.TensorProduct
 public import Physlib.Mathematics.Trigonometry.Tanh
 public import Physlib.Mathematics.VariationalCalculus.Basic
 public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
@@ -181,7 +186,21 @@ public import Physlib.Particles.FlavorPhysics.CKMMatrix.Relations
 public import Physlib.Particles.FlavorPhysics.CKMMatrix.Rows
 public import Physlib.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
 public import Physlib.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
+public import Physlib.Particles.LeptonGaugeSector.JetAlgebra.Boosts.FieldStrength
+public import Physlib.Particles.LeptonGaugeSector.JetAlgebra.Covariantization
 public import Physlib.Particles.NeutrinoPhysics.Basic
+public import Physlib.Particles.QED.Basic
+public import Physlib.Particles.QED.CurrentCoupling
+public import Physlib.Particles.QED.Evaluation
+public import Physlib.Particles.QED.FermionStatistics
+public import Physlib.Particles.QED.FieldStrength
+public import Physlib.Particles.QED.Fields
+public import Physlib.Particles.QED.GammaMatrices
+public import Physlib.Particles.QED.GaugeInvariance
+public import Physlib.Particles.QED.JetCompleteness
+public import Physlib.Particles.QED.Lagrangian
+public import Physlib.Particles.QED.LorentzInvariance
+public import Physlib.Particles.QED.MassDimension
 public import Physlib.Particles.StandardModel.AnomalyCancellation.Basic
 public import Physlib.Particles.StandardModel.AnomalyCancellation.FamilyMaps
 public import Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.Basic
@@ -190,13 +209,53 @@ public import Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lin
 public import Physlib.Particles.StandardModel.AnomalyCancellation.Permutations
 public import Physlib.Particles.StandardModel.Basic
 public import Physlib.Particles.StandardModel.Fermions.DownSinglet
+public import Physlib.Particles.StandardModel.Fermions.JetAlgebra.Basic
 public import Physlib.Particles.StandardModel.Fermions.LeptonDoublet
-public import Physlib.Particles.StandardModel.Fermions.LeptonSinglet
+public import Physlib.Particles.StandardModel.Fermions.LeptonSinglet.Basic
+public import Physlib.Particles.StandardModel.Fermions.LeptonSinglet.JetAlgebra.Basic
+public import Physlib.Particles.StandardModel.Fermions.LeptonSinglet.JetAlgebra.GaugeAction
+public import Physlib.Particles.StandardModel.Fermions.LeptonSinglet.JetAlgebra.JetDeriv
+public import Physlib.Particles.StandardModel.Fermions.LeptonSinglet.JetAlgebra.LorentzAction
+public import Physlib.Particles.StandardModel.Fermions.LeptonSinglet.JetAlgebra.MassDim
+public import Physlib.Particles.StandardModel.Fermions.LeptonSinglet.JetComponentSpace
 public import Physlib.Particles.StandardModel.Fermions.QuarkDoublet
 public import Physlib.Particles.StandardModel.Fermions.UpSinglet
+public import Physlib.Particles.StandardModel.GaugeBosons.GaugeJetAlgebra.Basic
+public import Physlib.Particles.StandardModel.GaugeBosons.GaugeJetAlgebra.GaugeAction
+public import Physlib.Particles.StandardModel.GaugeBosons.GaugeJetAlgebra.Invariants
+public import Physlib.Particles.StandardModel.GaugeBosons.GaugeJetAlgebra.JetDeriv
+public import Physlib.Particles.StandardModel.GaugeBosons.GaugeJetAlgebra.LorentzAction
+public import Physlib.Particles.StandardModel.GaugeBosons.GaugeJetAlgebra.MassDim
+public import Physlib.Particles.StandardModel.GaugeBosons.Gluons.JetCompleteness
+public import Physlib.Particles.StandardModel.GaugeGroup.GaugeWeightDecomposition
+public import Physlib.Particles.StandardModel.GaugeGroup.HyperchargeDecomposition
+public import Physlib.Particles.StandardModel.GaugeGroup.IsospinDecomposition
+public import Physlib.Particles.StandardModel.GaugeGroup.SU2PermDecomposition
 public import Physlib.Particles.StandardModel.HiggsBoson.Basic
 public import Physlib.Particles.StandardModel.HiggsBoson.EffectivePotential
+public import Physlib.Particles.StandardModel.HiggsBoson.JetAlgebra.Basic
 public import Physlib.Particles.StandardModel.HiggsBoson.Potential
+public import Physlib.Particles.StandardModel.JetAlgebra.Basic
+public import Physlib.Particles.StandardModel.JetAlgebra.GaugeAction
+public import Physlib.Particles.StandardModel.JetAlgebra.Invariants
+public import Physlib.Particles.StandardModel.JetAlgebra.JetDeriv
+public import Physlib.Particles.StandardModel.JetAlgebra.LorentzAction
+public import Physlib.Particles.StandardModel.JetAlgebra.MassDim
+public import Physlib.Particles.StandardModel.Matter.BosonicAlgebra.Basic
+public import Physlib.Particles.StandardModel.Matter.BosonicAlgebra.GaugeAction
+public import Physlib.Particles.StandardModel.Matter.BosonicAlgebra.JetDeriv
+public import Physlib.Particles.StandardModel.Matter.BosonicAlgebra.LorentzAction
+public import Physlib.Particles.StandardModel.Matter.BosonicAlgebra.MassDim
+public import Physlib.Particles.StandardModel.Matter.BosonicAlgebra.Prod
+public import Physlib.Particles.StandardModel.Matter.FermionicAlgebra.Basic
+public import Physlib.Particles.StandardModel.Matter.FermionicAlgebra.GaugeAction
+public import Physlib.Particles.StandardModel.Matter.FermionicAlgebra.JetDeriv
+public import Physlib.Particles.StandardModel.Matter.FermionicAlgebra.LorentzAction
+public import Physlib.Particles.StandardModel.Matter.FermionicAlgebra.MassDim
+public import Physlib.Particles.StandardModel.Matter.FermionicAlgebra.Prod
+public import Physlib.Particles.StandardModel.Matter.JetComponentSpace.Basic
+public import Physlib.Particles.StandardModel.Matter.JetComponentSpace.CovariantDeriv
+public import Physlib.Particles.StandardModel.Matter.JetComponentSpace.InfinitesimalAction
 public import Physlib.Particles.StandardModel.Representations
 public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.B3
 public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Basic
@@ -363,8 +422,11 @@ public import Physlib.Relativity.LorentzAlgebra.Basis
 public import Physlib.Relativity.LorentzAlgebra.ExponentialMap
 public import Physlib.Relativity.LorentzGroup.Basic
 public import Physlib.Relativity.LorentzGroup.Boosts.Apply
+public import Physlib.Relativity.LorentzGroup.Boosts.Axis
+public import Physlib.Relativity.LorentzGroup.Boosts.WeightGrading
 public import Physlib.Relativity.LorentzGroup.Boosts.Basic
 public import Physlib.Relativity.LorentzGroup.Boosts.Generalized
+public import Physlib.Relativity.LorentzGroup.FermionicParity
 public import Physlib.Relativity.LorentzGroup.Orthochronous.Basic
 public import Physlib.Relativity.LorentzGroup.Proper
 public import Physlib.Relativity.LorentzGroup.Restricted.Basic

Physlib/Mathematics/ConjModule.lean

@@ -9,7 +9,8 @@ public import Mathlib.Algebra.Module.Equiv.Defs
 public import Mathlib.Algebra.Star.Module
 public import Mathlib.LinearAlgebra.Basis.Defs
 public import Mathlib.Tactic.Ring
-
+public import Mathlib.RepresentationTheory.Basic
+public import Mathlib.LinearAlgebra.TensorProduct.Basic
 /-!
 
 # The conjugate module
@@ -36,6 +37,7 @@ conjugate-linear identity `conjEquiv : M ≃ₛₗ[starRingEnd k] ConjModule M`,
 @[expose] public section
 
 open Module
+open scoped TensorProduct
 
 variable {k : Type*} [CommRing k] [StarRing k]
 variable {M : Type*} [AddCommGroup M] [Module k M]
@@ -53,6 +55,19 @@ conjugation ring endomorphism `starRingEnd k`. -/
 instance instModule : Module k (ConjModule M) :=
   Module.compHom M (starRingEnd k)
 
+variable {A : Type*} [Ring A]
+
+instance : Ring (ConjModule A) :=
+  let i1 : AddCommGroup (ConjModule A) := inferInstanceAs (AddCommGroup (ConjModule A))
+  let i2 : Ring A := inferInstanceAs (Ring A)
+  { i1, i2 with }
+
+/-- The conjugate module of a `k`-algebra is a `k`-algebra: the same ring, with scalars
+acting through `star`. -/
+instance instAlgebra [Algebra k A] : Algebra k (ConjModule A) :=
+  Algebra.ofModule (fun r x y => smul_mul_assoc (β := A) (star r) x y)
+    (fun r x y => mul_smul_comm (β := A) (star r) x y)
+
 end ConjModule
 
 /-- The canonical conjugate-linear equivalence `M ≃ₛₗ[starRingEnd k] ConjModule M`, the identity on
@@ -65,6 +80,26 @@ def conjEquiv : M ≃ₛₗ[starRingEnd k] ConjModule M where
   left_inv _ := rfl
   right_inv _ := rfl
 
+/-- The canonical conjugate-linear equivalence between the dual of a module `M` and
+  the dual of its conjugate. -/
+def conjDualEquiv : Module.Dual k M ≃ₛₗ[starRingEnd k] Module.Dual k (ConjModule M) where
+  toFun f := (starRingEnd k).toSemilinearMap.comp
+    (f.comp (conjEquiv (k := k) (M := M)).symm.toLinearMap)
+  invFun f := (starRingEnd k).toSemilinearMap.comp
+    (f.comp (conjEquiv (k := k) (M := M)).toLinearMap)
+  map_add' f g := by
+    ext x
+    simp
+  map_smul' r f := by
+    ext x
+    simp
+  left_inv f := by
+    ext x
+    simp
+  right_inv f := by
+    ext x
+    simp
+
 namespace ConjModule
 
 /-- Conjugating twice returns the original module: the `k`-linear isomorphism
@@ -89,23 +124,197 @@ noncomputable def starFinsupp : (ι →₀ k) ≃ₛₗ[starRingEnd k] (ι →
 
 /-- A basis of `M` transported to a basis of `ConjModule M`: the same basis vectors, with
 coordinates conjugated (`(Basis.conj b).repr v = star ∘ b.repr v`). -/
-noncomputable def _root_.Basis.conj (b : Basis ι k M) : Basis ι k (ConjModule M) :=
+noncomputable def _root_.Module.Basis.conj (b : Basis ι k M) : Basis ι k (ConjModule M) :=
   Basis.ofRepr
     (((conjEquiv (k := k) (M := M)).symm.trans b.repr).trans starFinsupp)
 
 /-- Coordinates in `Basis.conj b` are the `star` of the coordinates in `b`. -/
-@[simp] lemma _root_.Basis.conj_repr_apply (b : Basis ι k M) (v : ConjModule M) (i : ι) :
+@[simp] lemma _root_.Module.Basis.conj_repr_apply (b : Basis ι k M) (v : ConjModule M) (i : ι) :
     (Basis.conj b).repr v i = star (b.repr ((conjEquiv (k := k) (M := M)).symm v) i) := rfl
 
 /-- The basis vectors of `Basis.conj b` are those of `b`, viewed through `conjEquiv`. -/
-@[simp] lemma _root_.Basis.conj_apply (b : Basis ι k M) (i : ι) :
+@[simp] lemma _root_.Module.Basis.conj_apply (b : Basis ι k M) (i : ι) :
     Basis.conj b i = conjEquiv (k := k) (M := M) (b i) := by
   apply (Basis.conj b).repr.injective
   ext j
   rcases eq_or_ne j i with h | h
   · subst h; simp [Basis.conj_repr_apply]
   · simp [Basis.conj_repr_apply, Finsupp.single_eq_of_ne, h]
 
+/-!
+
+## The conjugate of a representation
+
+-/
+
+/-- The conjugate of a representation `ρ` of `G` on `M`: the same maps `ρ g`, acting on
+`ConjModule M` through `conjEquiv`. -/
+def _root_.Representation.conj {G} [Group G] (ρ : Representation k G M) :
+    Representation k G (ConjModule M) where
+  toFun g := {
+    toFun := conjEquiv (k := k) (M := M) ∘ ρ g ∘ (conjEquiv (k := k) (M := M)).symm
+    map_add' x y := (ρ g).map_add x y
+    map_smul' a m := (ρ g).map_smul (star a) m }
+  map_one' := LinearMap.ext fun _ =>
+    congrArg (conjEquiv (k := k)) (LinearMap.congr_fun (map_one ρ) _)
+  map_mul' g h := LinearMap.ext fun _ =>
+    congrArg (conjEquiv (k := k)) (LinearMap.congr_fun (map_mul ρ g h) _)
+
+lemma _root_.Representation.conj_apply {G} [Group G] (ρ : Representation k G M) (g : G)
+    (m : ConjModule M) :
+    ρ.conj g m = conjEquiv (k := k) (M := M) (ρ g ((conjEquiv (k := k) (M := M)).symm m)) := rfl
+
+/-!
+
+## Functoriality, and conjugation of tensor products
+
+Conjugation is monoidal: `ConjModule M ⊗ ConjModule N ≃ ConjModule (M ⊗ N)`, the identity
+on pure tensors. The map is honestly `k`-linear because the twist on each factor cancels
+against the twist on the target.
+
+Everything below routes through `conjEquiv` rather than relying on definitional unfolding
+of the `ConjModule` synonym. Writing `m ⊗ₜ n` for `m : ConjModule M` makes elaboration
+pick the *twisted* module instances, landing in the wrong tensor product; converting
+explicitly with `conjEquiv` fixes every instance by construction.
+
+-/
+
+variable {N : Type*} [AddCommGroup N] [Module k N]
+
+/-- Functoriality of conjugation: a `k`-linear map induces a `k`-linear map of the
+conjugate modules, given by the same underlying function. -/
+def map (f : M →ₗ[k] N) : ConjModule M →ₗ[k] ConjModule N where
+  toFun := f
+  map_add' := f.map_add
+  map_smul' c x := f.map_smul (star c) x
+
+@[simp]
+lemma map_apply (f : M →ₗ[k] N) (x : ConjModule M) : map f x = f x := rfl
+
+/-- **Conjugation commutes with finite products.** The conjugate of a product is the product
+of the conjugates, by the identity underlying function: the twisted scalar action is applied
+componentwise. -/
+def prodEquiv : ConjModule (M × N) ≃ₗ[k] ConjModule M × ConjModule N where
+  toFun x := (map (LinearMap.fst k M N) x, map (LinearMap.snd k M N) x)
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  invFun x := (x.1, x.2)
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+@[simp]
+lemma prodEquiv_apply (x : ConjModule (M × N)) :
+    prodEquiv (k := k) x = (map (LinearMap.fst k M N) x, map (LinearMap.snd k M N) x) := rfl
+
+/-- The conjugate module of a finite free module is finite: the conjugated basis
+`Module.Basis.conj` is indexed by the same type. -/
+instance instFinite [Module.Free k M] [Module.Finite k M] :
+    Module.Finite k (ConjModule M) :=
+  Module.Finite.of_basis (Module.Basis.conj (Module.Free.chooseBasis k M))
+
+/-- The canonical `k`-linear map `ConjModule M ⊗ ConjModule N → ConjModule (M ⊗ N)`,
+the identity on pure tensors. -/
+noncomputable def tensorHom : ConjModule M ⊗[k] ConjModule N →ₗ[k] ConjModule (M ⊗[k] N) :=
+  TensorProduct.lift
+    { toFun := fun m =>
+        { toFun := fun n => conjEquiv (k := k) (M := M ⊗[k] N)
+            ((conjEquiv (k := k) (M := M)).symm m ⊗ₜ[k] (conjEquiv (k := k) (M := N)).symm n)
+          map_add' := by
+            intro n₁ n₂
+            rw [map_add, TensorProduct.tmul_add, map_add]
+          map_smul' := by
+            intro c n
+            rw [map_smulₛₗ, TensorProduct.tmul_smul, map_smulₛₗ]
+            simp }
+      map_add' := by
+        intro m₁ m₂
+        ext n
+        simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
+        rw [map_add, TensorProduct.add_tmul, map_add]
+      map_smul' := by
+        intro c m
+        ext n
+        simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.smul_apply, RingHom.id_apply]
+        rw [map_smulₛₗ, ← TensorProduct.smul_tmul', map_smulₛₗ]
+        simp }
+
+@[simp]
+lemma tensorHom_tmul (m : ConjModule M) (n : ConjModule N) :
+    tensorHom (k := k) (m ⊗ₜ[k] n)
+      = conjEquiv (k := k) (M := M ⊗[k] N)
+        ((conjEquiv (k := k) (M := M)).symm m ⊗ₜ[k] (conjEquiv (k := k) (M := N)).symm n) :=
+  rfl
+
+/-- The inverse map `ConjModule (M ⊗ N) → ConjModule M ⊗ ConjModule N`, again the identity
+on pure tensors. A `k`-linear map out of `ConjModule X` is the same data as a `k`-linear
+map into `ConjModule` of the target, which is what `map` and `involution` package here. -/
+noncomputable def tensorInv : ConjModule (M ⊗[k] N) →ₗ[k] ConjModule M ⊗[k] ConjModule N :=
+  (involution (k := k) (M := ConjModule M ⊗[k] ConjModule N)).toLinearMap ∘ₗ
+    map (TensorProduct.lift
+      { toFun := fun m =>
+          { toFun := fun n => conjEquiv (k := k) (M := ConjModule M ⊗[k] ConjModule N)
+              (conjEquiv (k := k) (M := M) m ⊗ₜ[k] conjEquiv (k := k) (M := N) n)
+            map_add' := by
+              intro n₁ n₂
+              rw [map_add, TensorProduct.tmul_add, map_add]
+            map_smul' := by
+              intro c n
+              rw [map_smulₛₗ, TensorProduct.tmul_smul, map_smulₛₗ]
+              simp }
+        map_add' := by
+          intro m₁ m₂
+          ext n
+          simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
+          rw [map_add, TensorProduct.add_tmul, map_add]
+        map_smul' := by
+          intro c m
+          ext n
+          simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.smul_apply, RingHom.id_apply]
+          rw [map_smulₛₗ, ← TensorProduct.smul_tmul', map_smulₛₗ]
+          simp })
+
+/-- **Conjugation is monoidal.** `ConjModule M ⊗ ConjModule N ≃ₗ[k] ConjModule (M ⊗ N)`,
+the identity on pure tensors. Injectivity comes from `tensorInv` being a left inverse;
+surjectivity from every element of `M ⊗ N` being a sum of pure tensors. -/
+noncomputable def tensorEquiv :
+    ConjModule M ⊗[k] ConjModule N ≃ₗ[k] ConjModule (M ⊗[k] N) :=
+  LinearEquiv.ofBijective tensorHom
+    ⟨by
+      have h : ∀ w : ConjModule M ⊗[k] ConjModule N, tensorInv (tensorHom w) = w := by
+        intro w
+        induction w using TensorProduct.induction_on with
+        | zero => simp
+        | tmul m n => rfl
+        | add x y hx hy => rw [map_add, map_add, hx, hy]
+      exact Function.LeftInverse.injective h,
+     by
+      intro z
+      induction z using TensorProduct.induction_on with
+      | zero => exact ⟨0, map_zero _⟩
+      | tmul m n =>
+          exact ⟨conjEquiv (k := k) (M := M) m ⊗ₜ[k] conjEquiv (k := k) (M := N) n, rfl⟩
+      | add x y hx hy =>
+          obtain ⟨w₁, h₁⟩ := hx
+          obtain ⟨w₂, h₂⟩ := hy
+          refine ⟨w₁ + w₂, ?_⟩
+          rw [map_add, h₁, h₂]
+          rfl⟩
+
+@[simp]
+lemma tensorEquiv_tmul (m : ConjModule M) (n : ConjModule N) :
+    tensorEquiv (k := k) (m ⊗ₜ[k] n)
+      = conjEquiv (k := k) (M := M ⊗[k] N)
+        ((conjEquiv (k := k) (M := M)).symm m ⊗ₜ[k] (conjEquiv (k := k) (M := N)).symm n) :=
+  rfl
+
+@[simp]
+lemma tensorEquiv_symm_conjEquiv_tmul (m : M) (n : N) :
+    (tensorEquiv (k := k) (M := M) (N := N)).symm
+        (conjEquiv (k := k) (M := M ⊗[k] N) (m ⊗ₜ[k] n))
+      = conjEquiv (k := k) (M := M) m ⊗ₜ[k] conjEquiv (k := k) (M := N) n := by
+  rw [LinearEquiv.symm_apply_eq, tensorEquiv_tmul]
+  simp
+
 end ConjModule
 
 end