diff --git a/HepLean.lean b/HepLean.lean index 55353f1..e6c9326 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean new file mode 100644 index 0000000..9d06fc7 --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean new file mode 100644 index 0000000..91786d7 --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean @@ -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 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..5de3e2d --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean @@ -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 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 diff --git a/HepLean/AnomalyCancellation/SMNu/Permutations.lean b/HepLean/AnomalyCancellation/SMNu/Permutations.lean new file mode 100644 index 0000000..2d05f3a --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/Permutations.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean new file mode 100644 index 0000000..fc7ef5b --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean @@ -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 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 diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean new file mode 100644 index 0000000..9c3ef17 --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean new file mode 100644 index 0000000..36c528d --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean new file mode 100644 index 0000000..e938e7f --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean @@ -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