DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update FamilyMaps.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-05-20 00:19:34 +02:00
parent e77dd4b098
commit 1cd9dd3ed4
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
View file

@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SMNu.Basic
/-! /-!
# Family maps for the Standard Model for RHN ACCs # Family maps for the Standard Model for RHN ACCs
We define the a series of maps between the charges for different numbers of famlies. We define the a series of maps between the charges for different numbers of families.
-/ -/
@ -89,7 +89,7 @@ other charges zero. -/
def familyEmbedding (m n : ℕ) : (SMνCharges m).charges →ₗ[ℚ] (SMνCharges n).charges := def familyEmbedding (m n : ℕ) : (SMνCharges m).charges →ₗ[ℚ] (SMνCharges n).charges :=
chargesMapOfSpeciesMap (speciesEmbed m n) chargesMapOfSpeciesMap (speciesEmbed m n)
/-- For species, the embeddding of the `1`-family charges into the `n`-family charges in /-- For species, the embedding of the `1`-family charges into the `n`-family charges in
a universal manor. -/ a universal manor. -/
@[simps!] @[simps!]
def speciesFamilyUniversial (n : ℕ) : def speciesFamilyUniversial (n : ℕ) :
@ -103,7 +103,7 @@ def speciesFamilyUniversial (n : ℕ) :
simp [HSMul.hSMul] simp [HSMul.hSMul]
-- rw [show Rat.cast a = a from rfl] -- rw [show Rat.cast a = a from rfl]
/-- The embeddding of the `1`-family charges into the `n`-family charges in /-- The embedding of the `1`-family charges into the `n`-family charges in
a universal manor. -/ a universal manor. -/
def familyUniversal (n : ℕ) : (SMνCharges 1).charges →ₗ[ℚ] (SMνCharges n).charges := def familyUniversal (n : ℕ) : (SMνCharges 1).charges →ₗ[ℚ] (SMνCharges n).charges :=
chargesMapOfSpeciesMap (speciesFamilyUniversial n) chargesMapOfSpeciesMap (speciesFamilyUniversial n)