Merge pull request #167 from HEPLean/informal_defs

feat: Add Georgi Glashow

HepLean.lean

@@ -46,6 +46,7 @@ import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
 import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
+import HepLean.BeyondTheStandardModel.GeorgiGlashow.Basic
 import HepLean.BeyondTheStandardModel.PatiSalam.Basic
 import HepLean.BeyondTheStandardModel.Spin10.Basic
 import HepLean.BeyondTheStandardModel.TwoHDM.Basic

HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean

@@ -0,0 +1,44 @@
+/-
+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 Georgi-Glashow Model
+
+The Georgi-Glashow model is a grand unified theory that unifies the Standard Model gauge group into
+`SU(5)`.
+
+This file currently contains informal-results about the Georgi-Glashow group.
+
+-/
+
+namespace GeorgiGlashow
+
+informal_definition GaugeGroupI where
+  math :≈ "The group `SU(5)`."
+  physics :≈ "The gauge group of the Georgi-Glashow model."
+
+informal_definition inclSM where
+  physics :≈ "The homomorphism of the Standard Model gauge group into the
+    Georgi-Glashow gauge group."
+  math :≈ "The group homomorphism `SU(3) x SU(2) x U(1) -> SU(5)`
+    taking (h, g, α) to (blockdiag (α ^ 3 g, α ^ (-2) h)."
+  ref :≈ "Page 34 of https://math.ucr.edu/home/baez/guts.pdf"
+  deps :≈ [``GaugeGroupI, ``StandardModel.GaugeGroupI]
+
+informal_lemma inclSM_ker where
+  math :≈ "The kernel of the map ``inclSM is equal to the subgroup
+    ``StandardModel.gaugeGroupℤ₆SubGroup."
+  ref :≈ "Page 34 of https://math.ucr.edu/home/baez/guts.pdf"
+  deps :≈ [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup]
+
+informal_definition embedSMℤ₆ where
+  math :≈ "The group embedding from ``StandardModel.GaugeGroupℤ₆ to ``GaugeGroupI
+    induced by ``inclSM by quotienting by the kernal ``inclSM_ker."
+  deps :≈ [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupI, ``inclSM_ker]
+
+end GeorgiGlashow

HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean

@@ -12,7 +12,7 @@ import HepLean.Meta.Informal
 The Pati-Salam model is a petite 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.
+This file currently contains informal-results about the Pati-Salam group.
 
 -/
 

HepLean/BeyondTheStandardModel/Spin10/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.BeyondTheStandardModel.PatiSalam.Basic
+import HepLean.BeyondTheStandardModel.GeorgiGlashow.Basic
 import HepLean.Meta.Informal
 /-!
 
@@ -34,4 +35,19 @@ informal_definition inclSM where
   ref :≈ "Page 56 of https://math.ucr.edu/home/baez/guts.pdf"
   deps :≈ [``inclPatiSalam, ``PatiSalam.inclSM]
 
+informal_definition inclGeorgiGlashow where
+  physics :≈ "The inclusion of the Georgi-Glashow gauge group into Spin(10)."
+  math :≈ "The Lie group homomorphism from SU(n) → Spin(2n) dicussed on page 46 of
+    https://math.ucr.edu/home/baez/guts.pdf for n = 5."
+  deps :≈ [``GaugeGroupI, ``GeorgiGlashow.GaugeGroupI]
+
+informal_definition inclSMThruGeorgiGlashow where
+  physics :≈ "The inclusion of the Standard Model gauge group into Spin(10)."
+  math :≈ "The composition of ``inclGeorgiGlashow and ``GeorgiGlashow.inclSM."
+  deps :≈ [``inclGeorgiGlashow, ``GeorgiGlashow.inclSM]
+
+informal_lemma inclSM_eq_inclSMThruGeorgiGlashow where
+  math :≈ "The inclusion ``inclSM is equal to the inclusion ``inclSMThruGeorgiGlashow."
+  deps :≈ [``inclSM, ``inclSMThruGeorgiGlashow]
+
 end Spin10Model