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

refactor: Proof golf

Browse source
This commit is contained in:
jstoobysmith 2024-10-21 14:17:14 +00:00
parent 1e57e50d5e
commit 7fc850cc38
2 changed files with 4 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

20
HepLean/Tensors/ComplexLorentz/Lemmas.lean
View file

@ -89,8 +89,7 @@ lemma contr_rank_2_symm {T1 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
rw [perm_perm]
rw [perm_eq_id]
· rfl
· apply OverColor.Hom.ext
rfl
· rfl
· apply OverColor.Hom.ext
ext x
exact Fin.elim0 x
@ -105,7 +104,6 @@ lemma contr_rank_2_symm' {T1 : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
ext x
exact Fin.elim0 x
set_option maxRecDepth 20000 in
/-- Contracting a rank-2 anti-symmetric tensor with a rank-2 symmetric tensor gives zero. -/
lemma antiSymm_contr_symm {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
{S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
@ -122,21 +120,7 @@ lemma antiSymm_contr_symm {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V
rw [contr_tensor_eq (contr_tensor_eq (neg_fst_prod _ _))]
rw [contr_tensor_eq (neg_contr _)]
rw [neg_contr]
rw [neg_tensor]
apply congrArg
rw [contr_tensor_eq (contr_tensor_eq (prod_perm_left _ _ _ _))]
rw [contr_tensor_eq (perm_contr _ _)]
rw [perm_contr]
rw [perm_tensor_eq (contr_tensor_eq (contr_tensor_eq (prod_perm_right _ _ _ _)))]
rw [perm_tensor_eq (contr_tensor_eq (perm_contr _ _))]
rw [perm_tensor_eq (perm_contr _ _)]
rw [perm_perm]
nth_rewrite 1 [perm_tensor_eq (contr_contr _ _ _)]
rw [perm_perm]
rw [perm_eq_id]
· rfl
· apply OverColor.Hom.ext
rfl
rfl
lemma symm_contr_antiSymm {S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
{A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}

11
HepLean/Tensors/Tree/NodeIdentities/ContrSwap.lean
View file

@ -88,12 +88,6 @@ lemma contrMap_swap : q.contrMap = q.swap.contrMap ≫ S.F.map q.contrSwapHom :=
Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V, Equivalence.symm_inverse,
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
Functor.comp_obj, Discrete.functor_obj_eq_as, map_smul]
have h1n' {a b d: Fin n.succ.succ} (hbd : b = d) (h : c d = S.τ (c a))
(h' : c b = S.τ (c a)) :
(S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
(S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
subst hbd
rfl
congr 1
/- The contractions. -/
· apply congrArg
@ -106,10 +100,9 @@ lemma contrMap_swap : q.contrMap = q.swap.contrMap ≫ S.F.map q.contrSwapHom :=
subst haa'
simp_all
refine h1' ?_ ?_ ?_
· simp
· simp only [Discrete.mk.injEq]
exact Eq.symm (swapI_color q)
· refine h1n' ?_ ?_ ?_
rfl
· rfl
· change _ = ((S.FDiscrete.map (Discrete.eqToHom _)) ≫ S.FDiscrete.map (Discrete.eqToHom _)).hom
(x (q.swap.i.succAbove q.swap.j))
rw [← S.FDiscrete.map_comp]