diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean b/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean index 260ede1..73b3eff 100644 --- a/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean +++ b/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean @@ -130,7 +130,6 @@ lemma coMetric_apply_one : coMetric.hom (1 : ℂ) = coMetricVal := by simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, coMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] - /-! ## Contraction of metrics diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean b/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean index cbb5df6..0229513 100644 --- a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean +++ b/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean @@ -145,10 +145,11 @@ lemma contr_contrCoUnit (x : complexCo) : Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, _root_.map_smul] - have h1' (x y : CoeSort.coe complexCo) (z : CoeSort.coe complexContr) : + have h1' (x y : CoeSort.coe complexCo) (z : CoeSort.coe complexContr) : (α_ complexCo.V complexContr.V complexCo.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl repeat rw [h1'] - have h1'' ( y : CoeSort.coe complexCo) (z : CoeSort.coe complexCo ⊗[ℂ] CoeSort.coe complexContr) : + have h1'' (y : CoeSort.coe complexCo) + (z : CoeSort.coe complexCo ⊗[ℂ] CoeSort.coe complexContr) : (coContrContraction.hom ▷ complexCo.V) (z ⊗ₜ[ℂ] y) = (coContrContraction.hom z) ⊗ₜ[ℂ] y := rfl repeat rw (config := { transparency := .instances }) [h1''] repeat rw [coContrContraction_basis'] @@ -178,11 +179,14 @@ lemma contr_coContrUnit (x : complexContr) : Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, _root_.map_smul] - have h1' (x y : CoeSort.coe complexContr) (z : CoeSort.coe complexCo) : - (α_ complexContr.V complexCo.V complexContr.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl + have h1' (x y : CoeSort.coe complexContr) (z : CoeSort.coe complexCo) : + (α_ complexContr.V complexCo.V complexContr.V).inv + (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl repeat rw [h1'] - have h1'' ( y : CoeSort.coe complexContr) (z : CoeSort.coe complexContr ⊗[ℂ] CoeSort.coe complexCo) : - (contrCoContraction.hom ▷ complexContr.V) (z ⊗ₜ[ℂ] y) = (contrCoContraction.hom z) ⊗ₜ[ℂ] y := rfl + have h1'' (y : CoeSort.coe complexContr) + (z : CoeSort.coe complexContr ⊗[ℂ] CoeSort.coe complexCo) : + (contrCoContraction.hom ▷ complexContr.V) (z ⊗ₜ[ℂ] y) = + (contrCoContraction.hom z) ⊗ₜ[ℂ] y := rfl repeat rw (config := { transparency := .instances }) [h1''] repeat rw [contrCoContraction_basis'] simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, ↓reduceIte, reduceCtorEq, @@ -199,7 +203,6 @@ lemma contr_coContrUnit (x : complexContr) : -/ - open CategoryTheory lemma contrCoUnit_symm : diff --git a/HepLean/SpaceTime/WeylFermion/Metric.lean b/HepLean/SpaceTime/WeylFermion/Metric.lean index 44c9ae7..cf45196 100644 --- a/HepLean/SpaceTime/WeylFermion/Metric.lean +++ b/HepLean/SpaceTime/WeylFermion/Metric.lean @@ -352,8 +352,8 @@ lemma rightAltContraction_apply_metric : (β_ rightHanded altRightHanded).hom.ho ((rightHanded.V ◁ rightAltContraction.hom ▷ altRightHanded.V) (((rightHanded.V ◁ (α_ rightHanded.V altRightHanded.V altRightHanded.V).inv) ((α_ rightHanded.V rightHanded.V (altRightHanded.V ⊗ altRightHanded.V)).hom - ((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2))))) - = x1 ⊗ₜ[ℂ] ((λ_ altRightHanded.V).hom ((rightAltContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl + ((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2))))) = x1 ⊗ₜ[ℂ] ((λ_ altRightHanded.V).hom + ((rightAltContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl repeat rw (config := { transparency := .instances }) [h1] repeat rw [rightAltContraction_basis] simp only [Fin.isValue, Fin.val_one, Fin.val_zero, one_ne_zero, ↓reduceIte, zero_tmul, map_zero, @@ -374,7 +374,8 @@ lemma altRightContraction_apply_metric : (β_ altRightHanded rightHanded).hom.ho rw [rightMetricVal_expand_tmul, altRightMetricVal_expand_tmul] simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue, tmul_add, tmul_neg, sub_tmul, map_add, map_neg, map_sub] - have h1 (x1 x2 : altRightHanded) (y1 y2 : rightHanded) : (altRightHanded.V ◁ (λ_ rightHanded.V).hom) + have h1 (x1 x2 : altRightHanded) (y1 y2 : rightHanded) : + (altRightHanded.V ◁ (λ_ rightHanded.V).hom) ((altRightHanded.V ◁ altRightContraction.hom ▷ rightHanded.V) (((altRightHanded.V ◁ (α_ altRightHanded.V rightHanded.V rightHanded.V).inv) ((α_ altRightHanded.V altRightHanded.V (rightHanded.V ⊗ rightHanded.V)).hom diff --git a/HepLean/SpaceTime/WeylFermion/Unit.lean b/HepLean/SpaceTime/WeylFermion/Unit.lean index 38d74d3..accba8a 100644 --- a/HepLean/SpaceTime/WeylFermion/Unit.lean +++ b/HepLean/SpaceTime/WeylFermion/Unit.lean @@ -251,7 +251,7 @@ lemma contr_altLeftLeftUnit (x : leftHanded) : simp only [Fin.isValue, one_smul] /-- Contraction on the right with `leftAltLeftUnit` does nothing. -/ -lemma contr_leftAltLeftUnit (x : altLeftHanded) : +lemma contr_leftAltLeftUnit (x : altLeftHanded) : (λ_ altLeftHanded).hom.hom (((altLeftContraction) ▷ altLeftHanded).hom ((α_ _ _ altLeftHanded).inv.hom @@ -333,29 +333,29 @@ lemma contr_rightAltRightUnit (x : altRightHanded) : open CategoryTheory lemma altLeftLeftUnit_symm : - (altLeftLeftUnit.hom (1 : ℂ)) = (altLeftHanded ◁ 𝟙 _).hom ((β_ leftHanded altLeftHanded ).hom.hom - (leftAltLeftUnit.hom (1 : ℂ))) := by + (altLeftLeftUnit.hom (1 : ℂ)) = (altLeftHanded ◁ 𝟙 _).hom + ((β_ leftHanded altLeftHanded).hom.hom (leftAltLeftUnit.hom (1 : ℂ))) := by rw [altLeftLeftUnit_apply_one, altLeftLeftUnitVal_expand_tmul] rw [leftAltLeftUnit_apply_one, leftAltLeftUnitVal_expand_tmul] rfl lemma leftAltLeftUnit_symm : - (leftAltLeftUnit.hom (1 : ℂ)) = (leftHanded ◁ 𝟙 _).hom ((β_ altLeftHanded leftHanded ).hom.hom + (leftAltLeftUnit.hom (1 : ℂ)) = (leftHanded ◁ 𝟙 _).hom ((β_ altLeftHanded leftHanded).hom.hom (altLeftLeftUnit.hom (1 : ℂ))) := by rw [altLeftLeftUnit_apply_one, altLeftLeftUnitVal_expand_tmul] rw [leftAltLeftUnit_apply_one, leftAltLeftUnitVal_expand_tmul] rfl lemma altRightRightUnit_symm : - (altRightRightUnit.hom (1 : ℂ)) = (altRightHanded ◁ 𝟙 _).hom ((β_ rightHanded altRightHanded ).hom.hom - (rightAltRightUnit.hom (1 : ℂ))) := by + (altRightRightUnit.hom (1 : ℂ)) = (altRightHanded ◁ 𝟙 _).hom + ((β_ rightHanded altRightHanded).hom.hom (rightAltRightUnit.hom (1 : ℂ))) := by rw [altRightRightUnit_apply_one, altRightRightUnitVal_expand_tmul] rw [rightAltRightUnit_apply_one, rightAltRightUnitVal_expand_tmul] rfl lemma rightAltRightUnit_symm : - (rightAltRightUnit.hom (1 : ℂ)) = (rightHanded ◁ 𝟙 _).hom ((β_ altRightHanded rightHanded ).hom.hom - (altRightRightUnit.hom (1 : ℂ))) := by + (rightAltRightUnit.hom (1 : ℂ)) = (rightHanded ◁ 𝟙 _).hom + ((β_ altRightHanded rightHanded).hom.hom (altRightRightUnit.hom (1 : ℂ))) := by rw [altRightRightUnit_apply_one, altRightRightUnitVal_expand_tmul] rw [rightAltRightUnit_apply_one, rightAltRightUnitVal_expand_tmul] rfl diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean index 9ef374f..b1dd57f 100644 --- a/HepLean/Tensors/ComplexLorentz/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/Basic.lean @@ -183,7 +183,7 @@ def complexLorentzTensor : TensorSpecies where | Color.downR => Fermion.rightAltRightUnit_symm | Color.up => Lorentz.coContrUnit_symm | Color.down => Lorentz.contrCoUnit_symm - contr_metric := fun c => + contr_metric := fun c => match c with | Color.upL => by simpa using Fermion.leftAltContraction_apply_metric | Color.downL => by simpa using Fermion.altLeftContraction_apply_metric