feat: Add unitary rep

HepLean/StandardModel/Basic.lean

@@ -8,6 +8,8 @@ import Mathlib.Geometry.Manifold.VectorBundle.Basic
 import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 import Mathlib.Geometry.Manifold.Instances.Real
 import Mathlib.RepresentationTheory.Basic
+import Mathlib.LinearAlgebra.Matrix.ToLin
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 /-!
 # The Standard Model
 
@@ -29,4 +31,55 @@ abbrev spaceTime := EuclideanSpace ℝ (Fin 4)
 abbrev guageGroup : Type := specialUnitaryGroup (Fin 3) ℂ ×
   specialUnitaryGroup (Fin 2) ℂ × unitary ℂ
 
+-- TODO: Move to MathLib.
+lemma star_specialUnitary (g : specialUnitaryGroup (Fin 2) ℂ) :
+    star g.1 ∈ specialUnitaryGroup (Fin 2) ℂ := by
+  have hg := mem_specialUnitaryGroup_iff.mp g.prop
+  rw [@mem_specialUnitaryGroup_iff]
+  apply And.intro
+  rw [@mem_unitaryGroup_iff, star_star]
+  exact mem_unitaryGroup_iff'.mp hg.1
+  rw [star_eq_conjTranspose, det_conjTranspose, hg.2, star_one]
+
+-- TOMOVE
+@[simps!]
+noncomputable def repU1Map (g : unitary ℂ) : unitaryGroup (Fin 2) ℂ :=
+  ⟨g ^ 3 • 1, by
+    rw [mem_unitaryGroup_iff, smul_one_mul, show g = ⟨g.1, g.prop⟩ from rfl]
+    simp only [SubmonoidClass.mk_pow, Submonoid.mk_smul, star_smul, star_pow, RCLike.star_def,
+      star_one]
+    rw [smul_smul, ← mul_pow]
+    erw [(unitary.mem_iff.mp g.prop).2]
+    simp only [one_pow, one_smul]⟩
+
+@[simps!]
+noncomputable def repU1 : unitary ℂ →* unitaryGroup (Fin 2) ℂ where
+  toFun g := repU1Map g
+  map_mul' g h := by
+    simp only [repU1Map, Submonoid.mk_mul_mk, mul_smul_one, smul_smul, mul_comm, ← mul_pow]
+  map_one' := by
+    simp only [repU1Map, one_pow, one_smul, Submonoid.mk_eq_one]
+
+@[simps!]
+def fundamentalSU2 : specialUnitaryGroup (Fin 2) ℂ →* unitaryGroup (Fin 2) ℂ where
+  toFun g := ⟨g.1, g.prop.1⟩
+  map_mul' _ _ := Subtype.ext rfl
+  map_one' := Subtype.ext rfl
+
+lemma repU1_fundamentalSU2_commute (u1 : unitary ℂ) (g : specialUnitaryGroup (Fin 2) ℂ) :
+    repU1 u1 * fundamentalSU2 g = fundamentalSU2 g * repU1 u1 := by
+  apply Subtype.ext
+  simp
+
+noncomputable def higgsRepUnitary : guageGroup →* unitaryGroup (Fin 2) ℂ where
+  toFun g := repU1 g.2.2 * fundamentalSU2 g.2.1
+  map_mul'  := by
+    intro ⟨_, a2, a3⟩ ⟨_, b2, b3⟩
+    change repU1 (a3 * b3) *  fundamentalSU2 (a2 * b2) = _
+    rw [repU1.map_mul, fundamentalSU2.map_mul]
+    rw [mul_assoc, mul_assoc, ← mul_assoc (repU1 b3) _ _, repU1_fundamentalSU2_commute]
+    repeat rw [mul_assoc]
+  map_one' := by
+    simp
+
 end StandardModel

HepLean/StandardModel/HiggsField.lean

@@ -55,6 +55,8 @@ instance : NormedAddCommGroup (Fin 2 → ℂ) := by
 
 section higgsVec
 
+
+
 /-- The continous linear map from the vector space `higgsVec` to `(Fin 2 → ℂ)` acheived by
 casting vectors. -/
 def higgsVecToFin2ℂ : higgsVec →L[ℝ] (Fin 2 → ℂ) where
@@ -102,6 +104,49 @@ noncomputable def higgsRep : Representation ℂ guageGroup higgsVec where
 
 namespace higgsVec
 
+/-- An orthonomral basis of higgsVec. -/
+noncomputable def orthonormBasis : OrthonormalBasis (Fin 2) ℂ higgsVec :=
+  EuclideanSpace.basisFun (Fin 2) ℂ
+
+/-- Takes in a `2×2`-matrix and returns a linear map of `higgsVec`. -/
+@[simps!]
+noncomputable def matrixToLin : Matrix (Fin 2) (Fin 2) ℂ →* (higgsVec →L[ℂ] higgsVec) where
+  toFun g := LinearMap.toContinuousLinearMap
+    $ Matrix.toLin orthonormBasis.toBasis orthonormBasis.toBasis g
+  map_mul' g h := ContinuousLinearMap.coe_inj.mp $
+    Matrix.toLin_mul orthonormBasis.toBasis orthonormBasis.toBasis orthonormBasis.toBasis g h
+  map_one' := ContinuousLinearMap.coe_inj.mp $ Matrix.toLin_one orthonormBasis.toBasis
+
+lemma matrixToLin_star (g : Matrix (Fin 2) (Fin 2) ℂ) :
+    matrixToLin (star g) = star (matrixToLin g) :=
+  ContinuousLinearMap.coe_inj.mp (Matrix.toLin_conjTranspose orthonormBasis orthonormBasis g)
+
+lemma matrixToLin_unitary (g : unitaryGroup (Fin 2) ℂ) :
+    matrixToLin g ∈ unitary (higgsVec →L[ℂ] higgsVec) := by
+  rw [@unitary.mem_iff, ← matrixToLin_star, ← matrixToLin.map_mul, ← matrixToLin.map_mul]
+  rw [mem_unitaryGroup_iff.mp g.prop, mem_unitaryGroup_iff'.mp g.prop, matrixToLin.map_one]
+  simp
+
+noncomputable def unitaryToLin : unitaryGroup (Fin 2) ℂ →* unitary (higgsVec →L[ℂ] higgsVec) where
+  toFun g := ⟨matrixToLin g, matrixToLin_unitary g⟩
+  map_mul' g h := by
+    ext
+    simp
+  map_one' := by
+    ext
+    simp
+
+@[simps!]
+def unitToLinear : unitary (higgsVec →L[ℂ] higgsVec) →* higgsVec →ₗ[ℂ] higgsVec :=
+  DistribMulAction.toModuleEnd ℂ higgsVec
+
+@[simps!]
+def rep : Representation ℂ guageGroup higgsVec :=
+   unitToLinear.comp (unitaryToLin.comp higgsRepUnitary)
+
+lemma norm_invariant (g : guageGroup) (φ : higgsVec) : ‖rep g φ‖ = ‖φ‖ :=
+  ContinuousLinearMap.norm_map_of_mem_unitary (unitaryToLin (higgsRepUnitary g)).2 φ
+
 /-- Given a vector `ℂ²` the constant higgs field with value equal to that
 section. -/
 noncomputable def toField (φ : higgsVec) : higgsField where
@@ -115,6 +160,11 @@ noncomputable def toField (φ : higgsVec) : higgsField where
 def potential (μSq lambda : ℝ) (φ : higgsVec) : ℝ := - μSq  * ‖φ‖ ^ 2  +
   lambda * ‖φ‖ ^ 4
 
+lemma potential_invariant (μSq lambda : ℝ) (φ : higgsVec)  (g : guageGroup) :
+    potential μSq lambda (rep g φ) = potential μSq lambda φ := by
+  simp only [potential, neg_mul]
+  rw [norm_invariant]
+
 lemma potential_snd_term_nonneg {lambda : ℝ} (hLam : 0 < lambda) (φ : higgsVec) :
     0 ≤ lambda * ‖φ‖ ^ 4 := by
   rw [mul_nonneg_iff]