Family maps for the Standard Model for RHN ACCs

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

def SMRHN.chargesMapOfSpeciesMap {n m : ℕ} (f : (SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Charges) : (SMνCharges n).Charges →ₗ[ℚ] (SMνCharges 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 SMRHN.chargesMapOfSpeciesMap_apply {n m : ℕ} (f : (SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Charges) (S : (SMνCharges n).Charges) : (chargesMapOfSpeciesMap f) S = SMνCharges.toSpeciesEquiv.symm fun (i : Fin 6) => f ((SMνCharges.toSpecies i) S)

theorem SMRHN.chargesMapOfSpeciesMap_toSpecies {n m : ℕ} (f : (SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Charges) (S : (SMνCharges n).Charges) (j : Fin 6) : (SMνCharges.toSpecies j) ((chargesMapOfSpeciesMap f) S) = (f ∘ₗ SMνCharges.toSpecies j) S

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

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

Equations

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

@[simp]

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

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

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

Equations

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

def SMRHN.speciesFamilyUniversial (n : ℕ) : (SMνSpecies 1).Charges →ₗ[ℚ] (SMνSpecies 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 SMRHN.speciesFamilyUniversial_apply (n : ℕ) (S : (SMνSpecies 1).Charges) (x✝ : Fin (SMνSpecies n).numberCharges) : (speciesFamilyUniversial n) S x✝ = S 0

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

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

Equations

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

theorem SMRHN.toSpecies_familyUniversal {n : ℕ} (j : Fin 6) (S : (SMνCharges 1).Charges) (i : Fin n) : (SMνCharges.toSpecies j) ((familyUniversal n) S) i = (SMνCharges.toSpecies j) S ⟨0, ⋯⟩

theorem SMRHN.sum_familyUniversal {n : ℕ} (m : ℕ) (S : (SMνCharges 1).Charges) (j : Fin 6) : ∑ i : Fin (SMνSpecies n).numberCharges, ((fun (a : ℚ) => a ^ m) ∘ (SMνCharges.toSpecies j) ((familyUniversal n) S)) i = ↑n * (SMνCharges.toSpecies j) S ⟨0, ⋯⟩ ^ m

theorem SMRHN.sum_familyUniversal_one {n : ℕ} (S : (SMνCharges 1).Charges) (j : Fin 6) : ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) ((familyUniversal n) S) i = ↑n * (SMνCharges.toSpecies j) S ⟨0, ⋯⟩

theorem SMRHN.sum_familyUniversal_two {n : ℕ} (S : (SMνCharges 1).Charges) (T : (SMνCharges n).Charges) (j : Fin 6) : ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) ((familyUniversal n) S) i * (SMνCharges.toSpecies j) T i = (SMνCharges.toSpecies j) S ⟨0, ⋯⟩ * ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) T i

theorem SMRHN.sum_familyUniversal_three {n : ℕ} (S : (SMνCharges 1).Charges) (T L : (SMνCharges n).Charges) (j : Fin 6) : ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) ((familyUniversal n) S) i * (SMνCharges.toSpecies j) T i * (SMνCharges.toSpecies j) L i = (SMνCharges.toSpecies j) S ⟨0, ⋯⟩ * ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) T i * (SMνCharges.toSpecies j) L i

theorem SMRHN.familyUniversal_accGrav {n : ℕ} (S : (SMνCharges 1).Charges) : SMνACCs.accGrav ((familyUniversal n) S) = ↑n * SMνACCs.accGrav S

theorem SMRHN.familyUniversal_accSU2 {n : ℕ} (S : (SMνCharges 1).Charges) : SMνACCs.accSU2 ((familyUniversal n) S) = ↑n * SMνACCs.accSU2 S

theorem SMRHN.familyUniversal_accSU3 {n : ℕ} (S : (SMνCharges 1).Charges) : SMνACCs.accSU3 ((familyUniversal n) S) = ↑n * SMνACCs.accSU3 S

theorem SMRHN.familyUniversal_accYY {n : ℕ} (S : (SMνCharges 1).Charges) : SMνACCs.accYY ((familyUniversal n) S) = ↑n * SMνACCs.accYY S

theorem SMRHN.familyUniversal_quadBiLin {n : ℕ} (S : (SMνCharges 1).Charges) (T : (SMνCharges n).Charges) : (SMνACCs.quadBiLin ((familyUniversal n) S)) T = S 0 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q T i - 2 * S 1 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U T i + S 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D T i - S 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L T i + S 4 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.E T i

theorem SMRHN.familyUniversal_accQuad {n : ℕ} (S : (SMνCharges 1).Charges) : SMνACCs.accQuad ((familyUniversal n) S) = ↑n * SMνACCs.accQuad S

theorem SMRHN.familyUniversal_cubeTriLin {n : ℕ} (S : (SMνCharges 1).Charges) (T R : (SMνCharges n).Charges) : ((SMνACCs.cubeTriLin ((familyUniversal n) S)) T) R = 6 * S 0 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q T i * SMνCharges.Q R i + 3 * S 1 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U T i * SMνCharges.U R i + 3 * S 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D T i * SMνCharges.D R i + 2 * S 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L T i * SMνCharges.L R i + S 4 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.E T i * SMνCharges.E R i + S 5 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.N T i * SMνCharges.N R i

theorem SMRHN.familyUniversal_cubeTriLin' {n : ℕ} (S T : (SMνCharges 1).Charges) (R : (SMνCharges n).Charges) : ((SMνACCs.cubeTriLin ((familyUniversal n) S)) ((familyUniversal n) T)) R = 6 * S 0 * T 0 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q R i + 3 * S 1 * T 1 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U R i + 3 * S 2 * T 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D R i + 2 * S 3 * T 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L R i + S 4 * T 4 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.E R i + S 5 * T 5 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.N R i

theorem SMRHN.familyUniversal_accCube {n : ℕ} (S : (SMνCharges 1).Charges) : SMνACCs.accCube ((familyUniversal n) S) = ↑n * SMνACCs.accCube S