DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #159 from HEPLean/informal_defs

Browse source 
feat: Informal defs for gauge group of the SM
This commit is contained in:
Joseph Tooby-Smith 2024-09-18 08:03:24 -04:00 • committed by GitHub
commit 523c9b334d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 86 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/SpaceTime/WeylFermion/Basic.lean
View file

@ -87,8 +87,8 @@ informal_lemma leftAltWeylFermionContraction_invariant where
deps :≈ [``leftAltWeylFermionContraction]
informal_definition altLeftWeylFermionContraction where
math :≈ "The linear map from altLeftHandedWeylFermion ⊗ leftHandedWeylFermion to ℂ given by
summing over components of altLeftHandedWeylFermion and leftHandedWeylFermion in the
math :≈ "The linear map from altLeftHandedWeylFermion ⊗ leftHandedWeylFermion to ℂ given by
summing over components of altLeftHandedWeylFermion and leftHandedWeylFermion in the
standard basis (i.e. the dot product)."
physics :≈ "The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
In index notation this is φ^a ψ_a ."

62
HepLean/StandardModel/Basic.lean
View file

@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
import Mathlib.Data.Complex.Exponential
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.LinearAlgebra.Matrix.ToLin
import HepLean.Meta.Informal
/-!
# The Standard Model
@ -21,8 +22,65 @@ open Matrix
open Complex
open ComplexConjugate
/-- The global gauge group of the standard model. -/
abbrev GaugeGroup : Type :=
/-- The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients. -/
abbrev GaugeGroupI : Type :=
specialUnitaryGroup (Fin 3) ℂ × specialUnitaryGroup (Fin 2) ℂ × unitary ℂ
informal_definition gaugeGroupℤ₆SubGroup where
physics :≈ "The subgroup of the un-quotiented gauge group which acts trivially on
all particles in the standard model. "
math :≈ "The ℤ₆-subgroup of ``GaugeGroupI with elements (α^2 * I₃, α^(-3) * I₂, α), where `α`
is a sixth complex root of unity."
ref :≈ "https://math.ucr.edu/home/baez/guts.pdf"
deps :≈ [``GaugeGroupI]
informal_definition GaugeGroupℤ₆ where
physics :≈ "The smallest possible gauge group of the Standard Model."
math :≈ "The quotient of ``GaugeGroupI by the ℤ₆-subgroup `gaugeGroupℤ₆SubGroup`."
ref :≈ "https://math.ucr.edu/home/baez/guts.pdf"
deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
informal_definition gaugeGroupℤ₂SubGroup where
physics :≈ "The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on
all particles in the standard model. "
math :≈ "The ℤ₂-subgroup of ``GaugeGroupI derived from the ℤ₂ subgroup of `gaugeGroupℤ₆SubGroup`."
ref :≈ "https://math.ucr.edu/home/baez/guts.pdf"
deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
informal_definition GaugeGroupℤ₂ where
physics :≈ "The guage group of the Standard Model with a ℤ₂ quotient."
math :≈ "The quotient of ``GaugeGroupI by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`."
ref :≈ "https://math.ucr.edu/home/baez/guts.pdf"
deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₂SubGroup]
informal_definition gaugeGroupℤ₃SubGroup where
physics :≈ "The ℤ₃-subgroup of the un-quotiented gauge group which acts trivially on
all particles in the standard model. "
math :≈ "The ℤ₃-subgroup of ``GaugeGroupI derived from the ℤ₃ subgroup of `gaugeGroupℤ₆SubGroup`."
ref :≈ "https://math.ucr.edu/home/baez/guts.pdf"
deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
informal_definition GaugeGroupℤ₃ where
physics :≈ "The guage group of the Standard Model with a ℤ₃-quotient."
math :≈ "The quotient of ``GaugeGroupI by the ℤ₃-subgroup `gaugeGroupℤ₃SubGroup`."
ref :≈ "https://math.ucr.edu/home/baez/guts.pdf"
deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₃SubGroup]
/-- Specifies the allowed quotients of `SU(3) x SU(2) x U(1)` which give a valid
gauge group of the Standard Model. -/
inductive GaugeGroupQuot : Type
| ℤ₆ : GaugeGroupQuot
| ℤ₂ : GaugeGroupQuot
| ℤ₃ : GaugeGroupQuot
| I : GaugeGroupQuot
informal_definition GaugeGroup where
physics :≈ "The (global) gauge group of the Standard Model given a choice of quotient."
math :≈ "The map from `GaugeGroupQuot` to `Type` which gives the gauge group of the Standard Model
for a given choice of quotient."
ref :≈ "https://math.ucr.edu/home/baez/guts.pdf"
deps :≈ [``GaugeGroupI, ``gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup, ``gaugeGroupℤ₃SubGroup,
``GaugeGroupQuot]
end StandardModel

27
HepLean/StandardModel/HiggsBoson/GaugeAction.lean
View file

@ -32,7 +32,7 @@ open ComplexConjugate
/-- The Higgs representation as a homomorphism from the gauge group to unitary `2×2`-matrices. -/
@[simps!]
noncomputable def higgsRepUnitary : GaugeGroup →* unitaryGroup (Fin 2) ℂ where
noncomputable def higgsRepUnitary : GaugeGroupI →* unitaryGroup (Fin 2) ℂ where
toFun g := repU1 g.2.2 * fundamentalSU2 g.2.1
map_mul' := by
intro ⟨_, a2, a3⟩ ⟨_, b2, b3⟩
@ -75,14 +75,14 @@ def unitToLinear : unitary (HiggsVec →L[ℂ] HiggsVec) →* HiggsVec →ₗ[
/-- The representation of the gauge group acting on `higgsVec`. -/
@[simps!]
def rep : Representation ℂ GaugeGroup HiggsVec :=
def rep : Representation ℂ GaugeGroupI HiggsVec :=
unitToLinear.comp (unitaryToLin.comp higgsRepUnitary)
lemma higgsRepUnitary_mul (g : GaugeGroup) (φ : HiggsVec) :
lemma higgsRepUnitary_mul (g : GaugeGroupI) (φ : HiggsVec) :
(higgsRepUnitary g).1 *ᵥ φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) := by
simp [higgsRepUnitary_apply_coe, smul_mulVec_assoc]
lemma rep_apply (g : GaugeGroup) (φ : HiggsVec) : rep g φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) :=
lemma rep_apply (g : GaugeGroupI) (φ : HiggsVec) : rep g φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) :=
higgsRepUnitary_mul g φ
/-!
@ -131,7 +131,7 @@ lemma rotateMatrix_specialUnitary {φ : HiggsVec} (hφ : φ ≠ 0) :
/-- Given a Higgs vector, an element of the gauge group which puts the first component of the
vector to zero, and the second component to a real number. -/
def rotateGuageGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroup :=
def rotateGuageGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroupI :=
⟨1, ⟨(rotateMatrix φ), rotateMatrix_specialUnitary hφ⟩, 1⟩
lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
@ -155,7 +155,7 @@ lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
theorem rotate_fst_zero_snd_real (φ : HiggsVec) :
∃ (g : GaugeGroup), rep g φ = ![0, Complex.ofReal ‖φ‖] := by
∃ (g : GaugeGroupI), rep g φ = ![0, Complex.ofReal ‖φ‖] := by
by_cases h : φ = 0
· use ⟨1, 1, 1⟩
simp only [Prod.mk_one_one, _root_.map_one, h, map_zero, Nat.succ_eq_add_one, Nat.reduceAdd,
@ -166,9 +166,9 @@ theorem rotate_fst_zero_snd_real (φ : HiggsVec) :
exact rotateGuageGroup_apply h
theorem rotate_fst_real_snd_zero (φ : HiggsVec) :
∃ (g : GaugeGroup), rep g φ = ![Complex.ofReal ‖φ‖, 0] := by
∃ (g : GaugeGroupI), rep g φ = ![Complex.ofReal ‖φ‖, 0] := by
obtain ⟨g, h⟩ := rotate_fst_zero_snd_real φ
let P : GaugeGroup := ⟨1, ⟨!![0, 1; -1, 0], by
let P : GaugeGroupI := ⟨1, ⟨!![0, 1; -1, 0], by
rw [mem_specialUnitaryGroup_iff]
apply And.intro
· rw [mem_unitaryGroup_iff, star_eq_conjTranspose]
@ -190,13 +190,20 @@ theorem rotate_fst_real_snd_zero (φ : HiggsVec) :
· simp only [Fin.mk_one, Fin.isValue, Pi.smul_apply, Function.comp_apply, cons_val_one, head_cons,
tail_cons, smul_zero]
informal_lemma stablity_group where
informal_lemma stability_group_single where
physics :≈ "The Higgs boson breaks electroweak symmetry down to the electromagnetic force."
math :≈ "The stablity group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`,
for non-zero `‖φ‖` is the `SU(3) x U(1)` subgroup of
`gaugeGroup := SU(3) x SU(2) x U(1)` with the embedding given by
`(g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ})`."
deps :≈ [`StandardModel.HiggsVec, `StandardModel.HiggsVec.rep]
deps :≈ [``StandardModel.HiggsVec, ``StandardModel.HiggsVec.rep]
informal_lemma stability_group where
math :≈ "The subgroup of `gaugeGroup := SU(3) x SU(2) x U(1)` which preserves every `HiggsVec`
by the action of ``StandardModel.HiggsVec.rep is given by `SU(3) x ℤ₆` where ℤ₆
is the subgroup of `SU(2) x U(1)` with elements `(α^(-3) * I₂, α)` where
α is a sixth root of unity."
deps :≈ [``StandardModel.HiggsVec, ``StandardModel.HiggsVec.rep]
end HiggsVec

13
scripts/MetaPrograms/informal.lean
View file

@ -261,17 +261,18 @@ unsafe def mkDot (imports : Array Import) : MetaM String := do
let informal_name := informal.map (fun c => c.2.name)
let formal_deps := deps.filter (fun d => d ∉ informal_name)
let formal_nodes ← formal_deps.mapM formalToNode
let header := "strict digraph G {
bgcolor=\"lightyellow\";
label=\"Informal dependency graph for HepLean\";
labelloc=\"t\";
labeljust=\"l\";"
let footer := "}"
let nodes := String.intercalate "\n" formal_nodes.toList
let informalLemmaNodes ← informal.mapM informalToNode
let informalNodes := String.intercalate "\n" informalLemmaNodes.toList
let edges ← informal.mapM informalToEdges
let edges := String.intercalate "\n" edges.toList
let header := "strict digraph G {
bgcolor=\"lightyellow\";
label=\"Informal dependency graph for HepLean\";
labelloc=\"t\";
labeljust=\"l\";
edge [arrowhead=vee];"
let footer := "}"
pure (header ++ "\n" ++ nodes ++ "\n" ++ informalNodes ++ "\n" ++ edges ++ "\n" ++ footer)
end dotFile