Family maps for the Standard Model ACCs

We define the a series of maps between the charges for different numbers of families.

def SM.chargesMapOfSpeciesMap {n m : ℕ} (f : (SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Charges) : (SMCharges n).Charges →ₗ[ℚ] (SMCharges m).Charges

Given a map of for a generic species, the corresponding map for charges.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SM.chargesMapOfSpeciesMap_apply {n m : ℕ} (f : (SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Charges) (S : (SMCharges n).Charges) : (chargesMapOfSpeciesMap f) S = SMCharges.toSpeciesEquiv.symm fun (i : Fin 5) => f ((SMCharges.toSpecies i) S)

def SM.speciesFamilyProj {m n : ℕ} (h : n ≤ m) : (SMSpecies m).Charges →ₗ[ℚ] (SMSpecies n).Charges

The projection of the m-family charges onto the first n-family charges for species.

Equations

• SM.speciesFamilyProj h = { toFun := fun (S : (SMSpecies m).Charges) => S ∘ Fin.castLE h, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SM.speciesFamilyProj_apply {m n : ℕ} (h : n ≤ m) (S : (SMSpecies m).Charges) (a✝ : Fin (SMSpecies n).numberCharges) : (speciesFamilyProj h) S a✝ = S (Fin.castLE h a✝)

def SM.familyProjection {m n : ℕ} (h : n ≤ m) : (SMCharges m).Charges →ₗ[ℚ] (SMCharges n).Charges

The projection of the m-family charges onto the first n-family charges.

Equations

• SM.familyProjection h = SM.chargesMapOfSpeciesMap (SM.speciesFamilyProj h)

def SM.speciesEmbed (m n : ℕ) : (SMSpecies m).Charges →ₗ[ℚ] (SMSpecies n).Charges

For species, the embedding of the m-family charges onto the n-family charges, with all other charges zero.

Equations

• SM.speciesEmbed m n = { toFun := fun (S : (SMSpecies m).Charges) (i : Fin (SMSpecies n).numberCharges) => if hi : ↑i < m then S ⟨↑i, hi⟩ else 0, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SM.speciesEmbed_apply (m n : ℕ) (S : (SMSpecies m).Charges) (i : Fin (SMSpecies n).numberCharges) : (speciesEmbed m n) S i = if hi : ↑i < m then S ⟨↑i, hi⟩ else 0

def SM.familyEmbedding (m n : ℕ) : (SMCharges m).Charges →ₗ[ℚ] (SMCharges n).Charges

The embedding of the m-family charges onto the n-family charges, with all other charges zero.

Equations

• SM.familyEmbedding m n = SM.chargesMapOfSpeciesMap (SM.speciesEmbed m n)

def SM.speciesFamilyUniversial (n : ℕ) : (SMSpecies 1).Charges →ₗ[ℚ] (SMSpecies n).Charges

For species, the embedding of the 1-family charges into the n-family charges in a universal manner.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SM.speciesFamilyUniversial_apply (n : ℕ) (S : (SMSpecies 1).Charges) (x✝ : Fin (SMSpecies n).numberCharges) : (speciesFamilyUniversial n) S x✝ = S 0

def SM.familyUniversal (n : ℕ) : (SMCharges 1).Charges →ₗ[ℚ] (SMCharges n).Charges

The embedding of the 1-family charges into the n-family charges in a universal manner.

Equations

• SM.familyUniversal n = SM.chargesMapOfSpeciesMap (SM.speciesFamilyUniversial n)