From 942ee12e6057019370c8fb758c0b4e3a3d852096 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 24 Oct 2024 15:52:56 +0000 Subject: [PATCH] feat: contr_unit for Complex Lorentz Tensors --- .../LorentzVector/Complex/Contraction.lean | 22 ++++ .../SpaceTime/LorentzVector/Complex/Unit.lean | 71 ++++++++++++ HepLean/SpaceTime/WeylFermion/Unit.lean | 102 +++++++++++++++++- HepLean/Tensors/ComplexLorentz/Basic.lean | 8 ++ 4 files changed, 201 insertions(+), 2 deletions(-) diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean b/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean index 4cd7e1c..0302039 100644 --- a/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean +++ b/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean @@ -97,6 +97,17 @@ lemma contrCoContraction_basis (i j : Fin 4) : refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl) simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm] +lemma contrCoContraction_basis' (i j : Fin 1 ⊕ Fin 3) : + contrCoContraction.hom (complexContrBasis i ⊗ₜ complexCoBasis j) = + if i = j then (1 : ℂ) else 0 := by + rw [contrCoContraction_hom_tmul] + simp only [Action.instMonoidalCategory_tensorUnit_V, complexContrBasisFin4, Basis.coe_reindex, + Function.comp_apply, complexContrBasis_toFin13ℂ, complexCoBasisFin4, complexCoBasis_toFin13ℂ, + dotProduct_single, mul_one] + rw [Pi.single_apply] + refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl) + exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a) + /-- The linear map from complexCo ⊗ complexContr to ℂ given by summing over components of covariant Lorentz vector and contravariant Lorentz vector in the @@ -126,6 +137,17 @@ lemma coContrContraction_basis (i j : Fin 4) : refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl) simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm] +lemma coContrContraction_basis' (i j : Fin 1 ⊕ Fin 3) : + coContrContraction.hom (complexCoBasis i ⊗ₜ complexContrBasis j) = + if i = j then (1 : ℂ) else 0 := by + rw [coContrContraction_hom_tmul] + simp only [Action.instMonoidalCategory_tensorUnit_V, complexCoBasisFin4, Basis.coe_reindex, + Function.comp_apply, complexCoBasis_toFin13ℂ, complexContrBasisFin4, complexContrBasis_toFin13ℂ, + dotProduct_single, mul_one] + rw [Pi.single_apply] + refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl) + simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm] + /-! ## Symmetry diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean b/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean index 015c2a0..1fdea5d 100644 --- a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean +++ b/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzVector.Complex.Two +import HepLean.SpaceTime.LorentzVector.Complex.Contraction /-! # Unit for complex Lorentz vectors @@ -122,6 +123,76 @@ lemma coContrUnit_apply_one : coContrUnit.hom (1 : ℂ) = coContrUnitVal := by change coContrUnit.hom.toFun (1 : ℂ) = coContrUnitVal simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, coContrUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] +/-! + +## Contraction of the units + +-/ + +/-- Contraction on the right with `contrCoUnit` does nothing. -/ +lemma contr_contrCoUnit (x : complexCo) : + (λ_ complexCo).hom.hom + ((coContrContraction ▷ complexCo).hom + ((α_ _ _ complexCo).inv.hom + (x ⊗ₜ[ℂ] contrCoUnit.hom (1 : ℂ)))) = x := by + obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span complexCoBasis x) + subst hc + rw [contrCoUnit_apply_one, contrCoUnitVal_expand_tmul] + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom, + Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse, + Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, + 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) : + (α_ 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) : + (coContrContraction.hom ▷ complexCo.V) (z ⊗ₜ[ℂ] y) = (coContrContraction.hom z) ⊗ₜ[ℂ] y := rfl + repeat rw (config := { transparency := .instances }) [h1''] + repeat rw [coContrContraction_basis'] + simp only [Fin.isValue, leftUnitor, ModuleCat.MonoidalCategory.leftUnitor, ModuleCat.of_coe, + CategoryTheory.Iso.trans_hom, LinearEquiv.toModuleIso_hom, ModuleCat.ofSelfIso_hom, + CategoryTheory.Category.comp_id, Action.instMonoidalCategory_tensorUnit_V, ↓reduceIte, + reduceCtorEq, zero_tmul, map_zero, smul_zero, add_zero, Sum.inr.injEq, one_ne_zero, + Fin.reduceEq, zero_add, zero_ne_one] + erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul, TensorProduct.lid_tmul, + TensorProduct.lid_tmul] + simp only [Fin.isValue, one_smul] + repeat rw [add_assoc] + +/-- Contraction on the right with `coContrUnit`. -/ +lemma contr_coContrUnit (x : complexContr) : + (λ_ complexContr).hom.hom + ((contrCoContraction ▷ complexContr).hom + ((α_ _ _ complexContr).inv.hom + (x ⊗ₜ[ℂ] coContrUnit.hom (1 : ℂ)))) = x := by + obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span complexContrBasis x) + subst hc + rw [coContrUnit_apply_one, coContrUnitVal_expand_tmul] + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom, + Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse, + Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, + 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 + 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 + repeat rw (config := { transparency := .instances }) [h1''] + repeat rw [contrCoContraction_basis'] + simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, ↓reduceIte, reduceCtorEq, + zero_tmul, map_zero, smul_zero, add_zero, Sum.inr.injEq, one_ne_zero, Fin.reduceEq, zero_add, + zero_ne_one] + erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul, TensorProduct.lid_tmul, + TensorProduct.lid_tmul] + simp only [Fin.isValue, one_smul] + repeat rw [add_assoc] + end Lorentz end diff --git a/HepLean/SpaceTime/WeylFermion/Unit.lean b/HepLean/SpaceTime/WeylFermion/Unit.lean index bbf5663..b67e111 100644 --- a/HepLean/SpaceTime/WeylFermion/Unit.lean +++ b/HepLean/SpaceTime/WeylFermion/Unit.lean @@ -7,6 +7,7 @@ import HepLean.SpaceTime.WeylFermion.Basic import HepLean.SpaceTime.WeylFermion.Contraction import Mathlib.LinearAlgebra.TensorProduct.Matrix import HepLean.SpaceTime.WeylFermion.Two +import LLMLean /-! # Units of Weyl fermions @@ -221,11 +222,108 @@ lemma altRightRightUnit_apply_one : altRightRightUnit.hom (1 : ℂ) = altRightRi -/ -lemma contr_leftAltLeftUnitVal (x : leftHanded) : +/-- Contraction on the right with `altLeftLeftUnit` does nothing. -/ +lemma contr_altLeftLeftUnit (x : leftHanded) : (λ_ leftHanded).hom.hom (((leftAltContraction) ▷ leftHanded).hom ((α_ _ _ leftHanded).inv.hom (x ⊗ₜ[ℂ] altLeftLeftUnit.hom (1 : ℂ)))) = x := by - sorry + obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span leftBasis x) + subst hc + rw [altLeftLeftUnit_apply_one, altLeftLeftUnitVal_expand_tmul] + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom, + Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse, + Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, + Fin.sum_univ_two, Fin.isValue, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, + _root_.map_smul] + have h1 (x y : leftHanded) (z : altLeftHanded) : (leftAltContraction.hom ▷ leftHanded.V) + ((α_ leftHanded.V altLeftHanded.V leftHanded.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y)) = + (leftAltContraction.hom (x ⊗ₜ[ℂ] z)) ⊗ₜ[ℂ] y := rfl + erw [h1, h1, h1, h1] + repeat rw [leftAltContraction_basis] + simp only [Fin.isValue, leftUnitor, ModuleCat.MonoidalCategory.leftUnitor, ModuleCat.of_coe, + CategoryTheory.Iso.trans_hom, LinearEquiv.toModuleIso_hom, ModuleCat.ofSelfIso_hom, + CategoryTheory.Category.comp_id, Action.instMonoidalCategory_tensorUnit_V, Fin.val_zero, + ↓reduceIte, Fin.val_one, one_ne_zero, zero_tmul, map_zero, smul_zero, add_zero, zero_ne_one, + zero_add] + erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul] + simp only [Fin.isValue, one_smul] + +/-- Contraction on the right with `leftAltLeftUnit` does nothing. -/ +lemma contr_leftAltLeftUnit (x : altLeftHanded) : + (λ_ altLeftHanded).hom.hom + (((altLeftContraction) ▷ altLeftHanded).hom + ((α_ _ _ altLeftHanded).inv.hom + (x ⊗ₜ[ℂ] leftAltLeftUnit.hom (1 : ℂ)))) = x := by + obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span altLeftBasis x) + subst hc + rw [leftAltLeftUnit_apply_one, leftAltLeftUnitVal_expand_tmul] + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom, + Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse, + Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, + Fin.sum_univ_two, Fin.isValue, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, + _root_.map_smul] + have h1 (x y : altLeftHanded) (z : leftHanded) : (altLeftContraction.hom ▷ altLeftHanded.V) + ((α_ altLeftHanded.V leftHanded.V altLeftHanded.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y)) = + (altLeftContraction.hom (x ⊗ₜ[ℂ] z)) ⊗ₜ[ℂ] y := rfl + erw [h1, h1, h1, h1] + repeat rw [altLeftContraction_basis] + simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, Fin.val_zero, ↓reduceIte, + Fin.val_one, one_ne_zero, zero_tmul, map_zero, smul_zero, add_zero, zero_ne_one, zero_add] + erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul] + simp only [Fin.isValue, one_smul] + +/-- Contraction on the right with `altRightRightUnit` does nothing. -/ +lemma contr_altRightRightUnit (x : rightHanded) : + (λ_ rightHanded).hom.hom + (((rightAltContraction) ▷ rightHanded).hom + ((α_ _ _ rightHanded).inv.hom + (x ⊗ₜ[ℂ] altRightRightUnit.hom (1 : ℂ)))) = x := by + obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span rightBasis x) + subst hc + rw [altRightRightUnit_apply_one, altRightRightUnitVal_expand_tmul] + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom, + Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse, + Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, + Fin.sum_univ_two, Fin.isValue, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, + _root_.map_smul] + have h1 (x y : rightHanded) (z : altRightHanded) : (rightAltContraction.hom ▷ rightHanded.V) + ((α_ rightHanded.V altRightHanded.V rightHanded.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y)) = + (rightAltContraction.hom (x ⊗ₜ[ℂ] z)) ⊗ₜ[ℂ] y := rfl + erw [h1, h1, h1, h1] + repeat rw [rightAltContraction_basis] + simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, Fin.val_zero, ↓reduceIte, + Fin.val_one, one_ne_zero, zero_tmul, map_zero, smul_zero, add_zero, zero_ne_one, zero_add] + erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul] + simp only [Fin.isValue, one_smul] + +/-- Contraction on the right with `rightAltRightUnit` does nothing. -/ +lemma contr_rightAltRightUnit (x : altRightHanded) : + (λ_ altRightHanded).hom.hom + (((altRightContraction) ▷ altRightHanded).hom + ((α_ _ _ altRightHanded).inv.hom + (x ⊗ₜ[ℂ] rightAltRightUnit.hom (1 : ℂ)))) = x := by + obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span altRightBasis x) + subst hc + rw [rightAltRightUnit_apply_one, rightAltRightUnitVal_expand_tmul] + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom, + Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse, + Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, + Fin.sum_univ_two, Fin.isValue, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, + _root_.map_smul] + have h1 (x y : altRightHanded) (z : rightHanded) : (altRightContraction.hom ▷ altRightHanded.V) + ((α_ altRightHanded.V rightHanded.V altRightHanded.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y)) = + (altRightContraction.hom (x ⊗ₜ[ℂ] z)) ⊗ₜ[ℂ] y := rfl + erw [h1, h1, h1, h1] + repeat rw [altRightContraction_basis] + simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, Fin.val_zero, ↓reduceIte, + Fin.val_one, one_ne_zero, zero_tmul, map_zero, smul_zero, add_zero, zero_ne_one, zero_add] + erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul] + simp only [Fin.isValue, one_smul] + end end Fermion diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean index 8c4a0a0..57fcf69 100644 --- a/HepLean/Tensors/ComplexLorentz/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/Basic.lean @@ -167,6 +167,14 @@ def complexLorentzTensor : TensorSpecies where | Color.downR => Fermion.altRightContraction_tmul_symm | Color.up => Lorentz.contrCoContraction_tmul_symm | Color.down => Lorentz.coContrContraction_tmul_symm + contr_unit := fun c => + match c with + | Color.upL => Fermion.contr_altLeftLeftUnit + | Color.downL => Fermion.contr_leftAltLeftUnit + | Color.upR => Fermion.contr_altRightRightUnit + | Color.downR => Fermion.contr_rightAltRightUnit + | Color.up => Lorentz.contr_coContrUnit + | Color.down => Lorentz.contr_contrCoUnit instance : DecidableEq complexLorentzTensor.C := Fermion.instDecidableEqColor