From 7f447c6df89bd3ae888656fd74605e63333a96fb Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 18 Apr 2024 09:06:16 -0400
Subject: [PATCH] feat: Add basics for SMNu PlusU1

---
 HepLean.lean                                  |   4 +-
 .../SMNu/Ordinary/Basic.lean                  |   3 +-
 .../SMNu/PlusU1/Basic.lean                    | 141 ++++++++++++++++++
 .../SMNu/PlusU1/FamilyMaps.lean               |  62 ++++++++
 4 files changed, 207 insertions(+), 3 deletions(-)
 create mode 100644 HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
 create mode 100644 HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean

diff --git a/HepLean.lean b/HepLean.lean
index fce406c..f1f78df 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -19,6 +19,8 @@ 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
+import HepLean.AnomalyCancellation.SMNu.Permutations
+import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
+import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
index d69248d..5de3e2d 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
@@ -8,8 +8,7 @@ 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.
+We define the ACC system for the Standard Model (without hypercharge) with right-handed neutrinos.
 
 -/
 
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
new file mode 100644
index 0000000..933af3c
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
@@ -0,0 +1,141 @@
+/-
+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
+
+We define the ACC system for the Standard Model with right-handed neutrinos.
+
+-/
+universe v u
+
+namespace SMRHN
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+/-- The ACC system for the SM plus RHN with an additional U1. -/
+@[simps!]
+def PlusU1 (n : ℕ) : ACCSystem where
+  numberLinear := 4
+  linearACCs := fun i =>
+    match i with
+    | 0 => @accGrav n
+    | 1 => accSU2
+    | 2 => accSU3
+    | 3 => accYY
+  numberQuadratic := 1
+  quadraticACCs := fun i =>
+    match i with
+    | 0 => accQuad
+  cubicACC := accCube
+
+namespace PlusU1
+
+
+variable {n : ℕ}
+
+lemma gravSol  (S : (PlusU1 n).LinSols) : accGrav S.val = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 0
+
+lemma SU2Sol  (S : (PlusU1 n).LinSols) : accSU2 S.val = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 1
+
+lemma SU3Sol  (S : (PlusU1 n).LinSols) : accSU3 S.val = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 2
+
+lemma YYsol  (S : (PlusU1 n).LinSols) : accYY S.val = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 3
+
+lemma quadSol  (S : (PlusU1 n).QuadSols) : accQuad S.val = 0 := by
+  have hS := S.quadSol
+  simp at hS
+  exact hS 0
+
+lemma cubeSol  (S : (PlusU1 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 : (PlusU1 n).charges) (hGrav : accGrav S = 0)
+    (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) (hYY : accYY S = 0) :
+    (PlusU1 n).LinSols :=
+  ⟨S, by
+    intro i
+    simp at i
+    match i with
+    | 0 => exact hGrav
+    | 1 => exact hSU2
+    | 2 => exact hSU3
+    | 3 => exact hYY⟩
+
+/-- An element of `LinSols` which satisfies the quadratic ACCs
+  gives us a element of `AnomalyFreeQuad`. -/
+def linearToQuad (S : (PlusU1 n).LinSols) (hQ : accQuad S.val = 0) :
+    (PlusU1 n).QuadSols :=
+  ⟨S, by
+    intro i
+    simp at i
+    match i with
+    | 0 => exact hQ⟩
+
+/-- An element of `QuadSols` which satisfies the quadratic ACCs
+  gives us a element of `Sols`. -/
+def quadToAF (S : (PlusU1 n).QuadSols) (hc : accCube S.val = 0) :
+    (PlusU1 n).Sols := ⟨S, hc⟩
+
+/-- An element of `charges` which satisfies the linear and quadratic ACCs
+  gives us a element of `QuadSols`. -/
+def chargeToQuad (S : (PlusU1 n).charges) (hGrav : accGrav S = 0)
+    (hSU2 : accSU2 S = 0) (hSU3 : accSU3 S = 0) (hYY : accYY S = 0) (hQ : accQuad S = 0) :
+    (PlusU1 n).QuadSols :=
+  linearToQuad (chargeToLinear S hGrav hSU2 hSU3 hYY) hQ
+
+/-- An element of `charges` which satisfies the linear, quadratic and cubic ACCs
+  gives us a element of `Sols`. -/
+def chargeToAF (S : (PlusU1 n).charges) (hGrav : accGrav S = 0) (hSU2 : accSU2 S = 0)
+    (hSU3 : accSU3 S = 0) (hYY : accYY S = 0) (hQ : accQuad S = 0) (hc : accCube S = 0) :
+    (PlusU1 n).Sols :=
+  quadToAF (chargeToQuad S hGrav hSU2 hSU3 hYY hQ) hc
+
+/-- An element of `LinSols` which satisfies the  quadratic and cubic ACCs
+  gives us a element of `Sols`. -/
+def linearToAF (S : (PlusU1 n).LinSols) (hQ : accQuad S.val = 0)
+    (hc : accCube S.val = 0) : (PlusU1 n).Sols :=
+  quadToAF (linearToQuad S hQ) hc
+
+/-- The permutations acting on the ACC system corresponding to the SM with  RHN. -/
+def perm (n : ℕ) : ACCSystemGroupAction (PlusU1 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
+    | 3 => exact accYY_invariant
+  quadInvariant := by
+    intro i
+    simp at i
+    match i with
+    | 0 => exact accQuad_invariant
+  cubicInvariant := accCube_invariant
+
+end PlusU1
+
+end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean
new file mode 100644
index 0000000..fbc1c52
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
+import HepLean.AnomalyCancellation.SMNu.FamilyMaps
+/-!
+# Family Maps for SM with RHN
+
+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 PlusU1
+
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+variable {n : ℕ}
+
+/-- The family universal maps on `LinSols`. -/
+def familyUniversalLinear (n : ℕ) :
+    (PlusU1 1).LinSols →ₗ[ℚ] (PlusU1 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])
+    (by rw [familyUniversal_accYY, YYsol 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 : ℕ) :
+    (PlusU1 1).QuadSols → (PlusU1 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])
+    (by rw [familyUniversal_accYY, YYsol S.1, mul_zero])
+    (by rw [familyUniversal_accQuad, quadSol S, mul_zero])
+
+/-- The family universal maps on `Sols`. -/
+def familyUniversalAF (n : ℕ) :
+    (PlusU1 1).Sols → (PlusU1 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_accYY, YYsol S.1.1, mul_zero])
+    (by rw [familyUniversal_accQuad, quadSol S.1, mul_zero])
+    (by rw [familyUniversal_accCube, cubeSol S, mul_zero])
+
+end PlusU1
+end SMRHN