diff --git a/HepLean/StandardModel/Basic.lean b/HepLean/StandardModel/Basic.lean index 83fe567..2bad1c5 100644 --- a/HepLean/StandardModel/Basic.lean +++ b/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 diff --git a/HepLean/StandardModel/HiggsField.lean b/HepLean/StandardModel/HiggsField.lean index f4bccf9..f069035 100644 --- a/HepLean/StandardModel/HiggsField.lean +++ b/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]