Merge branch 'master' into AnomalyCancellation/MSSM
This commit is contained in:
jstoobysmith
commit
c13a474330
8 changed files with 1107 additions and 1 deletions
318
HepLean/AnomalyCancellation/SM/Basic.lean
Normal file
318
HepLean/AnomalyCancellation/SM/Basic.lean
Normal file
|
|
@ -0,0 +1,318 @@
|
|||
/-
|
||||
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.
|
||||
|
||||
We define the ACC system for the Standard Model with`n`-famlies and no RHN.
|
||||
|
||||
-/
|
||||
|
||||
universe v u
|
||||
open Nat
|
||||
open BigOperators
|
||||
|
||||
/-- Aassociate to each (including RHN) SM fermion a set of charges-/
|
||||
@[simps!]
|
||||
def SMCharges (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk (5 * n)
|
||||
|
||||
/-- The vector space associated with a single species of fermions. -/
|
||||
@[simps!]
|
||||
def SMSpecies (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk n
|
||||
|
||||
namespace SMCharges
|
||||
|
||||
variable {n : ℕ}
|
||||
|
||||
/-- An equivalence between the set `(SMCharges n).charges` and the set
|
||||
`(Fin 5 → Fin n → ℚ)`. -/
|
||||
@[simps!]
|
||||
def toSpeciesEquiv : (SMCharges n).charges ≃ (Fin 5 → Fin n → ℚ) :=
|
||||
((Equiv.curry _ _ _).symm.trans ((@finProdFinEquiv 5 n).arrowCongr (Equiv.refl ℚ))).symm
|
||||
|
||||
/-- For a given `i ∈ Fin 5`, the projection of a charge onto that species. -/
|
||||
@[simps!]
|
||||
def toSpecies (i : Fin 5) : (SMCharges n).charges →ₗ[ℚ] (SMSpecies n).charges where
|
||||
toFun S := toSpeciesEquiv S i
|
||||
map_add' _ _ := by aesop
|
||||
map_smul' _ _ := by aesop
|
||||
|
||||
lemma charges_eq_toSpecies_eq (S T : (SMCharges 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 5) (f : (Fin 5 → Fin n → ℚ) ) :
|
||||
(toSpecies i) (toSpeciesEquiv.symm f) = f i := by
|
||||
change (toSpeciesEquiv ∘ toSpeciesEquiv.symm ) _ i= f i
|
||||
simp
|
||||
|
||||
/-- 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
|
||||
|
||||
end SMCharges
|
||||
|
||||
namespace SMACCs
|
||||
|
||||
open SMCharges
|
||||
|
||||
variable {n : ℕ}
|
||||
|
||||
/-- The gravitational anomaly equation. -/
|
||||
@[simp]
|
||||
def accGrav : (SMCharges 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)
|
||||
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
|
||||
|
||||
/-- Extensionality lemma for `accGrav`. -/
|
||||
lemma accGrav_ext {S T : (SMCharges n).charges}
|
||||
(hj : ∀ (j : Fin 5), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
|
||||
accGrav S = accGrav T := by
|
||||
simp only [accGrav, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk]
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
repeat erw [hj]
|
||||
rfl
|
||||
|
||||
/-- The `SU(2)` anomaly equation. -/
|
||||
@[simp]
|
||||
def accSU2 : (SMCharges 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
|
||||
|
||||
/-- Extensionality lemma for `accSU2`. -/
|
||||
lemma accSU2_ext {S T : (SMCharges n).charges}
|
||||
(hj : ∀ (j : Fin 5), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
|
||||
accSU2 S = accSU2 T := by
|
||||
simp only [accSU2, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk]
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
repeat erw [hj]
|
||||
rfl
|
||||
|
||||
/-- The `SU(3)` anomaly equations. -/
|
||||
@[simp]
|
||||
def accSU3 : (SMCharges 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
|
||||
|
||||
/-- Extensionality lemma for `accSU3`. -/
|
||||
lemma accSU3_ext {S T : (SMCharges n).charges}
|
||||
(hj : ∀ (j : Fin 5), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
|
||||
accSU3 S = accSU3 T := by
|
||||
simp only [accSU3, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk]
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
repeat erw [hj]
|
||||
rfl
|
||||
|
||||
/-- The `Y²` anomaly equation. -/
|
||||
@[simp]
|
||||
def accYY : (SMCharges 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
|
||||
|
||||
/-- Extensionality lemma for `accYY`. -/
|
||||
lemma accYY_ext {S T : (SMCharges n).charges}
|
||||
(hj : ∀ (j : Fin 5), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
|
||||
accYY S = accYY T := by
|
||||
simp only [accYY, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk]
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
repeat erw [hj]
|
||||
rfl
|
||||
|
||||
/-- The quadratic bilinear map. -/
|
||||
@[simps!]
|
||||
def quadBiLin : BiLinearSymm (SMCharges 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 [SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
|
||||
/-- The quadratic anomaly cancellation condition. -/
|
||||
@[simp]
|
||||
def accQuad : HomogeneousQuadratic (SMCharges n).charges :=
|
||||
(@quadBiLin n).toHomogeneousQuad
|
||||
|
||||
/-- Extensionality lemma for `accQuad`. -/
|
||||
lemma accQuad_ext {S T : (SMCharges 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
|
||||
simp only [accQuad, BiLinearSymm.toHomogeneousQuad_toFun, Fin.isValue]
|
||||
erw [← quadBiLin.toFun_eq_coe]
|
||||
rw [quadBiLin]
|
||||
simp only
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
ring_nf
|
||||
erw [h 0, h 1, h 2, h 3, h 4]
|
||||
rfl
|
||||
|
||||
/-- The trilinear function defining the cubic. -/
|
||||
@[simps!]
|
||||
def cubeTriLin : TriLinearSymm (SMCharges 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)))
|
||||
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 [SMSpecies_numberCharges, toSpecies_apply, Fin.isValue]
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
swap₂' S T L := by
|
||||
simp only [SMSpecies_numberCharges, toSpecies_apply, Fin.isValue]
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
|
||||
/-- The cubic acc. -/
|
||||
@[simp]
|
||||
def accCube : HomogeneousCubic (SMCharges n).charges := cubeTriLin.toCubic
|
||||
|
||||
/-- Extensionality lemma for `accCube`. -/
|
||||
lemma accCube_ext {S T : (SMCharges 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
|
||||
simp only [accCube, TriLinearSymm.toCubic_toFun, Fin.isValue]
|
||||
erw [← cubeTriLin.toFun_eq_coe]
|
||||
rw [cubeTriLin]
|
||||
simp only
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
ring_nf
|
||||
have h1 : ∀ j, ∑ i, (toSpecies j S i)^3 = ∑ i, (toSpecies j T i)^3 := by
|
||||
intro j
|
||||
erw [h]
|
||||
rfl
|
||||
repeat rw [h1]
|
||||
|
||||
|
||||
end SMACCs
|
||||
106
HepLean/AnomalyCancellation/SM/FamilyMaps.lean
Normal file
106
HepLean/AnomalyCancellation/SM/FamilyMaps.lean
Normal file
|
|
@ -0,0 +1,106 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.AnomalyCancellation.SM.Basic
|
||||
/-!
|
||||
# Family maps for the Standard Model ACCs
|
||||
|
||||
We define the a series of maps between the charges for different numbers of famlies.
|
||||
|
||||
-/
|
||||
|
||||
universe v u
|
||||
|
||||
namespace SM
|
||||
open SMCharges
|
||||
open SMACCs
|
||||
open BigOperators
|
||||
|
||||
/-- Given a map of for a generic species, the corresponding map for charges. -/
|
||||
@[simps!]
|
||||
def chargesMapOfSpeciesMap {n m : ℕ} (f : (SMSpecies n).charges →ₗ[ℚ] (SMSpecies m).charges) :
|
||||
(SMCharges n).charges →ₗ[ℚ] (SMCharges 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
|
||||
|
||||
/-- The projection of the `m`-family charges onto the first `n`-family charges for species. -/
|
||||
@[simps!]
|
||||
def speciesFamilyProj {m n : ℕ} (h : n ≤ m) :
|
||||
(SMSpecies m).charges →ₗ[ℚ] (SMSpecies 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) : (SMCharges m).charges →ₗ[ℚ] (SMCharges 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 : ℕ) :
|
||||
(SMSpecies m).charges →ₗ[ℚ] (SMSpecies 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 [SMSpecies_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 : ℕ) : (SMCharges m).charges →ₗ[ℚ] (SMCharges 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 : ℕ) :
|
||||
(SMSpecies 1).charges →ₗ[ℚ] (SMSpecies 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 : ℕ) : (SMCharges 1).charges →ₗ[ℚ] (SMCharges n).charges :=
|
||||
chargesMapOfSpeciesMap (speciesFamilyUniversial n)
|
||||
|
||||
end SM
|
||||
95
HepLean/AnomalyCancellation/SM/NoGrav/Basic.lean
Normal file
95
HepLean/AnomalyCancellation/SM/NoGrav/Basic.lean
Normal file
|
|
@ -0,0 +1,95 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.AnomalyCancellation.SM.Basic
|
||||
/-!
|
||||
# Anomaly Cancellation in the Standard Model without Gravity
|
||||
|
||||
This file defines the system of anaomaly equations for the SM without RHN, and
|
||||
without the gravitational ACC.
|
||||
|
||||
-/
|
||||
universe v u
|
||||
|
||||
namespace SM
|
||||
open SMCharges
|
||||
open SMACCs
|
||||
open BigOperators
|
||||
|
||||
/-- The ACC system for the standard model without RHN and without the gravitational ACC. -/
|
||||
@[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 `AnomalyFreeLinear`. -/
|
||||
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 `AnomalyFreeLinear` which satisfies the quadratic ACCs
|
||||
gives us a element of `AnomalyFreeQuad`. -/
|
||||
def linearToQuad (S : (SMNoGrav n).LinSols) : (SMNoGrav n).QuadSols :=
|
||||
⟨S, by
|
||||
intro i
|
||||
exact Fin.elim0 i⟩
|
||||
|
||||
/-- An element of `AnomalyFreeQuad` which satisfies the quadratic ACCs
|
||||
gives us a element of `AnomalyFree`. -/
|
||||
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 `AnomalyFreeQuad`. -/
|
||||
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 `AnomalyFree`. -/
|
||||
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 `AnomalyFreeLinear` which satisfies the quadratic and cubic ACCs
|
||||
gives us a element of `AnomalyFree`. -/
|
||||
def linearToAF (S : (SMNoGrav n).LinSols)
|
||||
(hc : accCube S.val = 0) : (SMNoGrav n).Sols :=
|
||||
quadToAF (linearToQuad S) hc
|
||||
|
||||
end SMNoGrav
|
||||
|
||||
end SM
|
||||
78
HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
Normal file
78
HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
Normal file
|
|
@ -0,0 +1,78 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.AnomalyCancellation.SM.Basic
|
||||
import HepLean.AnomalyCancellation.SM.NoGrav.Basic
|
||||
import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
|
||||
/-!
|
||||
# Lemmas for 1 family SM Accs
|
||||
|
||||
The main result of this file is the conclusion of this paper:
|
||||
https://arxiv.org/abs/1907.00514
|
||||
|
||||
That eveery solution to the ACCs without gravity satifies for free the gravitational anomaly.
|
||||
-/
|
||||
|
||||
universe v u
|
||||
namespace SM
|
||||
namespace SMNoGrav
|
||||
namespace One
|
||||
|
||||
open SMCharges
|
||||
open SMACCs
|
||||
open BigOperators
|
||||
|
||||
|
||||
lemma E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : Q S.val (0 : Fin 1) = 0 ↔
|
||||
E S.val (0 : Fin 1) = 0 := by
|
||||
let S' := linearParameters.bijection.symm S.1.1
|
||||
have hC := cubeSol S
|
||||
have hS' := congrArg (fun S => S.val) (linearParameters.bijection.right_inv S.1.1)
|
||||
change S'.asCharges = S.val at hS'
|
||||
rw [← hS'] at hC
|
||||
apply Iff.intro
|
||||
intro hQ
|
||||
exact S'.cubic_zero_Q'_zero hC hQ
|
||||
intro hE
|
||||
exact S'.cubic_zero_E'_zero hC hE
|
||||
|
||||
|
||||
|
||||
lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) :
|
||||
accGrav S.val = 0 := by
|
||||
rw [accGrav]
|
||||
simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
erw [hQ, E_zero_iff_Q_zero.mp hQ]
|
||||
have h1 := SU2Sol S.1.1
|
||||
have h2 := SU3Sol S.1.1
|
||||
simp only [accSU2, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk, accSU3] at h1 h2
|
||||
erw [hQ] at h1 h2
|
||||
simp_all
|
||||
linear_combination 3 * h2
|
||||
|
||||
lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0) :
|
||||
accGrav S.val = 0 := by
|
||||
have hE := E_zero_iff_Q_zero.mpr.mt hQ
|
||||
let S' := linearParametersQENeqZero.bijection.symm ⟨S.1.1, And.intro hQ hE⟩
|
||||
have hC := cubeSol S
|
||||
have hS' := congrArg (fun S => S.val.val)
|
||||
(linearParametersQENeqZero.bijection.right_inv ⟨S.1.1, And.intro hQ hE⟩)
|
||||
change _ = S.val at hS'
|
||||
rw [← hS'] at hC
|
||||
rw [← hS']
|
||||
exact S'.grav_of_cubic hC
|
||||
|
||||
/-- Any solution to the ACCs without gravity satifies the gravitational ACC. -/
|
||||
theorem accGravSatisfied {S : (SMNoGrav 1).Sols} : accGrav S.val = 0 := by
|
||||
by_cases hQ : Q S.val (0 : Fin 1)= 0
|
||||
exact accGrav_Q_zero hQ
|
||||
exact accGrav_Q_neq_zero hQ
|
||||
|
||||
|
||||
end One
|
||||
end SMNoGrav
|
||||
end SM
|
||||
|
|
@ -0,0 +1,380 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.AnomalyCancellation.SM.Basic
|
||||
import HepLean.AnomalyCancellation.SM.NoGrav.Basic
|
||||
import Mathlib.Tactic.FieldSimp
|
||||
import Mathlib.Tactic.Linarith
|
||||
import Mathlib.NumberTheory.FLT.Basic
|
||||
import Mathlib.Algebra.QuadraticDiscriminant
|
||||
/-!
|
||||
# Parameterizations for solutions to the linear ACCs for 1 family
|
||||
|
||||
In this file we give two parameterizations
|
||||
- `linearParameters` of solutions to the linear ACCs for 1 family
|
||||
- `linearParametersQENeqZero` of solutions to the linear ACCs for 1 family with Q and E non-zero
|
||||
|
||||
These parameterizations are based on:
|
||||
https://arxiv.org/abs/1907.00514
|
||||
-/
|
||||
|
||||
universe v u
|
||||
namespace SM
|
||||
namespace SMNoGrav
|
||||
namespace One
|
||||
|
||||
open SMCharges
|
||||
open SMACCs
|
||||
open BigOperators
|
||||
|
||||
/-- The parameters for a linear parameterization to the solution of the linear ACCs. -/
|
||||
structure linearParameters where
|
||||
/-- The parameter `Q'`. -/
|
||||
Q' : ℚ
|
||||
/-- The parameter `Y`. -/
|
||||
Y : ℚ
|
||||
/-- The parameter `E'`. -/
|
||||
E' : ℚ
|
||||
|
||||
namespace linearParameters
|
||||
|
||||
@[ext]
|
||||
lemma ext {S T : linearParameters} (hQ : S.Q' = T.Q') (hY : S.Y = T.Y) (hE : S.E' = T.E') :
|
||||
S = T := by
|
||||
cases' S
|
||||
simp_all only
|
||||
|
||||
/-- The map from the linear paramaters to elements of `(SMNoGrav 1).charges`. -/
|
||||
@[simp]
|
||||
def asCharges (S : linearParameters) : (SMNoGrav 1).charges := fun i =>
|
||||
match i with
|
||||
| (0 : Fin 5) => S.Q'
|
||||
| (1 : Fin 5) => S.Y - S.Q'
|
||||
| (2 : Fin 5) => - (S.Y + S.Q')
|
||||
| (3: Fin 5) => - 3 * S.Q'
|
||||
| (4 : Fin 5) => S.E'
|
||||
|
||||
lemma speciesVal (S : linearParameters) :
|
||||
(toSpecies i) S.asCharges (0 : Fin 1) = S.asCharges i := by
|
||||
match i with
|
||||
| 0 => rfl
|
||||
| 1 => rfl
|
||||
| 2 => rfl
|
||||
| 3 => rfl
|
||||
| 4 => rfl
|
||||
|
||||
/-- The map from the linear paramaters to elements of `(SMNoGrav 1).LinSols`. -/
|
||||
def asLinear (S : linearParameters) : (SMNoGrav 1).LinSols :=
|
||||
chargeToLinear S.asCharges (by
|
||||
simp only [accSU2, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Fin.isValue, Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
erw [speciesVal, speciesVal]
|
||||
simp)
|
||||
(by
|
||||
simp only [accSU3, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Fin.isValue, Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
repeat erw [speciesVal]
|
||||
simp only [asCharges, neg_add_rev]
|
||||
ring)
|
||||
|
||||
lemma asLinear_val (S : linearParameters) : S.asLinear.val = S.asCharges := by
|
||||
rfl
|
||||
|
||||
lemma cubic (S : linearParameters) :
|
||||
accCube (S.asCharges) = - 54 * S.Q'^3 - 18 * S.Q' * S.Y ^ 2 + S.E'^3 := by
|
||||
simp only [accCube, TriLinearSymm.toCubic_toFun, Finset.univ_unique,
|
||||
Fin.default_eq_zero, Fin.isValue, asCharges, SMNoGrav_numberCharges, neg_add_rev, neg_mul,
|
||||
Finset.sum_singleton]
|
||||
erw [← TriLinearSymm.toFun_eq_coe]
|
||||
rw [cubeTriLin]
|
||||
simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton]
|
||||
repeat erw [speciesVal]
|
||||
simp only [asCharges, neg_add_rev, neg_mul, mul_neg, neg_neg]
|
||||
ring
|
||||
|
||||
lemma cubic_zero_Q'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
|
||||
(h : S.Q' = 0) : S.E' = 0 := by
|
||||
rw [cubic, h] at hc
|
||||
simp at hc
|
||||
exact hc
|
||||
|
||||
lemma cubic_zero_E'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
|
||||
(h : S.E' = 0) : S.Q' = 0 := by
|
||||
rw [cubic, h] at hc
|
||||
simp at hc
|
||||
have h1 : -(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = - 18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q' := by
|
||||
ring
|
||||
rw [h1] at hc
|
||||
simp at hc
|
||||
cases' hc with hc hc
|
||||
have h2 := (add_eq_zero_iff' (by nlinarith) (by nlinarith)).mp hc
|
||||
simp at h2
|
||||
exact h2.1
|
||||
exact hc
|
||||
|
||||
/-- The bijection between the type of linear parameters and `(SMNoGrav 1).LinSols`. -/
|
||||
def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
|
||||
toFun S := S.asLinear
|
||||
invFun S := ⟨SMCharges.Q S.val (0 : Fin 1), (SMCharges.U S.val (0 : Fin 1) -
|
||||
SMCharges.D S.val (0 : Fin 1))/2 ,
|
||||
SMCharges.E S.val (0 : Fin 1)⟩
|
||||
left_inv S := by
|
||||
apply linearParameters.ext
|
||||
simp only [Fin.isValue, toSpecies_apply]
|
||||
repeat erw [speciesVal]
|
||||
rfl
|
||||
repeat erw [speciesVal]
|
||||
simp only [Fin.isValue]
|
||||
repeat erw [speciesVal]
|
||||
simp only [asCharges, neg_add_rev]
|
||||
ring
|
||||
simp only [toSpecies_apply]
|
||||
repeat erw [speciesVal]
|
||||
rfl
|
||||
right_inv S := by
|
||||
simp only [Fin.isValue, toSpecies_apply]
|
||||
apply ACCSystemLinear.LinSols.ext
|
||||
rw [charges_eq_toSpecies_eq]
|
||||
intro i
|
||||
rw [asLinear_val]
|
||||
funext j
|
||||
have hj : j = (0 : Fin 1):= by
|
||||
simp only [Fin.isValue]
|
||||
ext
|
||||
simp
|
||||
subst hj
|
||||
erw [speciesVal]
|
||||
have h1 := SU3Sol S
|
||||
simp at h1
|
||||
have h2 := SU2Sol S
|
||||
simp at h2
|
||||
match i with
|
||||
| 0 => rfl
|
||||
| 1 =>
|
||||
field_simp
|
||||
linear_combination -(1 * h1)
|
||||
| 2 =>
|
||||
field_simp
|
||||
linear_combination -(1 * h1)
|
||||
| 3 =>
|
||||
field_simp
|
||||
linear_combination -(1 * h2)
|
||||
| 4 => rfl
|
||||
|
||||
/-- The bijection between the linear parameters and `(SMNoGrav 1).LinSols` in the special
|
||||
case when Q and E are both not zero. -/
|
||||
def bijectionQEZero : {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0} ≃
|
||||
{S : (SMNoGrav 1).LinSols // Q S.val (0 : Fin 1) ≠ 0 ∧ E S.val (0 : Fin 1) ≠ 0} where
|
||||
toFun S := ⟨bijection S, S.2⟩
|
||||
invFun S := ⟨bijection.symm S, S.2⟩
|
||||
left_inv S := by
|
||||
apply Subtype.ext
|
||||
exact bijection.left_inv S.1
|
||||
right_inv S := by
|
||||
apply Subtype.ext
|
||||
exact bijection.right_inv S.1
|
||||
|
||||
lemma grav (S : linearParameters) :
|
||||
accGrav S.asCharges = 0 ↔ S.E' = 6 * S.Q' := by
|
||||
rw [accGrav]
|
||||
simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
repeat erw [speciesVal]
|
||||
simp only [asCharges, neg_add_rev, neg_mul, mul_neg]
|
||||
ring_nf
|
||||
rw [add_comm, add_eq_zero_iff_eq_neg]
|
||||
simp
|
||||
|
||||
end linearParameters
|
||||
|
||||
|
||||
/-- The parameters for solutions to the linear ACCs with the condition that Q and E are non-zero.-/
|
||||
structure linearParametersQENeqZero where
|
||||
/-- The parameter `x`. -/
|
||||
x : ℚ
|
||||
/-- The parameter `v`. -/
|
||||
v : ℚ
|
||||
/-- The parameter `w`. -/
|
||||
w : ℚ
|
||||
hx : x ≠ 0
|
||||
hvw : v + w ≠ 0
|
||||
|
||||
namespace linearParametersQENeqZero
|
||||
|
||||
@[ext]
|
||||
lemma ext {S T : linearParametersQENeqZero} (hx : S.x = T.x) (hv : S.v = T.v)
|
||||
(hw : S.w = T.w) : S = T := by
|
||||
cases' S
|
||||
simp_all only
|
||||
|
||||
/-- A map from `linearParametersQENeqZero` to `linearParameters`. -/
|
||||
@[simps!]
|
||||
def toLinearParameters (S : linearParametersQENeqZero) :
|
||||
{S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0} :=
|
||||
⟨⟨S.x, 3 * S.x * (S.v - S.w) / (S.v + S.w), - 6 * S.x / (S.v + S.w)⟩,
|
||||
by
|
||||
apply And.intro S.hx
|
||||
simp only [neg_mul, ne_eq, div_eq_zero_iff, neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero,
|
||||
false_or]
|
||||
rw [not_or]
|
||||
exact And.intro S.hx S.hvw⟩
|
||||
|
||||
/-- A map from `linearParameters` to `linearParametersQENeqZero` in the special case when
|
||||
`Q'` and `E'` of the linear parameters are non-zero. -/
|
||||
@[simps!]
|
||||
def tolinearParametersQNeqZero (S : {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0}) :
|
||||
linearParametersQENeqZero :=
|
||||
⟨S.1.Q', - (3 * S.1.Q' + S.1.Y) / S.1.E', - (3 * S.1.Q' - S.1.Y)/ S.1.E', S.2.1,
|
||||
by
|
||||
simp only [ne_eq, neg_add_rev, neg_sub]
|
||||
field_simp
|
||||
rw [not_or]
|
||||
ring_nf
|
||||
simp only [neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero, or_false]
|
||||
exact S.2⟩
|
||||
|
||||
/-- A bijection between the type `linearParametersQENeqZero` and linear parameters
|
||||
with `Q'` and `E'` non-zero. -/
|
||||
@[simps!]
|
||||
def bijectionLinearParameters :
|
||||
linearParametersQENeqZero ≃ {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0} where
|
||||
toFun := toLinearParameters
|
||||
invFun := tolinearParametersQNeqZero
|
||||
left_inv S := by
|
||||
have hvw := S.hvw
|
||||
have hQ := S.hx
|
||||
apply linearParametersQENeqZero.ext
|
||||
simp only [tolinearParametersQNeqZero_x, toLinearParameters_coe_Q']
|
||||
field_simp
|
||||
ring
|
||||
simp only [tolinearParametersQNeqZero_w, toLinearParameters_coe_Y, toLinearParameters_coe_Q',
|
||||
toLinearParameters_coe_E']
|
||||
field_simp
|
||||
ring
|
||||
right_inv S := by
|
||||
apply Subtype.ext
|
||||
have hQ := S.2.1
|
||||
have hE := S.2.2
|
||||
apply linearParameters.ext
|
||||
simp only [ne_eq, toLinearParameters_coe_Q', tolinearParametersQNeqZero_x]
|
||||
field_simp
|
||||
ring_nf
|
||||
field_simp [hQ, hE]
|
||||
ring
|
||||
field_simp
|
||||
ring_nf
|
||||
field_simp [hQ, hE]
|
||||
ring
|
||||
|
||||
/-- The bijection between `linearParametersQENeqZero` and `LinSols` with `Q` and `E` non-zero. -/
|
||||
def bijection : linearParametersQENeqZero ≃
|
||||
{S : (SMNoGrav 1).LinSols // Q S.val (0 : Fin 1) ≠ 0 ∧ E S.val (0 : Fin 1) ≠ 0} :=
|
||||
bijectionLinearParameters.trans (linearParameters.bijectionQEZero)
|
||||
|
||||
lemma cubic (S : linearParametersQENeqZero) :
|
||||
accCube (bijection S).1.val = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1 := by
|
||||
erw [linearParameters.cubic]
|
||||
simp only [ne_eq, bijectionLinearParameters_apply_coe_Q', neg_mul,
|
||||
bijectionLinearParameters_apply_coe_Y, div_pow, bijectionLinearParameters_apply_coe_E']
|
||||
have hvw := S.hvw
|
||||
have hQ := S.hx
|
||||
field_simp
|
||||
have h1 : (-(54 * S.x ^ 3 * (S.v + S.w) ^ 2) - 18 * S.x * (3 * S.x * (S.v - S.w)) ^ 2) *
|
||||
(S.v + S.w) ^ 3 + (-(6 * S.x)) ^ 3 * (S.v + S.w) ^ 2 =
|
||||
- 216 * S.x ^3 * (S.v ^3 + S.w ^3 +1) * (S.v + S.w) ^ 2 := by
|
||||
ring
|
||||
rw [h1]
|
||||
simp_all
|
||||
rw [add_eq_zero_iff_eq_neg]
|
||||
|
||||
lemma FLTThree : FermatLastTheoremWith ℚ 3 := by sorry
|
||||
|
||||
lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) :
|
||||
S.v = 0 ∨ S.w = 0 := by
|
||||
rw [S.cubic] at h
|
||||
have h1 : (-1)^3 = (-1 : ℚ):= by rfl
|
||||
rw [← h1] at h
|
||||
by_contra hn
|
||||
simp [not_or] at hn
|
||||
have h2 := FLTThree S.v S.w (-1) hn.1 hn.2 (by simp)
|
||||
simp_all
|
||||
|
||||
lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
|
||||
(hv : S.v = 0 ) : S.w = -1 := by
|
||||
rw [S.cubic, hv] at h
|
||||
simp at h
|
||||
have h' : (S.w + 1) * (1 * S.w * S.w + (-1) * S.w + 1) = 0 := by
|
||||
ring_nf
|
||||
rw [add_comm]
|
||||
exact add_eq_zero_iff_eq_neg.mpr h
|
||||
have h'' : (1 * S.w * S.w + (-1) * S.w + 1) ≠ 0 := by
|
||||
refine quadratic_ne_zero_of_discrim_ne_sq ?_ S.w
|
||||
intro s
|
||||
by_contra hn
|
||||
have h : s ^ 2 < 0 := by
|
||||
rw [← hn]
|
||||
simp [discrim]
|
||||
nlinarith
|
||||
simp_all
|
||||
linear_combination h'
|
||||
|
||||
lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
|
||||
(hw : S.w = 0 ) : S.v = -1 := by
|
||||
rw [S.cubic, hw] at h
|
||||
simp at h
|
||||
have h' : (S.v + 1) * (1 * S.v * S.v + (-1) * S.v + 1) = 0 := by
|
||||
ring_nf
|
||||
rw [add_comm]
|
||||
exact add_eq_zero_iff_eq_neg.mpr h
|
||||
have h'' : (1 * S.v * S.v + (-1) * S.v + 1) ≠ 0 := by
|
||||
refine quadratic_ne_zero_of_discrim_ne_sq ?_ S.v
|
||||
intro s
|
||||
by_contra hn
|
||||
have h : s ^ 2 < 0 := by
|
||||
rw [← hn]
|
||||
simp [discrim]
|
||||
nlinarith
|
||||
simp_all
|
||||
linear_combination h'
|
||||
|
||||
lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) :
|
||||
(S.v = -1 ∧ S.w = 0) ∨ (S.v = 0 ∧ S.w = -1) := by
|
||||
have h' := cubic_v_or_w_zero S h
|
||||
cases' h' with hx hx
|
||||
simp [hx]
|
||||
exact cubic_v_zero S h hx
|
||||
simp [hx]
|
||||
exact cube_w_zero S h hx
|
||||
|
||||
lemma grav (S : linearParametersQENeqZero) : accGrav (bijection S).1.val = 0 ↔ S.v + S.w = -1 := by
|
||||
erw [linearParameters.grav]
|
||||
have hvw := S.hvw
|
||||
have hQ := S.hx
|
||||
field_simp
|
||||
apply Iff.intro
|
||||
intro h
|
||||
apply (mul_right_inj' hQ).mp
|
||||
linear_combination -1 * h / 6
|
||||
intro h
|
||||
rw [h]
|
||||
ring
|
||||
|
||||
lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) :
|
||||
accGrav (bijection S).1.val = 0 := by
|
||||
rw [grav]
|
||||
have h' := cube_w_v S h
|
||||
cases' h' with h h
|
||||
rw [h.1, h.2]
|
||||
simp only [add_zero]
|
||||
rw [h.1, h.2]
|
||||
simp
|
||||
|
||||
end linearParametersQENeqZero
|
||||
|
||||
|
||||
end One
|
||||
end SMNoGrav
|
||||
end SM
|
||||
122
HepLean/AnomalyCancellation/SM/Permutations.lean
Normal file
122
HepLean/AnomalyCancellation/SM/Permutations.lean
Normal file
|
|
@ -0,0 +1,122 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.AnomalyCancellation.SM.Basic
|
||||
import Mathlib.Tactic.Polyrith
|
||||
import HepLean.AnomalyCancellation.GroupActions
|
||||
/-!
|
||||
# Permutations of SM with no RHN.
|
||||
|
||||
We define the group of permutations for the SM charges with no RHN.
|
||||
|
||||
-/
|
||||
|
||||
universe v u
|
||||
|
||||
open Nat
|
||||
open Finset
|
||||
|
||||
namespace SM
|
||||
|
||||
open SMCharges
|
||||
open SMACCs
|
||||
open BigOperators
|
||||
|
||||
/-- The group of `Sₙ` permutations for each species. -/
|
||||
@[simp]
|
||||
def permGroup (n : ℕ) := ∀ (_ : Fin 5), 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) : (SMCharges n).charges →ₗ[ℚ] (SMCharges 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) (SMCharges 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 : (SMCharges n).charges) (j : Fin 5) :
|
||||
toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
|
||||
erw [toSMSpecies_toSpecies_inv]
|
||||
|
||||
|
||||
lemma toSpecies_sum_invariant (m : ℕ) (f : permGroup n) (S : (SMCharges n).charges) (j : Fin 5) :
|
||||
∑ 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 : (SMCharges 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 : (SMCharges 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 : (SMCharges 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 : (SMCharges 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 : (SMCharges n).charges) :
|
||||
accQuad (repCharges f S) = accQuad S :=
|
||||
accQuad_ext
|
||||
(toSpecies_sum_invariant 2 f S)
|
||||
|
||||
lemma accCube_invariant (f : permGroup n) (S : (SMCharges n).charges) :
|
||||
accCube (repCharges f S) = accCube S :=
|
||||
accCube_ext
|
||||
(by simpa using toSpecies_sum_invariant 3 f S)
|
||||
|
||||
end SM
|
||||
Loading…
Add table
Add a link
Reference in a new issue