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-10-21 08:55:20 +00:00
parent 3035a958a5
commit 7fab77435d
2 changed files with 11 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -74,14 +74,14 @@ lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ :
set_option maxRecDepth 20000 in
/-- Contracting a rank-2 anti-symmetric tensor with a rank-2 symmetric tensor gives zero. -/
lemma symm_contract_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V)
(S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V)
lemma antiSymm_contr_symm {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
{S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
(hA : {A | μ ν = - (A | ν μ)}ᵀ) (hs : {S | μ ν = S | ν μ}ᵀ) :
{A | μ ν ⊗ S | μ ν}ᵀ.tensor = 0 := by
have hn {M : Type} [AddCommGroup M] [Module ℂ M] {x : M} (h : x = - x) : x = 0 := by
have h1 {M : Type} [AddCommGroup M] [Module ℂ M] {x : M} (h : x = - x) : x = 0 := by
rw [eq_neg_iff_add_eq_zero, ← two_smul ℂ x] at h
simpa using h
refine hn ?_
refine h1 ?_
rw [← neg_tensor]
rw [neg_perm] at hA
nth_rewrite 1 [contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_fst hA))]

10
HepLean/Tensors/OverColor/Lift.lean
View file

@ -457,9 +457,13 @@ lemma braided' (X Y : OverColor C) : (μ F X Y).hom ≫ (objMap' F) (β_ X Y).ho
(β_ (objObj' F X) (objObj' F Y)).hom ≫ (μ F Y X).hom := by
ext1
apply HepLean.PiTensorProduct.induction_tmul (fun p q => ?_)
simp [CategoryStruct.comp]
change (objMap' F (β_ X Y).hom).hom ((μ F X Y).hom.hom ((PiTensorProduct.tprod k) p ⊗ₜ[k] (PiTensorProduct.tprod k) q)) = (μ F Y X).hom.hom
((PiTensorProduct.tprod k) q ⊗ₜ[k] (PiTensorProduct.tprod k) p)
simp only [objObj'_V_carrier, instMonoidalCategoryStruct_tensorObj_left,
instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp,
Action.Hom.comp_hom, Action.instMonoidalCategory_tensorObj_V, LinearMap.coe_comp,
Function.comp_apply]
change (objMap' F (β_ X Y).hom).hom ((μ F X Y).hom.hom
((PiTensorProduct.tprod k) p ⊗ₜ[k] (PiTensorProduct.tprod k) q)) = (μ F Y X).hom.hom
((PiTensorProduct.tprod k) q ⊗ₜ[k] (PiTensorProduct.tprod k) p)
rw [μ_tmul_tprod, μ_tmul_tprod]
erw [objMap'_tprod]
apply congrArg