refactor: Lint
This commit is contained in:
jstoobysmith
parent
982281b0ff
commit
2ad7fc3cea
4 changed files with 48 additions and 33 deletions
|
|
@ -49,7 +49,7 @@ lemma charges_eq_toSpecies_eq (S T : (SMνCharges n).charges) :
|
|||
apply Iff.intro
|
||||
intro h
|
||||
rw [h]
|
||||
simp
|
||||
simp only [forall_const]
|
||||
intro h
|
||||
apply toSpeciesEquiv.injective
|
||||
funext i
|
||||
|
|
@ -115,7 +115,8 @@ def accGrav : (SMνCharges n).charges →ₗ[ℚ] ℚ where
|
|||
lemma accGrav_decomp (S : (SMνCharges n).charges) :
|
||||
accGrav S = 6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i +
|
||||
∑ i, N S i := by
|
||||
simp
|
||||
simp only [accGrav, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk]
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
|
||||
|
|
@ -148,7 +149,8 @@ def accSU2 : (SMνCharges n).charges →ₗ[ℚ] ℚ where
|
|||
|
||||
lemma accSU2_decomp (S : (SMνCharges n).charges) :
|
||||
accSU2 S = 3 * ∑ i, Q S i + ∑ i, L S i := by
|
||||
simp
|
||||
simp only [accSU2, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk]
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
|
||||
|
|
@ -180,7 +182,8 @@ def accSU3 : (SMνCharges n).charges →ₗ[ℚ] ℚ where
|
|||
|
||||
lemma accSU3_decomp (S : (SMνCharges n).charges) :
|
||||
accSU3 S = 2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i := by
|
||||
simp
|
||||
simp only [accSU3, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk]
|
||||
repeat rw [Finset.sum_add_distrib]
|
||||
repeat rw [← Finset.mul_sum]
|
||||
|
||||
|
|
@ -213,7 +216,8 @@ def accYY : (SMνCharges n).charges →ₗ[ℚ] ℚ where
|
|||
|
||||
lemma accYY_decomp (S : (SMνCharges n).charges) :
|
||||
accYY S = ∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i := by
|
||||
simp
|
||||
simp only [accYY, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk]
|
||||
repeat rw [Finset.sum_add_distrib]
|
||||
repeat rw [← Finset.mul_sum]
|
||||
|
||||
|
|
@ -246,10 +250,11 @@ def quadBiLin : BiLinearSymm (SMνCharges n).charges where
|
|||
apply Fintype.sum_congr
|
||||
intro i
|
||||
repeat erw [map_add]
|
||||
simp
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue, neg_mul,
|
||||
one_mul]
|
||||
ring
|
||||
swap' S T := by
|
||||
simp
|
||||
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
|
|
@ -262,7 +267,7 @@ lemma quadBiLin_decomp (S T : (SMνCharges n).charges) :
|
|||
simp only
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
simp
|
||||
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul, add_left_inj]
|
||||
ring
|
||||
|
||||
/-- The quadratic anomaly cancellation condition. -/
|
||||
|
|
@ -308,15 +313,15 @@ def cubeTriLin : TriLinearSymm (SMνCharges n).charges where
|
|||
apply Fintype.sum_congr
|
||||
intro i
|
||||
repeat erw [map_add]
|
||||
simp
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue]
|
||||
ring
|
||||
swap₁' S T L := by
|
||||
simp
|
||||
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
swap₂' S T L := by
|
||||
simp
|
||||
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
|
|
|
|||
|
|
@ -71,7 +71,7 @@ def speciesEmbed (m n : ℕ) :
|
|||
0
|
||||
map_add' S T := by
|
||||
funext i
|
||||
simp
|
||||
simp only [SMνSpecies_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]
|
||||
|
|
@ -116,13 +116,15 @@ lemma toSpecies_familyUniversal {n : ℕ} (j : Fin 6) (S : (SMνCharges 1).charg
|
|||
lemma sum_familyUniversal {n : ℕ} (m : ℕ) (S : (SMνCharges 1).charges) (j : Fin 6) :
|
||||
∑ i, ((fun a => a ^ m) ∘ toSpecies j (familyUniversal n S)) i =
|
||||
n * (toSpecies j S ⟨0, by simp⟩) ^ m := by
|
||||
simp
|
||||
have h1 : (n : ℚ) * (toSpecies j S ⟨0, by simp⟩) ^ m = ∑ _i : Fin n, (toSpecies j S ⟨0, by simp⟩) ^ m:= by
|
||||
simp only [SMνSpecies_numberCharges, Function.comp_apply, toSpecies_apply, Fin.zero_eta,
|
||||
Fin.isValue]
|
||||
have h1 : (n : ℚ) * (toSpecies j S ⟨0, by simp⟩) ^ m =
|
||||
∑ _i : Fin n, (toSpecies j S ⟨0, by simp⟩) ^ m := by
|
||||
rw [Fin.sum_const]
|
||||
simp
|
||||
erw [h1]
|
||||
apply Finset.sum_congr
|
||||
simp
|
||||
simp only
|
||||
intro i _
|
||||
erw [toSpecies_familyUniversal]
|
||||
|
||||
|
|
@ -134,10 +136,10 @@ lemma sum_familyUniversal_two {n : ℕ} (S : (SMνCharges 1).charges)
|
|||
(T : (SMνCharges n).charges) (j : Fin 6) :
|
||||
∑ i, (toSpecies j (familyUniversal n S) i * toSpecies j T i) =
|
||||
(toSpecies j S ⟨0, by simp⟩) * ∑ i, toSpecies j T i := by
|
||||
simp
|
||||
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.zero_eta, Fin.isValue]
|
||||
rw [Finset.mul_sum]
|
||||
apply Finset.sum_congr
|
||||
simp
|
||||
simp only
|
||||
intro i _
|
||||
erw [toSpecies_familyUniversal]
|
||||
rfl
|
||||
|
|
@ -146,41 +148,45 @@ lemma sum_familyUniversal_three {n : ℕ} (S : (SMνCharges 1).charges)
|
|||
(T L : (SMνCharges n).charges) (j : Fin 6) :
|
||||
∑ i, (toSpecies j (familyUniversal n S) i * toSpecies j T i * toSpecies j L i) =
|
||||
(toSpecies j S ⟨0, by simp⟩) * ∑ i, toSpecies j T i * toSpecies j L i := by
|
||||
simp
|
||||
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.zero_eta, Fin.isValue]
|
||||
rw [Finset.mul_sum]
|
||||
apply Finset.sum_congr
|
||||
simp
|
||||
simp only
|
||||
intro i _
|
||||
erw [toSpecies_familyUniversal]
|
||||
simp
|
||||
simp only [SMνSpecies_numberCharges, Fin.zero_eta, Fin.isValue, toSpecies_apply]
|
||||
ring
|
||||
|
||||
lemma familyUniversal_accGrav (S : (SMνCharges 1).charges) :
|
||||
accGrav (familyUniversal n S) = n * (accGrav S) := by
|
||||
rw [accGrav_decomp, accGrav_decomp]
|
||||
repeat rw [sum_familyUniversal_one]
|
||||
simp
|
||||
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
|
||||
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
|
||||
ring
|
||||
|
||||
lemma familyUniversal_accSU2 (S : (SMνCharges 1).charges) :
|
||||
accSU2 (familyUniversal n S) = n * (accSU2 S) := by
|
||||
rw [accSU2_decomp, accSU2_decomp]
|
||||
repeat rw [sum_familyUniversal_one]
|
||||
simp
|
||||
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
|
||||
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
|
||||
ring
|
||||
|
||||
lemma familyUniversal_accSU3 (S : (SMνCharges 1).charges) :
|
||||
accSU3 (familyUniversal n S) = n * (accSU3 S) := by
|
||||
rw [accSU3_decomp, accSU3_decomp]
|
||||
repeat rw [sum_familyUniversal_one]
|
||||
simp
|
||||
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
|
||||
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
|
||||
ring
|
||||
|
||||
lemma familyUniversal_accYY (S : (SMνCharges 1).charges) :
|
||||
accYY (familyUniversal n S) = n * (accYY S) := by
|
||||
rw [accYY_decomp, accYY_decomp]
|
||||
repeat rw [sum_familyUniversal_one]
|
||||
simp
|
||||
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
|
||||
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
|
||||
ring
|
||||
|
||||
lemma familyUniversal_quadBiLin (S : (SMνCharges 1).charges) (T : (SMνCharges n).charges) :
|
||||
|
|
@ -190,7 +196,8 @@ lemma familyUniversal_quadBiLin (S : (SMνCharges 1).charges) (T : (SMνCharges
|
|||
rw [quadBiLin_decomp]
|
||||
repeat rw [sum_familyUniversal_two]
|
||||
repeat rw [toSpecies_one]
|
||||
simp
|
||||
simp only [Fin.isValue, SMνSpecies_numberCharges, toSpecies_apply, add_left_inj, sub_left_inj,
|
||||
sub_right_inj]
|
||||
ring
|
||||
|
||||
lemma familyUniversal_accQuad (S : (SMνCharges 1).charges) :
|
||||
|
|
@ -198,7 +205,8 @@ lemma familyUniversal_accQuad (S : (SMνCharges 1).charges) :
|
|||
rw [accQuad_decomp]
|
||||
repeat erw [sum_familyUniversal]
|
||||
rw [accQuad_decomp]
|
||||
simp
|
||||
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
|
||||
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
|
||||
ring
|
||||
|
||||
lemma familyUniversal_cubeTriLin (S : (SMνCharges 1).charges) (T R : (SMνCharges n).charges) :
|
||||
|
|
@ -209,7 +217,7 @@ lemma familyUniversal_cubeTriLin (S : (SMνCharges 1).charges) (T R : (SMνCharg
|
|||
rw [cubeTriLin_decomp]
|
||||
repeat rw [sum_familyUniversal_three]
|
||||
repeat rw [toSpecies_one]
|
||||
simp
|
||||
simp only [Fin.isValue, SMνSpecies_numberCharges, toSpecies_apply, add_left_inj]
|
||||
ring
|
||||
|
||||
lemma familyUniversal_cubeTriLin' (S T : (SMνCharges 1).charges) (R : (SMνCharges n).charges) :
|
||||
|
|
@ -222,7 +230,7 @@ lemma familyUniversal_cubeTriLin' (S T : (SMνCharges 1).charges) (R : (SMνChar
|
|||
rw [familyUniversal_cubeTriLin]
|
||||
repeat rw [sum_familyUniversal_two]
|
||||
repeat rw [toSpecies_one]
|
||||
simp
|
||||
simp only [Fin.isValue, SMνSpecies_numberCharges, toSpecies_apply]
|
||||
ring
|
||||
|
||||
lemma familyUniversal_accCube (S : (SMνCharges 1).charges) :
|
||||
|
|
@ -230,7 +238,8 @@ lemma familyUniversal_accCube (S : (SMνCharges 1).charges) :
|
|||
rw [accCube_decomp]
|
||||
repeat erw [sum_familyUniversal]
|
||||
rw [accCube_decomp]
|
||||
simp
|
||||
simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
|
||||
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
|
||||
ring
|
||||
|
||||
end SMRHN
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ def permGroup (n : ℕ) := Fin 6 → Equiv.Perm (Fin n)
|
|||
|
||||
variable {n : ℕ}
|
||||
|
||||
@[simps!]
|
||||
@[simp]
|
||||
instance : Group (permGroup n) := Pi.group
|
||||
|
||||
/-- The image of an element of `permGroup n` under the representation on charges. -/
|
||||
|
|
@ -52,16 +52,16 @@ def chargeMap (f : permGroup n) : (SMνCharges n).charges →ₗ[ℚ] (SMνCharg
|
|||
rfl
|
||||
|
||||
/-- The representation of `(permGroup n)` acting on the vector space of charges. -/
|
||||
@[simps!]
|
||||
@[simp]
|
||||
def repCharges {n : ℕ} : Representation ℚ (permGroup n) (SMνCharges n).charges where
|
||||
toFun f := chargeMap f⁻¹
|
||||
map_mul' f g :=by
|
||||
simp
|
||||
simp only [permGroup, mul_inv_rev]
|
||||
apply LinearMap.ext
|
||||
intro S
|
||||
rw [charges_eq_toSpecies_eq]
|
||||
intro i
|
||||
simp
|
||||
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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue