From 982281b0ffc2b4fff945395b4eb7ab3a38225ca1 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 18 Apr 2024 08:40:46 -0400 Subject: [PATCH] Feat: SMNu basics --- HepLean.lean | 2 + HepLean/AnomalyCancellation/SMNu/Basic.lean | 358 ++++++++++++++++++ .../AnomalyCancellation/SMNu/FamilyMaps.lean | 236 ++++++++++++ .../SMNu/Permutations.lean | 124 ++++++ 4 files changed, 720 insertions(+) create mode 100644 HepLean/AnomalyCancellation/SMNu/Basic.lean create mode 100644 HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean create mode 100644 HepLean/AnomalyCancellation/SMNu/Permutations.lean diff --git a/HepLean.lean b/HepLean.lean index 55353f1..8075639 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -16,3 +16,5 @@ 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 diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean new file mode 100644 index 0000000..edcc91a --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean @@ -0,0 +1,358 @@ +/- +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 + 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 + 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 + 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 + 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 + 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 + ring + swap' S T := by + simp + 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 + 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 + ring + swap₁' S T L := by + simp + apply Fintype.sum_congr + intro i + ring + swap₂' S T L := by + simp + 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..c6eca99 --- /dev/null +++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean @@ -0,0 +1,236 @@ +/- +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 + 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 + 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 + 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 + rw [Finset.mul_sum] + apply Finset.sum_congr + simp + 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 + rw [Finset.mul_sum] + apply Finset.sum_congr + simp + intro i _ + erw [toSpecies_familyUniversal] + simp + 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 + 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 + 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 + 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 + 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 + 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 + 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 + 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 + 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 + ring + +end SMRHN diff --git a/HepLean/AnomalyCancellation/SMNu/Permutations.lean b/HepLean/AnomalyCancellation/SMNu/Permutations.lean new file mode 100644 index 0000000..36878c4 --- /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 : ℕ} + +@[simps!] +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. -/ +@[simps!] +def repCharges {n : ℕ} : Representation ℚ (permGroup n) (SMνCharges n).charges where + toFun f := chargeMap f⁻¹ + map_mul' f g :=by + simp + apply LinearMap.ext + intro S + rw [charges_eq_toSpecies_eq] + intro i + simp + 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