From 938087ca518389355a984ea67e59d9bce5059d58 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 18 Apr 2024 08:59:48 -0400
Subject: [PATCH] feat: Add results in the NoGrav and Ordinary cases

---
 HepLean.lean                                  |   3 +
 .../SMNu/NoGrav/Basic.lean                    | 115 ++++++++++++++++
 .../SMNu/Ordinary/Basic.lean                  | 125 ++++++++++++++++++
 .../SMNu/Ordinary/FamilyMaps.lean             |  57 ++++++++
 4 files changed, 300 insertions(+)
 create mode 100644 HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
 create mode 100644 HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
 create mode 100644 HepLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean

diff --git a/HepLean.lean b/HepLean.lean
index 6dd8813..fce406c 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -18,4 +18,7 @@ import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
 import HepLean.AnomalyCancellation.SM.Permutations
 import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.FamilyMaps
+import HepLean.AnomalyCancellation.SMNu.NoGrav.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
+import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
+import HepLean.AnomalyCancellation.SMNu.Ordinary.FamilyMaps
diff --git a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
new file mode 100644
index 0000000..859ad28
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.SMNu.Basic
+import HepLean.AnomalyCancellation.SMNu.Permutations
+/-!
+# ACC system for SM with RHN and no gravitational anomaly.
+
+We define the ACC system for the Standard Model with right-handed neutrinos and no gravitational
+anomaly.
+
+-/
+universe v u
+
+namespace SMRHN
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+/-- The ACC system for the SM plus RHN with no gravitational anomaly. -/
+@[simps!]
+def SMNoGrav (n : ℕ) : ACCSystem where
+  numberLinear := 2
+  linearACCs := fun i =>
+    match i with
+    | 0 => @accSU2 n
+    | 1 => accSU3
+  numberQuadratic := 0
+  quadraticACCs := by
+    intro i
+    exact Fin.elim0 i
+  cubicACC := accCube
+
+namespace SMNoGrav
+
+variable {n : ℕ}
+
+lemma SU2Sol  (S : (SMNoGrav n).LinSols) : accSU2 S.val = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 0
+
+lemma SU3Sol  (S : (SMNoGrav n).LinSols) : accSU3 S.val = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 1
+
+lemma cubeSol  (S : (SMNoGrav n).Sols) : accCube S.val = 0 := by
+  exact S.cubicSol
+
+/-- An element of `charges` which satisfies the linear ACCs
+  gives us a element of `LinSols`. -/
+def chargeToLinear (S : (SMNoGrav n).charges) (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) :
+    (SMNoGrav n).LinSols :=
+  ⟨S, by
+    intro i
+    simp at i
+    match i with
+    | 0 => exact hSU2
+    | 1 => exact hSU3⟩
+
+/-- An element of `LinSols` which satisfies the quadratic ACCs
+  gives us a element of `QuadSols`. -/
+def linearToQuad (S : (SMNoGrav n).LinSols) : (SMNoGrav n).QuadSols :=
+  ⟨S, by
+    intro i
+    exact Fin.elim0 i⟩
+
+/-- An element of `QuadSols` which satisfies the quadratic ACCs
+  gives us a element of `LinSols`. -/
+def quadToAF (S : (SMNoGrav n).QuadSols) (hc : accCube S.val = 0) :
+    (SMNoGrav n).Sols := ⟨S, hc⟩
+
+/-- An element of `charges` which satisfies the linear and quadratic ACCs
+  gives us a element of `QuadSols`. -/
+def chargeToQuad (S : (SMNoGrav n).charges) (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) :
+    (SMNoGrav n).QuadSols :=
+  linearToQuad $ chargeToLinear S hSU2 hSU3
+
+/-- An element of `charges` which satisfies the linear, quadratic and cubic ACCs
+  gives us a element of `Sols`. -/
+def chargeToAF (S : (SMNoGrav n).charges) (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0)
+    (hc : accCube S = 0) : (SMNoGrav n).Sols :=
+  quadToAF (chargeToQuad S hSU2 hSU3) hc
+
+/-- An element of `LinSols` which satisfies the  quadratic and cubic ACCs
+  gives us a element of `Sols`. -/
+def linearToAF (S : (SMNoGrav n).LinSols)
+    (hc : accCube S.val = 0) : (SMNoGrav n).Sols :=
+  quadToAF (linearToQuad S) hc
+
+/-- The permutations acting on the ACC system corresponding to the SM with RHN,
+and no gravitational anomaly. -/
+def perm (n : ℕ) : ACCSystemGroupAction (SMNoGrav n) where
+  group := permGroup n
+  groupInst := inferInstance
+  rep := repCharges
+  linearInvariant := by
+    intro i
+    simp at i
+    match i with
+    | 0 => exact accSU2_invariant
+    | 1 => exact accSU3_invariant
+  quadInvariant := by
+    intro i
+    simp at i
+    exact Fin.elim0 i
+  cubicInvariant := accCube_invariant
+
+
+end SMNoGrav
+
+end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
new file mode 100644
index 0000000..d69248d
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.SMNu.Basic
+import HepLean.AnomalyCancellation.SMNu.Permutations
+/-!
+# ACC system for SM with RHN (without hypercharge).
+
+We define the ACC system for the Standard Model with right-handed neutrinos and no gravitational
+anomaly.
+
+-/
+
+universe v u
+
+namespace SMRHN
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+/-- The ACC system for the SM plus RHN. -/
+@[simps!]
+def SM (n : ℕ) : ACCSystem where
+  numberLinear := 3
+  linearACCs := fun i =>
+    match i with
+    | 0 => @accGrav n
+    | 1 => accSU2
+    | 2 => accSU3
+  numberQuadratic := 0
+  quadraticACCs := by
+    intro i
+    exact Fin.elim0 i
+  cubicACC := accCube
+
+namespace SM
+
+
+variable {n : ℕ}
+
+lemma gravSol  (S : (SM n).LinSols) : accGrav S.val = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 0
+
+lemma SU2Sol  (S : (SM n).LinSols) : accSU2 S.val = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 1
+
+lemma SU3Sol  (S : (SM n).LinSols) : accSU3 S.val = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 2
+
+lemma cubeSol  (S : (SM n).Sols) : accCube S.val = 0 := by
+  exact S.cubicSol
+
+/-- An element of `charges` which satisfies the linear ACCs
+  gives us a element of `LinSols`. -/
+def chargeToLinear (S : (SM n).charges) (hGrav : accGrav S = 0)
+    (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) : (SM n).LinSols :=
+  ⟨S, by
+    intro i
+    simp at i
+    match i with
+    | 0 => exact hGrav
+    | 1 => exact hSU2
+    | 2 => exact hSU3⟩
+
+/-- An element of `LinSols` which satisfies the quadratic ACCs
+  gives us a element of `QuadSols`. -/
+def linearToQuad (S : (SM n).LinSols) : (SM n).QuadSols :=
+  ⟨S, by
+    intro i
+    exact Fin.elim0 i⟩
+
+/-- An element of `QuadSols` which satisfies the quadratic ACCs
+  gives us a element of `Sols`. -/
+def quadToAF (S : (SM n).QuadSols) (hc : accCube S.val = 0) :
+    (SM n).Sols := ⟨S, hc⟩
+
+/-- An element of `charges` which satisfies the linear and quadratic ACCs
+  gives us a element of `QuadSols`. -/
+def chargeToQuad (S : (SM n).charges) (hGrav : accGrav S = 0)
+    (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) :
+    (SM n).QuadSols :=
+  linearToQuad $ chargeToLinear S hGrav hSU2 hSU3
+
+/-- An element of `charges` which satisfies the linear, quadratic and cubic ACCs
+  gives us a element of `Sols`. -/
+def chargeToAF (S : (SM n).charges) (hGrav : accGrav S = 0) (hSU2 : accSU2 S = 0)
+    (hSU3 : accSU3 S = 0) (hc : accCube S = 0) : (SM n).Sols :=
+  quadToAF (chargeToQuad S hGrav hSU2 hSU3) hc
+
+/-- An element of `LinSols` which satisfies the  quadratic and cubic ACCs
+  gives us a element of `Sols`. -/
+def linearToAF (S : (SM n).LinSols)
+    (hc : accCube S.val = 0) : (SM n).Sols :=
+  quadToAF (linearToQuad S) hc
+
+/-- The permutations acting on the ACC system corresponding to the SM with  RHN. -/
+def perm (n : ℕ) : ACCSystemGroupAction (SM n) where
+  group := permGroup n
+  groupInst := inferInstance
+  rep := repCharges
+  linearInvariant := by
+    intro i
+    simp at i
+    match i with
+    | 0 => exact accGrav_invariant
+    | 1 => exact accSU2_invariant
+    | 2 => exact accSU3_invariant
+  quadInvariant := by
+    intro i
+    simp at i
+    exact Fin.elim0 i
+  cubicInvariant := accCube_invariant
+
+
+end SM
+
+end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean
new file mode 100644
index 0000000..f79fd3a
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
+import HepLean.AnomalyCancellation.SMNu.FamilyMaps
+/-!
+# Family Maps for SM with RHN (no hypercharge)
+
+We give some propererties of the family maps for the SM with RHN, in particular, we
+define family universal maps in the case of `LinSols`, `QuadSols`, and `Sols`.
+-/
+universe v u
+
+namespace SMRHN
+namespace SM
+
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+variable {n : ℕ}
+
+/-- The family universal maps on `LinSols`. -/
+def familyUniversalLinear (n : ℕ) :
+    (SM 1).LinSols →ₗ[ℚ] (SM n).LinSols where
+  toFun S := chargeToLinear (familyUniversal n S.val)
+    (by rw [familyUniversal_accGrav, gravSol S, mul_zero])
+    (by rw [familyUniversal_accSU2, SU2Sol S, mul_zero])
+    (by rw [familyUniversal_accSU3, SU3Sol S, mul_zero])
+  map_add' S T := by
+    apply ACCSystemLinear.LinSols.ext
+    exact (familyUniversal n).map_add' _ _
+  map_smul' a S := by
+    apply ACCSystemLinear.LinSols.ext
+    exact (familyUniversal n).map_smul' _ _
+
+/-- The family universal maps on `QuadSols`. -/
+def familyUniversalQuad (n : ℕ) :
+    (SM 1).QuadSols → (SM n).QuadSols := fun S =>
+  chargeToQuad (familyUniversal n S.val)
+    (by rw [familyUniversal_accGrav, gravSol S.1, mul_zero])
+    (by rw [familyUniversal_accSU2, SU2Sol S.1, mul_zero])
+    (by rw [familyUniversal_accSU3, SU3Sol S.1, mul_zero])
+
+/-- The family universal maps on `Sols`. -/
+def familyUniversalAF (n : ℕ) :
+    (SM 1).Sols → (SM n).Sols := fun S =>
+  chargeToAF (familyUniversal n S.val)
+    (by rw [familyUniversal_accGrav, gravSol S.1.1, mul_zero])
+    (by rw [familyUniversal_accSU2, SU2Sol S.1.1, mul_zero])
+    (by rw [familyUniversal_accSU3, SU3Sol S.1.1, mul_zero])
+    (by rw [familyUniversal_accCube, cubeSol S, mul_zero])
+
+end SM
+end SMRHN