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

fix: Anomaly Cancellation Group Actions & others

Browse source
This commit is contained in:
jstoobysmith 2024-11-02 08:03:04 +00:00
parent a532c51d64
commit e6045e5f58
4 changed files with 14 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

14
HepLean/AnomalyCancellation/GroupActions.lean
View file

@ -89,16 +89,16 @@ instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
rfl
lemma linSolRep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
(S : χ.QuadSols) : χ.quadSolsInclLinSols (G.quadSolAction.toFun S g) =
(S : χ.QuadSols) : χ.quadSolsInclLinSols (G.quadSolAction.toFun _ _ S g) =
G.linSolRep g (χ.quadSolsInclLinSols S) := rfl
lemma rep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
(S : χ.QuadSols) : χ.quadSolsIncl (G.quadSolAction.toFun S g) =
(S : χ.QuadSols) : χ.quadSolsIncl (G.quadSolAction.toFun _ _ S g) =
G.rep g (χ.quadSolsIncl S) := rfl
/-- The group action acting on solutions to the anomaly cancellation conditions. -/
instance solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.group χ.Sols where
smul g S := ⟨G.quadSolAction.toFun S.1 g, by
smul g S := ⟨G.quadSolAction.toFun _ _ S.1 g, by
simp only [MulAction.toFun_apply]
change χ.cubicACC (G.rep g S.val) = 0
rw [G.cubicInvariant, S.cubicSol]⟩
@ -114,14 +114,14 @@ instance solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.
rfl
lemma quadSolAction_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
(S : χ.Sols) : χ.solsInclQuadSols (G.solAction.toFun S g) =
G.quadSolAction.toFun (χ.solsInclQuadSols S) g := rfl
(S : χ.Sols) : χ.solsInclQuadSols (G.solAction.toFun _ _ S g) =
G.quadSolAction.toFun _ _ (χ.solsInclQuadSols S) g := rfl
lemma linSolRep_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
(S : χ.Sols) : χ.solsInclLinSols (G.solAction.toFun S g) =
(S : χ.Sols) : χ.solsInclLinSols (G.solAction.toFun _ _ S g) =
G.linSolRep g (χ.solsInclLinSols S) := rfl
lemma rep_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
(S : χ.Sols) : χ.solsIncl (G.solAction.toFun S g) = G.rep g (χ.solsIncl S) := rfl
(S : χ.Sols) : χ.solsIncl (G.solAction.toFun _ _ S g) = G.rep g (χ.solsIncl S) := rfl
end ACCSystemGroupAction

9
HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
View file

@ -66,7 +66,7 @@ def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
split
· rename_i ht
exact (hn ht).elim
· rfl
· with_unfolding_all rfl
· intro k _ hkj
exact asCharges_ne_castSucc hkj.symm
· intro hk
@ -124,10 +124,11 @@ instance : Module.Finite ℚ ((PureU1 n.succ).LinSols) :=
Module.Finite.of_basis asBasis
lemma finrank_AnomalyFreeLinear :
FiniteDimensional.finrank ℚ (((PureU1 n.succ).LinSols)) = n := by
Module.finrank ℚ (((PureU1 n.succ).LinSols)) = n := by
have h := Module.mk_finrank_eq_card_basis (@asBasis n)
simp only [Nat.succ_eq_add_one, finrank_eq_rank, Cardinal.mk_fintype, Fintype.card_fin] at h
exact FiniteDimensional.finrank_eq_of_rank_eq h
simp only [Nat.succ_eq_add_one, Module.finrank_eq_rank, Cardinal.mk_fintype,
Fintype.card_fin] at h
exact Module.finrank_eq_of_rank_eq h
end BasisLinear

2
HepLean/AnomalyCancellation/SM/FamilyMaps.lean
View file

@ -65,7 +65,7 @@ def speciesEmbed (m n : ℕ) :
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]
rfl
with_unfolding_all rfl
map_smul' a S := by
funext i
simp only [SMSpecies_numberCharges, HSMul.hSMul, ACCSystemCharges.chargesModule_smul,