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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-04-18 10:27:57 -04:00
parent 96d1e87ba3
commit ee33a89de1
2 changed files with 21 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -67,11 +67,11 @@ def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
LinearMap.coe_mk, AddHom.coe_mk, Fin.coe_eq_castSucc]
rw [Fin.sum_univ_castSucc]
rw [Finset.sum_eq_single j]
simp
simp only [asCharges, PureU1_numberCharges, ↓reduceIte]
have hn : ¬ (Fin.last n = Fin.castSucc j) := by
have hj := j.prop
rw [Fin.ext_iff]
simp
simp only [Fin.val_last, Fin.coe_castSucc, ne_eq]
omega
split
rename_i ht
@ -99,17 +99,19 @@ noncomputable
def coordinateMap : ((PureU1 n.succ).LinSols) ≃ₗ[ℚ] Fin n →₀ ℚ where
toFun S := Finsupp.equivFunOnFinite.invFun (S.1 ∘ Fin.castSucc)
map_add' S T := by
simp
simp only [PureU1_numberCharges, ACCSystemLinear.linSolsAddCommMonoid_add_val,
Equiv.invFun_as_coe]
ext
simp
map_smul' a S := by
simp
simp only [PureU1_numberCharges, Equiv.invFun_as_coe, eq_ratCast, Rat.cast_eq_id, id_eq]
ext
simp
rfl
invFun f := ∑ i : Fin n, f i • asLinSols i
left_inv S := by
simp
simp only [PureU1_numberCharges, Equiv.invFun_as_coe, Finsupp.equivFunOnFinite_symm_apply_toFun,
Function.comp_apply]
apply pureU1_anomalyFree_ext
intro j
rw [sum_of_vectors]
@ -117,25 +119,25 @@ def coordinateMap : ((PureU1 n.succ).LinSols) ≃ₗ[ℚ] Fin n →₀ ℚ where
asLinSols_val, Equiv.toFun_as_coe,
Fin.coe_eq_castSucc, mul_ite, mul_one, mul_neg, mul_zero, Equiv.invFun_as_coe]
rw [Finset.sum_eq_single j]
simp
simp only [asCharges, PureU1_numberCharges, ↓reduceIte, mul_one]
intro k _ hkj
rw [asCharges_ne_castSucc hkj]
simp
simp only [mul_zero]
simp
right_inv f := by
simp
simp only [PureU1_numberCharges, Equiv.invFun_as_coe]
ext
rename_i j
simp
simp only [Finsupp.equivFunOnFinite_symm_apply_toFun, Function.comp_apply]
rw [sum_of_vectors]
simp only [HSMul.hSMul, SMul.smul, PureU1_numberCharges,
asLinSols_val, Equiv.toFun_as_coe,
Fin.coe_eq_castSucc, mul_ite, mul_one, mul_neg, mul_zero, Equiv.invFun_as_coe]
rw [Finset.sum_eq_single j]
simp
simp only [asCharges, PureU1_numberCharges, ↓reduceIte, mul_one]
intro k _ hkj
rw [asCharges_ne_castSucc hkj]
simp
simp only [mul_zero]
simp
/-- The basis of `LinSols`.-/

18
HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
View file

@ -54,7 +54,7 @@ lemma lineInPlaneCond_perm {S : (PureU1 (n)).LinSols} (hS : lineInPlaneCond S)
lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : lineInPlaneCond S)
(h : ¬ (S.val ((Fin.last n).castSucc))^2 = (S.val ((Fin.last n).succ))^2 ) :
(h : ¬ (S.val ((Fin.last n).castSucc))^2 = (S.val ((Fin.last n).succ))^2 ) :
(2 - n) * S.val (Fin.last (n + 1)) =
- (2 - n)* S.val (Fin.castSucc (Fin.last n)) := by
erw [sq_eq_sq_iff_eq_or_eq_neg] at h
@ -77,10 +77,8 @@ lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : lineIn
linear_combination h2
lemma lineInPlaneCond_eq_last {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols}
(hS : lineInPlaneCond S) :
constAbsProp
((S.val ((Fin.last n.succ.succ.succ).castSucc)), (S.val ((Fin.last n.succ.succ.succ).succ)))
:= by
(hS : lineInPlaneCond S) : constAbsProp ((S.val ((Fin.last n.succ.succ.succ).castSucc)),
(S.val ((Fin.last n.succ.succ.succ).succ))) := by
rw [constAbsProp]
by_contra hn
have h := lineInPlaneCond_eq_last' hS hn
@ -88,7 +86,7 @@ lemma lineInPlaneCond_eq_last {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols
simp [or_not] at hn
have hx : ((2 : ℚ) - ↑(n + 3)) ≠ 0 := by
rw [Nat.cast_add]
simp
simp only [Nat.cast_ofNat, ne_eq]
apply Not.intro
intro a
linarith
@ -111,7 +109,7 @@ lemma linesInPlane_eq_sq {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols}
exact lineInPlaneCond_eq_last (lineInPlaneCond_perm hS M)
theorem linesInPlane_constAbs {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols}
(hS : lineInPlaneCond S) : constAbs S.val := by
(hS : lineInPlaneCond S) : constAbs S.val := by
intro i j
by_cases hij : i ≠ j
exact linesInPlane_eq_sq hS i j hij
@ -119,7 +117,7 @@ theorem linesInPlane_constAbs {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols
rw [hij]
lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : lineInPlaneCond S.1.1) :
constAbsProp (S.val (0 : Fin 4), S.val (1 : Fin 4)) := by
constAbsProp (S.val (0 : Fin 4), S.val (1 : Fin 4)) := by
simp [constAbsProp]
by_contra hn
have hLin := pureU1_linear S.1.1
@ -172,7 +170,7 @@ lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols}
lemma linesInPlane_constAbs_four (S : (PureU1 4).Sols)
(hS : lineInPlaneCond S.1.1) : constAbs S.val := by
(hS : lineInPlaneCond S.1.1) : constAbs S.val := by
intro i j
by_cases hij : i ≠ j
exact linesInPlane_eq_sq_four hS i j hij
@ -180,7 +178,7 @@ lemma linesInPlane_constAbs_four (S : (PureU1 4).Sols)
rw [hij]
theorem linesInPlane_constAbs_AF (S : (PureU1 (n.succ.succ.succ.succ)).Sols)
(hS : lineInPlaneCond S.1.1) : constAbs S.val := by
(hS : lineInPlaneCond S.1.1) : constAbs S.val := by
induction n
exact linesInPlane_constAbs_four S hS
exact linesInPlane_constAbs hS