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

Merge pull request #9 from HEPLean/AnomalyCancellation/SMNu

Browse source 
feat: Add SM Nu
This commit is contained in:
Joseph Tooby-Smith 2024-04-18 10:53:11 -04:00 • committed by GitHub
commit 81a7c2b3ab
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
13 changed files with 1806 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
HepLean.lean
View file

@ -16,3 +16,15 @@ import HepLean.AnomalyCancellation.SM.NoGrav.Basic
import HepLean.AnomalyCancellation.SM.NoGrav.One.Lemmas
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.Ordinary.Basic
import HepLean.AnomalyCancellation.SMNu.Ordinary.FamilyMaps
import HepLean.AnomalyCancellation.SMNu.Permutations
import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol

363
HepLean/AnomalyCancellation/SMNu/Basic.lean Normal file
View file

@ -0,0 +1,363 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Mathlib.Tactic.FinCases
import Mathlib.Algebra.Module.Basic
import Mathlib.Tactic.Ring
import Mathlib.Algebra.GroupWithZero.Units.Lemmas
import HepLean.AnomalyCancellation.Basic
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Logic.Equiv.Fin
/-!
# Anomaly cancellation conditions for n family SM.
-/
universe v u
open Nat
open BigOperators
/-- The vector space of charges corresponding to the SM fermions with RHN. -/
@[simps!]
def SMνCharges (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk (6 * n)
/-- The vector spaces of charges of one species of fermions in the SM. -/
@[simps!]
def SMνSpecies (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk n
namespace SMνCharges
variable {n : ℕ}
/-- An equivalence between `(SMνCharges n).charges` and `(Fin 6 → Fin n → ℚ)`
splitting the charges into species.-/
@[simps!]
def toSpeciesEquiv : (SMνCharges n).charges ≃ (Fin 6 → Fin n → ℚ) :=
((Equiv.curry _ _ _).symm.trans ((@finProdFinEquiv 6 n).arrowCongr (Equiv.refl ℚ))).symm
/-- Given an `i ∈ Fin 6`, the projection of charges onto a given species. -/
@[simps!]
def toSpecies (i : Fin 6) : (SMνCharges n).charges →ₗ[ℚ] (SMνSpecies n).charges where
toFun S := toSpeciesEquiv S i
map_add' _ _ := by aesop
map_smul' _ _ := by aesop
lemma charges_eq_toSpecies_eq (S T : (SMνCharges n).charges) :
S = T ↔ ∀ i, toSpecies i S = toSpecies i T := by
apply Iff.intro
intro h
rw [h]
simp only [forall_const]
intro h
apply toSpeciesEquiv.injective
funext i
exact h i
lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f : (Fin 6 → Fin n → ℚ) ) :
(toSpecies i) (toSpeciesEquiv.symm f) = f i := by
change (toSpeciesEquiv ∘ toSpeciesEquiv.symm ) _ i = f i
simp
lemma toSpecies_one (S : (SMνCharges 1).charges) (j : Fin 6) :
toSpecies j S ⟨0, by simp⟩ = S j := by
match j with
| 0 => rfl
| 1 => rfl
| 2 => rfl
| 3 => rfl
| 4 => rfl
| 5 => rfl
/-- The `Q` charges as a map `Fin n → ℚ`. -/
abbrev Q := @toSpecies n 0
/-- The `U` charges as a map `Fin n → ℚ`. -/
abbrev U := @toSpecies n 1
/-- The `D` charges as a map `Fin n → ℚ`. -/
abbrev D := @toSpecies n 2
/-- The `L` charges as a map `Fin n → ℚ`. -/
abbrev L := @toSpecies n 3
/-- The `E` charges as a map `Fin n → ℚ`. -/
abbrev E := @toSpecies n 4
/-- The `N` charges as a map `Fin n → ℚ`. -/
abbrev N := @toSpecies n 5
end SMνCharges
namespace SMνACCs
open SMνCharges
variable {n : ℕ}
/-- The gravitational anomaly equation. -/
@[simp]
def accGrav : (SMνCharges n).charges →ₗ[ℚ] ℚ where
toFun S := ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i + N S i)
map_add' S T := by
simp only
repeat rw [map_add]
simp [Pi.add_apply, mul_add]
repeat erw [Finset.sum_add_distrib]
ring
map_smul' a S := by
simp only
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
-- rw [show Rat.cast a = a from rfl]
ring
lemma accGrav_decomp (S : (SMνCharges n).charges) :
accGrav S = 6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i +
∑ i, N S i := by
simp only [accGrav, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
AddHom.coe_mk]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
/-- Extensionality lemma for `accGrav`. -/
lemma accGrav_ext {S T : (SMνCharges n).charges}
(hj : ∀ (j : Fin 6), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
accGrav S = accGrav T := by
rw [accGrav_decomp, accGrav_decomp]
repeat erw [hj]
/-- The `SU(2)` anomaly equation. -/
@[simp]
def accSU2 : (SMνCharges n).charges →ₗ[ℚ] ℚ where
toFun S := ∑ i, (3 * Q S i + L S i)
map_add' S T := by
simp only
repeat rw [map_add]
simp [Pi.add_apply, mul_add]
repeat erw [Finset.sum_add_distrib]
ring
map_smul' a S := by
simp only
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
-- rw [show Rat.cast a = a from rfl]
ring
lemma accSU2_decomp (S : (SMνCharges n).charges) :
accSU2 S = 3 * ∑ i, Q S i + ∑ i, L S i := by
simp only [accSU2, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
AddHom.coe_mk]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
/-- Extensionality lemma for `accSU2`. -/
lemma accSU2_ext {S T : (SMνCharges n).charges}
(hj : ∀ (j : Fin 6), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
accSU2 S = accSU2 T := by
rw [accSU2_decomp, accSU2_decomp]
repeat erw [hj]
/-- The `SU(3)` anomaly equations. -/
@[simp]
def accSU3 : (SMνCharges n).charges →ₗ[ℚ] ℚ where
toFun S := ∑ i, (2 * Q S i + U S i + D S i)
map_add' S T := by
simp only
repeat rw [map_add]
simp [ Pi.add_apply, mul_add]
repeat erw [Finset.sum_add_distrib]
ring
map_smul' a S := by
simp only
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
-- rw [show Rat.cast a = a from rfl]
ring
lemma accSU3_decomp (S : (SMνCharges n).charges) :
accSU3 S = 2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i := by
simp only [accSU3, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
AddHom.coe_mk]
repeat rw [Finset.sum_add_distrib]
repeat rw [← Finset.mul_sum]
/-- Extensionality lemma for `accSU3`. -/
lemma accSU3_ext {S T : (SMνCharges n).charges}
(hj : ∀ (j : Fin 6), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
accSU3 S = accSU3 T := by
rw [accSU3_decomp, accSU3_decomp]
repeat rw [hj]
/-- The `Y²` anomaly equation. -/
@[simp]
def accYY : (SMνCharges n).charges →ₗ[ℚ] ℚ where
toFun S := ∑ i, (Q S i + 8 * U S i + 2 * D S i + 3 * L S i
+ 6 * E S i)
map_add' S T := by
simp only
repeat rw [map_add]
simp [Pi.add_apply, mul_add]
repeat erw [Finset.sum_add_distrib]
ring
map_smul' a S := by
simp only
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
-- rw [show Rat.cast a = a from rfl]
ring
lemma accYY_decomp (S : (SMνCharges n).charges) :
accYY S = ∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i := by
simp only [accYY, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
AddHom.coe_mk]
repeat rw [Finset.sum_add_distrib]
repeat rw [← Finset.mul_sum]
/-- Extensionality lemma for `accYY`. -/
lemma accYY_ext {S T : (SMνCharges n).charges}
(hj : ∀ (j : Fin 6), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
accYY S = accYY T := by
rw [accYY_decomp, accYY_decomp]
repeat rw [hj]
/-- The quadratic bilinear map. -/
@[simps!]
def quadBiLin : BiLinearSymm (SMνCharges n).charges where
toFun S := ∑ i, (Q S.1 i * Q S.2 i +
- 2 * (U S.1 i * U S.2 i) +
D S.1 i * D S.2 i +
(- 1) * (L S.1 i * L S.2 i) +
E S.1 i * E S.2 i)
map_smul₁' a S T := by
simp only
rw [Finset.mul_sum]
apply Fintype.sum_congr
intro i
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
ring
map_add₁' S T R := by
simp only
rw [← Finset.sum_add_distrib]
apply Fintype.sum_congr
intro i
repeat erw [map_add]
simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue, neg_mul,
one_mul]
ring
swap' S T := by
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
apply Fintype.sum_congr
intro i
ring
lemma quadBiLin_decomp (S T : (SMνCharges n).charges) :
quadBiLin (S, T) = ∑ i, Q S i * Q T i - 2 * ∑ i, U S i * U T i +
∑ i, D S i * D T i - ∑ i, L S i * L T i + ∑ i, E S i * E T i := by
erw [← quadBiLin.toFun_eq_coe]
rw [quadBiLin]
simp only
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul, add_left_inj]
ring
/-- The quadratic anomaly cancellation condition. -/
@[simp]
def accQuad : HomogeneousQuadratic (SMνCharges n).charges :=
(@quadBiLin n).toHomogeneousQuad
lemma accQuad_decomp (S : (SMνCharges n).charges) :
accQuad S = ∑ i, (Q S i)^2 - 2 * ∑ i, (U S i)^2 + ∑ i, (D S i)^2 - ∑ i, (L S i)^2
+ ∑ i, (E S i)^2 := by
erw [quadBiLin_decomp]
ring_nf
/-- Extensionality lemma for `accQuad`. -/
lemma accQuad_ext {S T : (SMνCharges n).charges}
(h : ∀ j, ∑ i, ((fun a => a^2) ∘ toSpecies j S) i =
∑ i, ((fun a => a^2) ∘ toSpecies j T) i) :
accQuad S = accQuad T := by
rw [accQuad_decomp, accQuad_decomp]
erw [h 0, h 1, h 2, h 3, h 4]
rfl
/-- The symmetric trilinear form used to define the cubic acc. -/
@[simps!]
def cubeTriLin : TriLinearSymm (SMνCharges n).charges where
toFun S := ∑ i, (6 * ((Q S.1 i) * (Q S.2.1 i) * (Q S.2.2 i))
+ 3 * ((U S.1 i) * (U S.2.1 i) * (U S.2.2 i))
+ 3 * ((D S.1 i) * (D S.2.1 i) * (D S.2.2 i))
+ 2 * ((L S.1 i) * (L S.2.1 i) * (L S.2.2 i))
+ ((E S.1 i) * (E S.2.1 i) * (E S.2.2 i))
+ ((N S.1 i) * (N S.2.1 i) * (N S.2.2 i)))
map_smul₁' a S T R := by
simp only
rw [Finset.mul_sum]
apply Fintype.sum_congr
intro i
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
ring
map_add₁' S T R L := by
simp only
rw [← Finset.sum_add_distrib]
apply Fintype.sum_congr
intro i
repeat erw [map_add]
simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue]
ring
swap₁' S T L := by
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
apply Fintype.sum_congr
intro i
ring
swap₂' S T L := by
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
apply Fintype.sum_congr
intro i
ring
lemma cubeTriLin_decomp (S T R : (SMνCharges n).charges) :
cubeTriLin (S, T, R) = 6 * ∑ i, (Q S i * Q T i * Q R i) + 3 * ∑ i, (U S i * U T i * U R i) +
3 * ∑ i, (D S i * D T i * D R i) + 2 * ∑ i, (L S i * L T i * L R i) +
∑ i, (E S i * E T i * E R i) + ∑ i, (N S i * N T i * N R i) := by
erw [← cubeTriLin.toFun_eq_coe]
rw [cubeTriLin]
simp only
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
/-- The cubic ACC. -/
@[simp]
def accCube : HomogeneousCubic (SMνCharges n).charges := cubeTriLin.toCubic
lemma accCube_decomp (S : (SMνCharges n).charges) :
accCube S = 6 * ∑ i, (Q S i)^3 + 3 * ∑ i, (U S i)^3 + 3 * ∑ i, (D S i)^3 + 2 * ∑ i, (L S i)^3 +
∑ i, (E S i)^3 + ∑ i, (N S i)^3 := by
erw [cubeTriLin_decomp]
ring_nf
/-- Extensionality lemma for `accCube`. -/
lemma accCube_ext {S T : (SMνCharges n).charges}
(h : ∀ j, ∑ i, ((fun a => a^3) ∘ toSpecies j S) i =
∑ i, ((fun a => a^3) ∘ toSpecies j T) i) :
accCube S = accCube T := by
rw [accCube_decomp]
have h1 : ∀ j, ∑ i, (toSpecies j S i) ^ 3 = ∑ i, (toSpecies j T i) ^ 3 := by
intro j
erw [h]
rfl
repeat rw [h1]
rw [accCube_decomp]
end SMνACCs

245
HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean Normal file
View file

@ -0,0 +1,245 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.Basic
/-!
# Family maps for the Standard Model for RHN ACCs
We define the a series of maps between the charges for different numbers of famlies.
-/
universe v u
namespace SMRHN
open SMνCharges
open SMνACCs
open BigOperators
/-- Given a map of for a generic species, the corresponding map for charges. -/
@[simps!]
def chargesMapOfSpeciesMap {n m : ℕ} (f : (SMνSpecies n).charges →ₗ[ℚ] (SMνSpecies m).charges) :
(SMνCharges n).charges →ₗ[ℚ] (SMνCharges m).charges where
toFun S := toSpeciesEquiv.symm (fun i => (LinearMap.comp f (toSpecies i)) S)
map_add' S T := by
rw [charges_eq_toSpecies_eq]
intro i
rw [map_add]
rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
rw [map_add]
map_smul' a S := by
rw [charges_eq_toSpecies_eq]
intro i
rw [map_smul]
rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
rw [map_smul]
rfl
lemma chargesMapOfSpeciesMap_toSpecies {n m : ℕ}
(f : (SMνSpecies n).charges →ₗ[ℚ] (SMνSpecies m).charges)
(S : (SMνCharges n).charges) (j : Fin 6) :
toSpecies j (chargesMapOfSpeciesMap f S) = (LinearMap.comp f (toSpecies j)) S := by
erw [toSMSpecies_toSpecies_inv]
/-- The projection of the `m`-family charges onto the first `n`-family charges for species. -/
@[simps!]
def speciesFamilyProj {m n : ℕ} (h : n ≤ m) :
(SMνSpecies m).charges →ₗ[ℚ] (SMνSpecies n).charges where
toFun S := S ∘ Fin.castLE h
map_add' S T := by
funext i
simp
map_smul' a S := by
funext i
simp [HSMul.hSMul]
-- rw [show Rat.cast a = a from rfl]
/-- The projection of the `m`-family charges onto the first `n`-family charges. -/
def familyProjection {m n : ℕ} (h : n ≤ m) : (SMνCharges m).charges →ₗ[ℚ] (SMνCharges n).charges :=
chargesMapOfSpeciesMap (speciesFamilyProj h)
/-- For species, the embedding of the `m`-family charges onto the `n`-family charges, with all
other charges zero. -/
@[simps!]
def speciesEmbed (m n : ℕ) :
(SMνSpecies m).charges →ₗ[ℚ] (SMνSpecies n).charges where
toFun S := fun i =>
if hi : i.val < m then
S ⟨i, hi⟩
else
0
map_add' S T := by
funext i
simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add]
by_cases hi : i.val < m
erw [dif_pos hi, dif_pos hi, dif_pos hi]
erw [dif_neg hi, dif_neg hi, dif_neg hi]
rfl
map_smul' a S := by
funext i
simp [HSMul.hSMul]
by_cases hi : i.val < m
erw [dif_pos hi, dif_pos hi]
erw [dif_neg hi, dif_neg hi]
simp
/-- The embedding of the `m`-family charges onto the `n`-family charges, with all
other charges zero. -/
def familyEmbedding (m n : ℕ) : (SMνCharges m).charges →ₗ[ℚ] (SMνCharges n).charges :=
chargesMapOfSpeciesMap (speciesEmbed m n)
/-- For species, the embeddding of the `1`-family charges into the `n`-family charges in
a universal manor. -/
@[simps!]
def speciesFamilyUniversial (n : ℕ) :
(SMνSpecies 1).charges →ₗ[ℚ] (SMνSpecies n).charges where
toFun S _ := S ⟨0, by simp⟩
map_add' S T := by
funext _
simp
map_smul' a S := by
funext i
simp [HSMul.hSMul]
-- rw [show Rat.cast a = a from rfl]
/-- The embeddding of the `1`-family charges into the `n`-family charges in
a universal manor. -/
def familyUniversal (n : ℕ) : (SMνCharges 1).charges →ₗ[ℚ] (SMνCharges n).charges :=
chargesMapOfSpeciesMap (speciesFamilyUniversial n)
lemma toSpecies_familyUniversal {n : ℕ} (j : Fin 6) (S : (SMνCharges 1).charges)
(i : Fin n) : toSpecies j (familyUniversal n S) i = toSpecies j S ⟨0, by simp⟩ := by
erw [chargesMapOfSpeciesMap_toSpecies]
rfl
lemma sum_familyUniversal {n : ℕ} (m : ℕ) (S : (SMνCharges 1).charges) (j : Fin 6) :
∑ i, ((fun a => a ^ m) ∘ toSpecies j (familyUniversal n S)) i =
n * (toSpecies j S ⟨0, by simp⟩) ^ m := by
simp only [SMνSpecies_numberCharges, Function.comp_apply, toSpecies_apply, Fin.zero_eta,
Fin.isValue]
have h1 : (n : ℚ) * (toSpecies j S ⟨0, by simp⟩) ^ m =
∑ _i : Fin n, (toSpecies j S ⟨0, by simp⟩) ^ m := by
rw [Fin.sum_const]
simp
erw [h1]
apply Finset.sum_congr
simp only
intro i _
erw [toSpecies_familyUniversal]
lemma sum_familyUniversal_one {n : ℕ} (S : (SMνCharges 1).charges) (j : Fin 6) :
∑ i, toSpecies j (familyUniversal n S) i = n * (toSpecies j S ⟨0, by simp⟩) := by
simpa using @sum_familyUniversal n 1 S j
lemma sum_familyUniversal_two {n : ℕ} (S : (SMνCharges 1).charges)
(T : (SMνCharges n).charges) (j : Fin 6) :
∑ i, (toSpecies j (familyUniversal n S) i * toSpecies j T i) =
(toSpecies j S ⟨0, by simp⟩) * ∑ i, toSpecies j T i := by
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.zero_eta, Fin.isValue]
rw [Finset.mul_sum]
apply Finset.sum_congr
simp only
intro i _
erw [toSpecies_familyUniversal]
rfl
lemma sum_familyUniversal_three {n : ℕ} (S : (SMνCharges 1).charges)
(T L : (SMνCharges n).charges) (j : Fin 6) :
∑ i, (toSpecies j (familyUniversal n S) i * toSpecies j T i * toSpecies j L i) =
(toSpecies j S ⟨0, by simp⟩) * ∑ i, toSpecies j T i * toSpecies j L i := by
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.zero_eta, Fin.isValue]
rw [Finset.mul_sum]
apply Finset.sum_congr
simp only
intro i _
erw [toSpecies_familyUniversal]
simp only [SMνSpecies_numberCharges, Fin.zero_eta, Fin.isValue, toSpecies_apply]
ring
lemma familyUniversal_accGrav (S : (SMνCharges 1).charges) :
accGrav (familyUniversal n S) = n * (accGrav S) := by
rw [accGrav_decomp, accGrav_decomp]
repeat rw [sum_familyUniversal_one]
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
ring
lemma familyUniversal_accSU2 (S : (SMνCharges 1).charges) :
accSU2 (familyUniversal n S) = n * (accSU2 S) := by
rw [accSU2_decomp, accSU2_decomp]
repeat rw [sum_familyUniversal_one]
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
ring
lemma familyUniversal_accSU3 (S : (SMνCharges 1).charges) :
accSU3 (familyUniversal n S) = n * (accSU3 S) := by
rw [accSU3_decomp, accSU3_decomp]
repeat rw [sum_familyUniversal_one]
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
ring
lemma familyUniversal_accYY (S : (SMνCharges 1).charges) :
accYY (familyUniversal n S) = n * (accYY S) := by
rw [accYY_decomp, accYY_decomp]
repeat rw [sum_familyUniversal_one]
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
ring
lemma familyUniversal_quadBiLin (S : (SMνCharges 1).charges) (T : (SMνCharges n).charges) :
quadBiLin (familyUniversal n S, T) =
S (0 : Fin 6) * ∑ i, Q T i - 2 * S (1 : Fin 6) * ∑ i, U T i + S (2 : Fin 6) *∑ i, D T i -
S (3 : Fin 6) * ∑ i, L T i + S (4 : Fin 6) * ∑ i, E T i := by
rw [quadBiLin_decomp]
repeat rw [sum_familyUniversal_two]
repeat rw [toSpecies_one]
simp only [Fin.isValue, SMνSpecies_numberCharges, toSpecies_apply, add_left_inj, sub_left_inj,
sub_right_inj]
ring
lemma familyUniversal_accQuad (S : (SMνCharges 1).charges) :
accQuad (familyUniversal n S) = n * (accQuad S) := by
rw [accQuad_decomp]
repeat erw [sum_familyUniversal]
rw [accQuad_decomp]
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
ring
lemma familyUniversal_cubeTriLin (S : (SMνCharges 1).charges) (T R : (SMνCharges n).charges) :
cubeTriLin (familyUniversal n S, T, R) = 6 * S (0 : Fin 6) * ∑ i, (Q T i * Q R i) +
3 * S (1 : Fin 6) * ∑ i, (U T i * U R i) + 3 * S (2 : Fin 6) * ∑ i, (D T i * D R i)
+ 2 * S (3 : Fin 6) * ∑ i, (L T i * L R i) +
S (4 : Fin 6) * ∑ i, (E T i * E R i) + S (5 : Fin 6) * ∑ i, (N T i * N R i) := by
rw [cubeTriLin_decomp]
repeat rw [sum_familyUniversal_three]
repeat rw [toSpecies_one]
simp only [Fin.isValue, SMνSpecies_numberCharges, toSpecies_apply, add_left_inj]
ring
lemma familyUniversal_cubeTriLin' (S T : (SMνCharges 1).charges) (R : (SMνCharges n).charges) :
cubeTriLin (familyUniversal n S, familyUniversal n T, R) =
6 * S (0 : Fin 6) * T (0 : Fin 6) * ∑ i, Q R i +
3 * S (1 : Fin 6) * T (1 : Fin 6) * ∑ i, U R i
+ 3 * S (2 : Fin 6) * T (2 : Fin 6) * ∑ i, D R i +
2 * S (3 : Fin 6) * T (3 : Fin 6) * ∑ i, L R i +
S (4 : Fin 6) * T (4 : Fin 6) * ∑ i, E R i + S (5 : Fin 6) * T (5 : Fin 6) * ∑ i, N R i := by
rw [familyUniversal_cubeTriLin]
repeat rw [sum_familyUniversal_two]
repeat rw [toSpecies_one]
simp only [Fin.isValue, SMνSpecies_numberCharges, toSpecies_apply]
ring
lemma familyUniversal_accCube (S : (SMνCharges 1).charges) :
accCube (familyUniversal n S) = n * (accCube S) := by
rw [accCube_decomp]
repeat erw [sum_familyUniversal]
rw [accCube_decomp]
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
ring
end SMRHN

115
HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean Normal file
View file

@ -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

124
HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean Normal file
View file

@ -0,0 +1,124 @@
/-
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 (without hypercharge) 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. -/
@[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

57
HepLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean Normal file
View file

@ -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

124
HepLean/AnomalyCancellation/SMNu/Permutations.lean Normal file
View file

@ -0,0 +1,124 @@
/-
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 Mathlib.Tactic.Polyrith
import HepLean.AnomalyCancellation.GroupActions
/-!
# Permutations of SM charges with RHN.
We define the group of permutations for the SM charges with RHN.
-/
universe v u
open Nat
open Finset
namespace SMRHN
open SMνCharges
open SMνACCs
open BigOperators
/-- The group of `Sₙ` permutations for each species. -/
@[simp]
def permGroup (n : ℕ) := Fin 6 → Equiv.Perm (Fin n)
variable {n : ℕ}
@[simp]
instance : Group (permGroup n) := Pi.group
/-- The image of an element of `permGroup n` under the representation on charges. -/
@[simps!]
def chargeMap (f : permGroup n) : (SMνCharges n).charges →ₗ[ℚ] (SMνCharges n).charges where
toFun S := toSpeciesEquiv.symm (fun i => toSpecies i S ∘ f i )
map_add' S T := by
simp only
rw [charges_eq_toSpecies_eq]
intro i
rw [(toSpecies i).map_add]
rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
rfl
map_smul' a S := by
simp only
rw [charges_eq_toSpecies_eq]
intro i
rw [(toSpecies i).map_smul, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
rfl
/-- The representation of `(permGroup n)` acting on the vector space of charges. -/
@[simp]
def repCharges {n : ℕ} : Representation ℚ (permGroup n) (SMνCharges n).charges where
toFun f := chargeMap f⁻¹
map_mul' f g :=by
simp only [permGroup, mul_inv_rev]
apply LinearMap.ext
intro S
rw [charges_eq_toSpecies_eq]
intro i
simp only [chargeMap_apply, Pi.mul_apply, Pi.inv_apply, Equiv.Perm.coe_mul, LinearMap.mul_apply]
repeat erw [toSMSpecies_toSpecies_inv]
rfl
map_one' := by
apply LinearMap.ext
intro S
rw [charges_eq_toSpecies_eq]
intro i
erw [toSMSpecies_toSpecies_inv]
rfl
lemma repCharges_toSpecies (f : permGroup n) (S : (SMνCharges n).charges) (j : Fin 6) :
toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
erw [toSMSpecies_toSpecies_inv]
lemma toSpecies_sum_invariant (m : ℕ) (f : permGroup n) (S : (SMνCharges n).charges) (j : Fin 6) :
∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by
erw [repCharges_toSpecies]
change ∑ i : Fin n, ((fun a => a ^ m) ∘ _) (⇑(f⁻¹ _) i) = ∑ i : Fin n, ((fun a => a ^ m) ∘ _) i
refine Equiv.Perm.sum_comp _ _ _ ?_
simp only [permGroup, Fin.isValue, Pi.inv_apply, ne_eq, coe_univ, Set.subset_univ]
lemma accGrav_invariant (f : permGroup n) (S : (SMνCharges n).charges) :
accGrav (repCharges f S) = accGrav S :=
accGrav_ext
(by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU2_invariant (f : permGroup n) (S : (SMνCharges n).charges) :
accSU2 (repCharges f S) = accSU2 S :=
accSU2_ext
(by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU3_invariant (f : permGroup n) (S : (SMνCharges n).charges) :
accSU3 (repCharges f S) = accSU3 S :=
accSU3_ext
(by simpa using toSpecies_sum_invariant 1 f S)
lemma accYY_invariant (f : permGroup n) (S : (SMνCharges n).charges) :
accYY (repCharges f S) = accYY S :=
accYY_ext
(by simpa using toSpecies_sum_invariant 1 f S)
lemma accQuad_invariant (f : permGroup n) (S : (SMνCharges n).charges) :
accQuad (repCharges f S) = accQuad S :=
accQuad_ext
(toSpecies_sum_invariant 2 f S)
lemma accCube_invariant (f : permGroup n) (S : (SMνCharges n).charges) :
accCube (repCharges f S) = accCube S :=
accCube_ext
(by simpa using toSpecies_sum_invariant 3 f S)
end SMRHN

120
HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean Normal file
View file

@ -0,0 +1,120 @@
/-
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.PlusU1.FamilyMaps
/-!
# B Minus L in SM with RHN.
Relavent definitions for the SM `B-L`.
-/
universe v u
namespace SMRHN
namespace PlusU1
open SMνCharges
open SMνACCs
open BigOperators
variable {n : ℕ}
/-- $B - L$ in the 1-family case. -/
@[simps!]
def BL₁ : (PlusU1 1).Sols where
val := fun i =>
match i with
| (0 : Fin 6) => 1
| (1 : Fin 6) => -1
| (2 : Fin 6) => -1
| (3 : Fin 6) => -3
| (4 : Fin 6) => 3
| (5 : Fin 6) => 3
linearSol := by
intro i
simp at i
match i with
| 0 => rfl
| 1 => rfl
| 2 => rfl
| 3 => rfl
quadSol := by
intro i
simp at i
match i with
| 0 => rfl
cubicSol := by rfl
/-- $B - L$ in the $n$-family case. -/
@[simps!]
def BL (n : ℕ) : (PlusU1 n).Sols :=
familyUniversalAF n BL₁
namespace BL
variable {n : ℕ}
lemma on_quadBiLin (S : (PlusU1 n).charges) :
quadBiLin ((BL n).val, S) = 1/2 * accYY S + 3/2 * accSU2 S - 2 * accSU3 S := by
erw [familyUniversal_quadBiLin]
rw [accYY_decomp, accSU2_decomp, accSU3_decomp]
simp only [Fin.isValue, BL₁_val, SMνSpecies_numberCharges, toSpecies_apply, one_mul, mul_neg,
mul_one, neg_mul, sub_neg_eq_add, one_div]
ring
lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin ((BL n).val, S.val) = 0 := by
rw [on_quadBiLin]
rw [YYsol S, SU2Sol S, SU3Sol S]
simp
lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
accQuad (a • S.val + b • (BL n).val) = a ^ 2 * accQuad S.val := by
erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • (BL n)).1]
rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂, quadBiLin.swap, on_quadBiLin_AFL]
erw [accQuad.map_smul]
simp
lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) :
accQuad (a • S.val + b • (BL n).val) = 0 := by
rw [add_AFL_quad, quadSol S]
simp
/-- The `QuadSol` obtained by adding $B-L$ to a `QuadSol`. -/
def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
linearToQuad (a • S.1 + b • (BL n).1.1) (add_quad S a b)
lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ): addQuad S a 0 = a • S := by
simp [addQuad, linearToQuad]
rfl
lemma on_cubeTriLin (S : (PlusU1 n).charges) :
cubeTriLin ((BL n).val, (BL n).val, S) = 9 * accGrav S - 24 * accSU3 S := by
erw [familyUniversal_cubeTriLin']
rw [accGrav_decomp, accSU3_decomp]
simp only [Fin.isValue, BL₁_val, mul_one, SMνSpecies_numberCharges, toSpecies_apply, mul_neg,
neg_neg, neg_mul]
ring
lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
cubeTriLin ((BL n).val, (BL n).val, S.val) = 0 := by
rw [on_cubeTriLin]
rw [gravSol S, SU3Sol S]
simp
lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
accCube (a • S.val + b • (BL n).val) =
a ^ 2 * (a * accCube S.val + 3 * b * cubeTriLin (S.val, S.val, (BL n).val)) := by
erw [TriLinearSymm.toCubic_add, cubeSol (b • (BL n)), accCube.map_smul]
repeat rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
rw [on_cubeTriLin_AFL]
simp only [accCube, TriLinearSymm.toCubic_toFun, cubeTriLin_toFun, Fin.isValue, add_zero, BL_val,
mul_zero]
ring
end BL
end PlusU1
end SMRHN

141
HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean Normal file
View file

@ -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

62
HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean Normal file
View file

@ -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

150
HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean Normal file
View file

@ -0,0 +1,150 @@
/-
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.PlusU1.FamilyMaps
/-!
# Hypercharge in SM with RHN.
Relavent definitions for the SM hypercharge.
-/
universe v u
namespace SMRHN
namespace PlusU1
open SMνCharges
open SMνACCs
open BigOperators
/-- The hypercharge for 1 family. -/
@[simps!]
def Y₁ : (PlusU1 1).Sols where
val := fun i =>
match i with
| (0 : Fin 6) => 1
| (1 : Fin 6) => -4
| (2 : Fin 6) => 2
| (3 : Fin 6) => -3
| (4 : Fin 6) => 6
| (5 : Fin 6) => 0
linearSol := by
intro i
simp at i
match i with
| 0 => rfl
| 1 => rfl
| 2 => rfl
| 3 => rfl
quadSol := by
intro i
simp at i
match i with
| 0 => rfl
cubicSol := by rfl
/-- The hypercharge for `n` family. -/
@[simps!]
def Y (n : ℕ) : (PlusU1 n).Sols :=
familyUniversalAF n Y₁
namespace Y
variable {n : ℕ}
lemma on_quadBiLin (S : (PlusU1 n).charges) :
quadBiLin ((Y n).val, S) = accYY S := by
erw [familyUniversal_quadBiLin]
rw [accYY_decomp]
simp only [Fin.isValue, Y₁_val, SMνSpecies_numberCharges, toSpecies_apply, one_mul, mul_neg,
neg_mul, sub_neg_eq_add, add_left_inj, add_right_inj, mul_eq_mul_right_iff]
ring_nf
simp
lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin ((Y n).val, S.val) = 0 := by
rw [on_quadBiLin]
rw [YYsol S]
lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
accQuad (a • S.val + b • (Y n).val) = a ^ 2 * accQuad S.val := by
erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • (Y n)).1]
rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂, quadBiLin.swap, on_quadBiLin_AFL]
erw [accQuad.map_smul]
simp
lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) :
accQuad (a • S.val + b • (Y n).val) = 0 := by
rw [add_AFL_quad, quadSol S]
simp
/-- The `QuadSol` obtained by adding hypercharge to a `QuadSol`. -/
def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
linearToQuad (a • S.1 + b • (Y n).1.1) (add_quad S a b)
lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ): addQuad S a 0 = a • S := by
simp [addQuad, linearToQuad]
rfl
lemma on_cubeTriLin (S : (PlusU1 n).charges) :
cubeTriLin ((Y n).val, (Y n).val, S) = 6 * accYY S := by
erw [familyUniversal_cubeTriLin']
rw [accYY_decomp]
simp only [Fin.isValue, Y₁_val, mul_one, SMνSpecies_numberCharges, toSpecies_apply, mul_neg,
neg_mul, neg_neg, mul_zero, zero_mul, add_zero]
ring
lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
cubeTriLin ((Y n).val, (Y n).val, S.val) = 0 := by
rw [on_cubeTriLin]
rw [YYsol S]
simp
lemma on_cubeTriLin' (S : (PlusU1 n).charges) :
cubeTriLin ((Y n).val, S, S) = 6 * accQuad S := by
erw [familyUniversal_cubeTriLin]
rw [accQuad_decomp]
simp only [Fin.isValue, Y₁_val, mul_one, SMνSpecies_numberCharges, toSpecies_apply, mul_neg,
neg_mul, zero_mul, add_zero]
ring_nf
lemma on_cubeTriLin'_ALQ (S : (PlusU1 n).QuadSols) :
cubeTriLin ((Y n).val, S.val, S.val) = 0 := by
rw [on_cubeTriLin']
rw [quadSol S]
simp
lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
accCube (a • S.val + b • (Y n).val) =
a ^ 2 * (a * accCube S.val + 3 * b * cubeTriLin (S.val, S.val, (Y n).val)) := by
erw [TriLinearSymm.toCubic_add, cubeSol (b • (Y n)), accCube.map_smul]
repeat rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
rw [on_cubeTriLin_AFL]
simp only [accCube, TriLinearSymm.toCubic_toFun, cubeTriLin_toFun, Fin.isValue, add_zero, Y_val,
mul_zero]
ring
lemma add_AFQ_cube (S : (PlusU1 n).QuadSols) (a b : ℚ) :
accCube (a • S.val + b • (Y n).val) = a ^ 3 * accCube S.val := by
rw [add_AFL_cube]
rw [cubeTriLin.swap₃]
rw [on_cubeTriLin'_ALQ]
ring
lemma add_AF_cube (S : (PlusU1 n).Sols) (a b : ℚ) :
accCube (a • S.val + b • (Y n).val) = 0 := by
rw [add_AFQ_cube]
rw [cubeSol S]
simp
/-- The `Sol` obtained by adding hypercharge to a `Sol`. -/
def addCube (S : (PlusU1 n).Sols) (a b : ℚ) : (PlusU1 n).Sols :=
quadToAF (addQuad S.1 a b) (add_AF_cube S a b)
end Y
end PlusU1
end SMRHN

146
HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean Normal file
View file

@ -0,0 +1,146 @@
/-
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.PlusU1.FamilyMaps
/-!
# Properties of Quad Sols for SM with RHN
We give a series of properties held by solutions to the quadratic equation.
In particular given a quad solution we define a map from linear solutions to quadratic solutions
and show that it is a surjection. The main reference for this is:
- https://arxiv.org/abs/2006.03588
-/
universe v u
namespace SMRHN
namespace PlusU1
open SMνCharges
open SMνACCs
open BigOperators
namespace QuadSol
variable {n : ℕ}
variable (C : (PlusU1 n).QuadSols)
lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
accQuad (a • S.val + b • C.val) =
a * (a * accQuad S.val + 2 * b * quadBiLin (S.val, C.val)) := by
erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • C)]
rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂]
erw [accQuad.map_smul]
ring
/-- A helper function for what comes later. -/
def α₁ (S : (PlusU1 n).LinSols) : ℚ := - 2 * quadBiLin (S.val, C.val)
/-- A helper function for what comes later. -/
def α₂ (S : (PlusU1 n).LinSols) : ℚ := accQuad S.val
lemma α₂_AFQ (S : (PlusU1 n).QuadSols) : α₂ S.1 = 0 := quadSol S
lemma accQuad_α₁_α₂ (S : (PlusU1 n).LinSols) :
accQuad ((α₁ C S) • S + α₂ S • C.1).val = 0 := by
erw [add_AFL_quad]
rw [α₁, α₂]
ring
lemma accQuad_α₁_α₂_zero (S : (PlusU1 n).LinSols) (h1 : α₁ C S = 0)
(h2 : α₂ S = 0) (a b : ℚ) : accQuad (a • S + b • C.1).val = 0 := by
erw [add_AFL_quad]
simp [α₁, α₂] at h1 h2
field_simp [h1, h2]
/-- The construction of a `QuadSol` from a `LinSols` in the generic case. -/
def genericToQuad (S : (PlusU1 n).LinSols) :
(PlusU1 n).QuadSols :=
linearToQuad ((α₁ C S) • S + α₂ S • C.1) (accQuad_α₁_α₂ C S)
lemma genericToQuad_on_quad (S : (PlusU1 n).QuadSols) :
genericToQuad C S.1 = (α₁ C S.1) • S := by
apply ACCSystemQuad.QuadSols.ext
change ((α₁ C S.1) • S.val + α₂ S.1 • C.val) = (α₁ C S.1) • S.val
rw [α₂_AFQ]
simp
lemma genericToQuad_neq_zero (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 ≠ 0) :
(α₁ C S.1)⁻¹ • genericToQuad C S.1 = S := by
rw [genericToQuad_on_quad, smul_smul, inv_mul_cancel h, one_smul]
/-- The construction of a `QuadSol` from a `LinSols` in the special case when `α₁ C S = 0` and
`α₂ S = 0`. -/
def specialToQuad (S : (PlusU1 n).LinSols) (a b : ℚ) (h1 : α₁ C S = 0)
(h2 : α₂ S = 0) : (PlusU1 n).QuadSols :=
linearToQuad (a • S + b • C.1) (accQuad_α₁_α₂_zero C S h1 h2 a b)
lemma special_on_quad (S : (PlusU1 n).QuadSols) (h1 : α₁ C S.1 = 0) :
specialToQuad C S.1 1 0 h1 (α₂_AFQ S) = S := by
apply ACCSystemQuad.QuadSols.ext
change (1 • S.val + 0 • C.val) = S.val
simp
/-- The construction of a `QuadSols` from a `LinSols` and two rationals taking account of the
generic and special cases. This function is a surjection. -/
def toQuad : (PlusU1 n).LinSols × ℚ × ℚ → (PlusU1 n).QuadSols := fun S =>
if h : α₁ C S.1 = 0 ∧ α₂ S.1 = 0 then
specialToQuad C S.1 S.2.1 S.2.2 h.1 h.2
else
S.2.1 • genericToQuad C S.1
/-- A function from `QuadSols` to `LinSols × ℚ × ℚ` which is a right inverse to `toQuad`. -/
@[simp]
def toQuadInv : (PlusU1 n).QuadSols → (PlusU1 n).LinSols × ℚ × ℚ := fun S =>
if α₁ C S.1 = 0 then
(S.1, 1, 0)
else
(S.1, (α₁ C S.1)⁻¹, 0)
lemma toQuadInv_fst (S : (PlusU1 n).QuadSols) :
(toQuadInv C S).1 = S.1 := by
rw [toQuadInv]
split
rfl
rfl
lemma toQuadInv_α₁_α₂ (S : (PlusU1 n).QuadSols) :
α₁ C S.1 = 0 ↔ α₁ C (toQuadInv C S).1 = 0 ∧ α₂ (toQuadInv C S).1 = 0 := by
rw [toQuadInv_fst, α₂_AFQ]
simp
lemma toQuadInv_special (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 = 0) :
specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2
((toQuadInv_α₁_α₂ C S).mp h).1 ((toQuadInv_α₁_α₂ C S).mp h).2 = S := by
simp only [toQuadInv_fst]
rw [show (toQuadInv C S).2.1 = 1 by rw [toQuadInv, if_pos h]]
rw [show (toQuadInv C S).2.2 = 0 by rw [toQuadInv, if_pos h]]
rw [special_on_quad]
lemma toQuadInv_generic (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 ≠ 0) :
(toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = S := by
simp only [toQuadInv_fst]
rw [show (toQuadInv C S).2.1 = (α₁ C S.1)⁻¹ by rw [toQuadInv, if_neg h]]
rw [genericToQuad_neq_zero C S h]
lemma toQuad_rightInverse : Function.RightInverse (@toQuadInv n C) (toQuad C) := by
intro S
by_cases h : α₁ C S.1 = 0
rw [toQuad, dif_pos ((toQuadInv_α₁_α₂ C S).mp h)]
exact toQuadInv_special C S h
rw [toQuad, dif_neg ((toQuadInv_α₁_α₂ C S).mpr.mt h)]
exact toQuadInv_generic C S h
theorem toQuad_surjective : Function.Surjective (toQuad C) :=
Function.RightInverse.surjective (toQuad_rightInverse C)
end QuadSol
end PlusU1
end SMRHN

147
HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean Normal file
View file

@ -0,0 +1,147 @@
/-
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.PlusU1.BMinusL
/-!
# Solutions from quad solutions
We use $B-L$ to form a surjective map from quad solutions to solutions. The main reference
for this material is:
- https://arxiv.org/abs/2006.03588
-/
universe v u
namespace SMRHN
namespace PlusU1
namespace QuadSolToSol
open SMνCharges
open SMνACCs
open BigOperators
variable {n : ℕ}
/-- A helper function for what follows. -/
@[simp]
def α₁ (S : (PlusU1 n).QuadSols) : ℚ := - 3 * cubeTriLin (S.val, S.val, (BL n).val)
/-- A helper function for what follows. -/
@[simp]
def α₂ (S : (PlusU1 n).QuadSols) : ℚ := accCube S.val
lemma cube_α₁_α₂_zero (S : (PlusU1 n).QuadSols) (a b : ℚ) (h1 : α₁ S = 0) (h2 : α₂ S = 0) :
accCube (BL.addQuad S a b).val = 0 := by
erw [BL.add_AFL_cube]
simp_all
lemma α₂_AF (S : (PlusU1 n).Sols) : α₂ S.toQuadSols = 0 := S.2
lemma BL_add_α₁_α₂_cube (S : (PlusU1 n).QuadSols) :
accCube (BL.addQuad S (α₁ S) (α₂ S)).val = 0 := by
erw [BL.add_AFL_cube]
field_simp
ring_nf
lemma BL_add_α₁_α₂_AF (S : (PlusU1 n).Sols) :
BL.addQuad S.1 (α₁ S.1) (α₂ S.1) = (α₁ S.1) • S.1 := by
rw [α₂_AF, BL.addQuad_zero]
/-- The construction of a `Sol` from a `QuadSol` in the generic case. -/
def generic (S : (PlusU1 n).QuadSols) : (PlusU1 n).Sols :=
quadToAF (BL.addQuad S (α₁ S) (α₂ S)) (BL_add_α₁_α₂_cube S)
lemma generic_on_AF (S : (PlusU1 n).Sols) : generic S.1 = (α₁ S.1) • S := by
apply ACCSystem.Sols.ext
change (BL.addQuad S.1 (α₁ S.1) (α₂ S.1)).val = _
rw [BL_add_α₁_α₂_AF]
rfl
lemma generic_on_AF_α₁_ne_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
(α₁ S.1)⁻¹ • generic S.1 = S := by
rw [generic_on_AF, smul_smul, inv_mul_cancel h, one_smul]
/-- The construction of a `Sol` from a `QuadSol` in the case when `α₁ S = 0` and `α₂ S = 0`. -/
def special (S : (PlusU1 n).QuadSols) (a b : ℚ) (h1 : α₁ S = 0) (h2 : α₂ S = 0) :
(PlusU1 n).Sols :=
quadToAF (BL.addQuad S a b) (cube_α₁_α₂_zero S a b h1 h2)
lemma special_on_AF (S : (PlusU1 n).Sols) (h1 : α₁ S.1 = 0) :
special S.1 1 0 h1 (α₂_AF S) = S := by
apply ACCSystem.Sols.ext
change (BL.addQuad S.1 1 0).val = _
rw [BL.addQuad_zero]
simp
end QuadSolToSol
open QuadSolToSol
/-- A map from `QuadSols × ℚ × ℚ` to `Sols` taking account of the special and generic cases.
We will show that this map is a surjection. -/
def quadSolToSol {n : ℕ} : (PlusU1 n).QuadSols × ℚ × ℚ → (PlusU1 n).Sols := fun S =>
if h1 : α₁ S.1 = 0 ∧ α₂ S.1 = 0 then
special S.1 S.2.1 S.2.2 h1.1 h1.2
else
S.2.1 • generic S.1
/-- A map from `Sols` to `QuadSols × ℚ × ℚ` which forms a right-inverse to `quadSolToSol`, as
shown in `quadSolToSolInv_rightInverse`. -/
def quadSolToSolInv {n : ℕ} : (PlusU1 n).Sols → (PlusU1 n).QuadSols × ℚ × ℚ :=
fun S =>
if α₁ S.1 = 0 then
(S.1, 1, 0)
else
(S.1, (α₁ S.1)⁻¹, 0)
lemma quadSolToSolInv_1 (S : (PlusU1 n).Sols) :
(quadSolToSolInv S).1 = S.1 := by
simp [quadSolToSolInv]
split
rfl
rfl
lemma quadSolToSolInv_α₁_α₂_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 = 0) :
α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0 := by
rw [quadSolToSolInv_1, α₂_AF S, h]
simp
lemma quadSolToSolInv_α₁_α₂_neq_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
¬ (α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0) := by
rw [not_and, quadSolToSolInv_1, α₂_AF S]
intro hn
simp_all
lemma quadSolToSolInv_special (S : (PlusU1 n).Sols) (h : α₁ S.1 = 0) :
special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2
(quadSolToSolInv_α₁_α₂_zero S h).1 (quadSolToSolInv_α₁_α₂_zero S h).2 = S := by
simp [quadSolToSolInv_1]
rw [show (quadSolToSolInv S).2.1 = 1 by rw [quadSolToSolInv, if_pos h]]
rw [show (quadSolToSolInv S).2.2 = 0 by rw [quadSolToSolInv, if_pos h]]
rw [special_on_AF]
lemma quadSolToSolInv_generic (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
(quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1 = S := by
simp [quadSolToSolInv_1]
rw [show (quadSolToSolInv S).2.1 = (α₁ S.1)⁻¹ by rw [quadSolToSolInv, if_neg h]]
rw [generic_on_AF_α₁_ne_zero S h]
lemma quadSolToSolInv_rightInverse : Function.RightInverse (@quadSolToSolInv n) quadSolToSol := by
intro S
by_cases h : α₁ S.1 = 0
rw [quadSolToSol, dif_pos (quadSolToSolInv_α₁_α₂_zero S h)]
exact quadSolToSolInv_special S h
rw [quadSolToSol, dif_neg (quadSolToSolInv_α₁_α₂_neq_zero S h)]
exact quadSolToSolInv_generic S h
theorem quadSolToSol_surjective : Function.Surjective (@quadSolToSol n) :=
Function.RightInverse.surjective quadSolToSolInv_rightInverse
end PlusU1
end SMRHN