65 lines
2.5 KiB
Text
65 lines
2.5 KiB
Text
/-
|
||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Joseph Tooby-Smith
|
||
-/
|
||
import HepLean.StandardModel.Basic
|
||
import HepLean.Meta.Informal
|
||
/-!
|
||
|
||
# The Pati-Salam Model
|
||
|
||
The Pati-Salam model is a grand unified theory that unifies the Standard Model gauge group into
|
||
`SU(4) x SU(2) x SU(2)`.
|
||
|
||
This file current contains informal-results about the Pati-Salam group.
|
||
|
||
-/
|
||
|
||
namespace PatiSalam
|
||
/-!
|
||
|
||
## The Pati-Salam gauge group.
|
||
|
||
-/
|
||
|
||
informal_definition GaugeGroupI where
|
||
math :≈ "The group `SU(4) x SU(2) x SU(2)`."
|
||
physics :≈ "The gauge group of the Pati-Salam model (unquotiented by ℤ₂)."
|
||
|
||
informal_definition embedSM where
|
||
physics :≈ "The embedding of the Standard Model gauge group into the Pati-Salam gauge group."
|
||
math :≈ "The group homomorphism `SU(3) x SU(2) x U(1) -> SU(4) x SU(2) x SU(2)`
|
||
taking (h, g, α) to (blockdiag (α h, α ^ (-3)), g, diag(α ^ (3), α ^(-3)))."
|
||
ref :≈ "Page 54 of https://math.ucr.edu/home/baez/guts.pdf"
|
||
deps :≈ [``GaugeGroupI, ``StandardModel.GaugeGroupI]
|
||
|
||
informal_definition gaugeGroupISpinEquiv where
|
||
math :≈ "The equivalence between `GaugeGroupI` and `Spin(6) × Spin(4)`."
|
||
deps :≈ [``GaugeGroupI]
|
||
|
||
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 the non-trivial element (-1, -1, -1)."
|
||
ref :≈ "https://math.ucr.edu/home/baez/guts.pdf"
|
||
deps :≈ [``GaugeGroupI]
|
||
|
||
informal_definition GaugeGroupℤ₂ where
|
||
physics :≈ "The gauge group of the Pati-Salam 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, ``gaugeGroupℤ₂SubGroup]
|
||
|
||
informal_lemma sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup where
|
||
math :≈ "The group ``StandardModel.gaugeGroupℤ₆SubGroup under the homomorphism ``embedSM factors
|
||
through the subgroup ``gaugeGroupℤ₂SubGroup."
|
||
deps :≈ [``embedSM, ``StandardModel.gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup]
|
||
|
||
informal_definition embedSMℤ₆Toℤ₂ where
|
||
math :≈ "The group homomorphism from ``StandardModel.GaugeGroupℤ₆ to ``GaugeGroupℤ₂
|
||
induced by ``embedSM."
|
||
deps :≈ [``embedSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupℤ₂,
|
||
``sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup]
|
||
|
||
end PatiSalam
|