Physlib.Particles.StandardModel.AnomalyCancellation.FamilyMaps

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Particles.StandardModel.AnomalyCancellation.Basic

Family maps for the Standard Model ACCs

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

@[expose] public section

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 := byn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Charges⊢ (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
  (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T
    rw [charges_eq_toSpecies_eqn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Charges⊢ ∀ (i : Fin 5),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
    (toSpecies i)
      ((toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Charges⊢ ∀ (i : Fin 5),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
    (toSpecies i)
      ((toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)]n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Charges⊢ ∀ (i : Fin 5),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
    (toSpecies i)
      ((toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)
    intro in:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
  (toSpecies i)
    ((toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)
    rw [map_addn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) +
    (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) +
    (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)]n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) +
    (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)
    rw [toSMSpecies_toSpecies_inv,n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (S + T) =
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) +
    (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (S + T) = (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) T toSMSpecies_toSpecies_inv,n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (S + T) = (f ∘ₗ toSpecies i) S + (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (S + T) = (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) T toSMSpecies_toSpecies_invn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (S + T) = (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) Tn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (S + T) = (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) T]n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (S + T) = (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) T
    rw [map_addn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).ChargesS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) T = (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) TAll goals completed! 🐙]All goals completed! 🐙
  map_smul' a S := byn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Charges⊢ (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
  (RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S
    rw [charges_eq_toSpecies_eqn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Charges⊢ ∀ (i : Fin 5),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
    (toSpecies i) ((RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Charges⊢ ∀ (i : Fin 5),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
    (toSpecies i) ((RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)]n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Charges⊢ ∀ (i : Fin 5),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
    (toSpecies i) ((RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)
    intro in:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
  (toSpecies i) ((RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)
    rw [map_smuln:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
  (RingHom.id ℚ) a • (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
  (RingHom.id ℚ) a • (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)]n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
  (RingHom.id ℚ) a • (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)
    rw [toSMSpecies_toSpecies_inv,n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (a • S) = (RingHom.id ℚ) a • (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (a • S) = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S toSMSpecies_toSpecies_invn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (a • S) = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) Sn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (a • S) = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S]n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ (f ∘ₗ toSpecies i) (a • S) = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S
    rw [map_smuln:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ a • (f ∘ₗ toSpecies i) S = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) Sn:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ a • (f ∘ₗ toSpecies i) S = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S]n:ℕm:ℕf:(SMSpecies n).Charges →ₗ[ℚ] (SMSpecies m).Chargesa:ℚS:(SMCharges n).Chargesi:Fin 5⊢ a • (f ∘ₗ toSpecies i) S = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S
    rflAll goals completed! 🐙

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' _ _ := rfl
  map_smul' _ _ := 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 := bym:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Charges⊢ (fun i => if hi : ↑i < m then (S + T) ⟨↑i, hi⟩ else 0) =
  (fun i => if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + fun i => if hi : ↑i < m then T ⟨↑i, hi⟩ else 0
    funext im:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberCharges⊢ (if hi : ↑i < m then (S + T) ⟨↑i, hi⟩ else 0) =
  ((fun i => if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + fun i => if hi : ↑i < m then T ⟨↑i, hi⟩ else 0) i
    simp only [ACCSystemCharges.chargesAddCommMonoid_add]m:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberCharges⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0
    by_cases hi : i.val < mposm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:↑i < m⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0negm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0
    ·posm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:↑i < m⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0 rw [dif_pos hi,posm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:↑i < m⊢ S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ = (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0All goals completed! 🐙 dif_pos hi,posm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:↑i < m⊢ S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ = S ⟨↑i, hi⟩ + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0All goals completed! 🐙 dif_pos hiposm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:↑i < m⊢ S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ = S ⟨↑i, hi⟩ + T ⟨↑i, hi⟩All goals completed! 🐙]All goals completed! 🐙
    ·negm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0 rw [dif_neg hi,negm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0negm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0 dif_neg hi,negm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0negm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0 dif_neg hinegm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0negm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0]negm:ℕn:ℕS:(SMSpecies m).ChargesT:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0
      with_unfolding_all rflAll goals completed! 🐙
  map_smul' a S := bym:ℕn:ℕa:ℚS:(SMSpecies m).Charges⊢ (fun i => if hi : ↑i < m then (a • S) ⟨↑i, hi⟩ else 0) =
  (RingHom.id ℚ) a • fun i => if hi : ↑i < m then S ⟨↑i, hi⟩ else 0
    funext im:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberCharges⊢ (if hi : ↑i < m then (a • S) ⟨↑i, hi⟩ else 0) = ((RingHom.id ℚ) a • fun i => if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) i
    simp only [HSMul.hSMul, ACCSystemCharges.chargesModule_smul, eq_ratCast, Rat.cast_eq_id, id_eq]m:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberCharges⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0
    by_cases hi : i.val < mposm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:↑i < m⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0negm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0
    ·posm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:↑i < m⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0 rw [dif_pos hi,posm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:↑i < m⊢ a * S ⟨↑i, ⋯⟩ = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0All goals completed! 🐙 dif_pos hiposm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:↑i < m⊢ a * S ⟨↑i, ⋯⟩ = a * S ⟨↑i, hi⟩All goals completed! 🐙]All goals completed! 🐙
    ·negm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0 rw [dif_neg hi,negm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0negm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * 0 dif_neg hinegm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * 0negm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * 0]negm:ℕn:ℕa:ℚS:(SMSpecies m).Chargesi:Fin (SMSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * 0
      exact Eq.symm (Rat.mul_zero a)All goals completed! 🐙

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 embedding of the 1-family charges into the n-family charges in a universal manner.

@[simps!]
def speciesFamilyUniversial (n : ℕ) :
    (SMSpecies 1).Charges →ₗ[ℚ] (SMSpecies n).Charges where
  toFun S _ := S ⟨0, Nat.zero_lt_succ 0⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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

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