From 14377da3d87ba2992070951dc63341bb731e9da6 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 24 Oct 2024 15:04:37 +0000 Subject: [PATCH] feat: Expansion lemmas for units --- .../SpaceTime/LorentzVector/Complex/Two.lean | 24 +++++++ .../SpaceTime/LorentzVector/Complex/Unit.lean | 38 +++++++++++ HepLean/SpaceTime/WeylFermion/Unit.lean | 64 +++++++++++++++++++ HepLean/Tensors/Tree/Basic.lean | 8 ++- 4 files changed, 131 insertions(+), 3 deletions(-) diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Two.lean b/HepLean/SpaceTime/LorentzVector/Complex/Two.lean index 57388d4..05b6f0e 100644 --- a/HepLean/SpaceTime/LorentzVector/Complex/Two.lean +++ b/HepLean/SpaceTime/LorentzVector/Complex/Two.lean @@ -66,6 +66,18 @@ def contrCoToMatrix : (complexContr ⊗ complexCo).V ≃ₗ[ℂ] Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) +/-- Expansion of `contrCoToMatrix` in terms of the standard basis. -/ +lemma contrCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) : + contrCoToMatrix.symm M = ∑ i, ∑ j, M i j • (complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j) := by + simp only [Action.instMonoidalCategory_tensorObj_V, contrCoToMatrix, LinearEquiv.trans_symm, + LinearEquiv.trans_apply, Basis.repr_symm_apply] + rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)] + · erw [Finset.sum_product] + refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_)) + erw [Basis.tensorProduct_apply complexContrBasis complexCoBasis i j] + rfl + · simp + /-- Equivalence of `complexCo ⊗ complexContr` to `4 x 4` complex matrices. -/ def coContrToMatrix : (complexCo ⊗ complexContr).V ≃ₗ[ℂ] Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ := @@ -73,6 +85,18 @@ def coContrToMatrix : (complexCo ⊗ complexContr).V ≃ₗ[ℂ] Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) +/-- Expansion of `coContrToMatrix` in terms of the standard basis. -/ +lemma coContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) : + coContrToMatrix.symm M = ∑ i, ∑ j, M i j • (complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j) := by + simp only [Action.instMonoidalCategory_tensorObj_V, coContrToMatrix, LinearEquiv.trans_symm, + LinearEquiv.trans_apply, Basis.repr_symm_apply] + rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)] + · erw [Finset.sum_product] + refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_)) + erw [Basis.tensorProduct_apply complexCoBasis complexContrBasis i j] + rfl + · simp + /-! ## Group actions diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean b/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean index 1d39f52..015c2a0 100644 --- a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean +++ b/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean @@ -23,6 +23,20 @@ namespace Lorentz def contrCoUnitVal : (complexContr ⊗ complexCo).V := contrCoToMatrix.symm 1 +/-- Expansion of `contrCoUnitVal` into basis. -/ +lemma contrCoUnitVal_expand_tmul : contrCoUnitVal = + complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) := by + simp only [Action.instMonoidalCategory_tensorObj_V, contrCoUnitVal, Fin.isValue] + erw [contrCoToMatrix_symm_expand_tmul] + simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne, + zero_smul, add_zero, one_apply_eq, one_smul, zero_add, Sum.inr.injEq, zero_ne_one, Fin.reduceEq, + one_ne_zero] + rfl + /-- The contra-co unit for complex lorentz vectors as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo`, manifesting the invaraince under the `SL(2, ℂ)` action. -/ @@ -51,10 +65,29 @@ def contrCoUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo where apply congrArg simp +lemma contrCoUnit_apply_one : contrCoUnit.hom (1 : ℂ) = contrCoUnitVal := by + change contrCoUnit.hom.toFun (1 : ℂ) = contrCoUnitVal + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + contrCoUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] + /-- The co-contra unit for complex lorentz vectors. Usually denoted `δᵢⁱ`. -/ def coContrUnitVal : (complexCo ⊗ complexContr).V := coContrToMatrix.symm 1 +/-- Expansion of `coContrUnitVal` into basis. -/ +lemma coContrUnitVal_expand_tmul : coContrUnitVal = + complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + + complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + + complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + + complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) := by + simp only [Action.instMonoidalCategory_tensorObj_V, coContrUnitVal, Fin.isValue] + erw [coContrToMatrix_symm_expand_tmul] + simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne, + zero_smul, add_zero, one_apply_eq, one_smul, zero_add, Sum.inr.injEq, zero_ne_one, Fin.reduceEq, + one_ne_zero] + rfl + /-- The co-contra unit for complex lorentz vectors as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr`, manifesting the invaraince under the `SL(2, ℂ)` action. -/ @@ -85,5 +118,10 @@ def coContrUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr where refine transpose_eq_one.mp ?h.h.h.a simp +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] + end Lorentz end diff --git a/HepLean/SpaceTime/WeylFermion/Unit.lean b/HepLean/SpaceTime/WeylFermion/Unit.lean index 53041fa..bbf5663 100644 --- a/HepLean/SpaceTime/WeylFermion/Unit.lean +++ b/HepLean/SpaceTime/WeylFermion/Unit.lean @@ -28,6 +28,14 @@ open CategoryTheory.MonoidalCategory def leftAltLeftUnitVal : (leftHanded ⊗ altLeftHanded).V := leftAltLeftToMatrix.symm 1 +/-- Expansion of `leftAltLeftUnitVal` into the basis. -/ +lemma leftAltLeftUnitVal_expand_tmul : leftAltLeftUnitVal = + leftBasis 0 ⊗ₜ[ℂ] altLeftBasis 0 + leftBasis 1 ⊗ₜ[ℂ] altLeftBasis 1 := by + simp only [Action.instMonoidalCategory_tensorObj_V, leftAltLeftUnitVal, Fin.isValue] + erw [leftAltLeftToMatrix_symm_expand_tmul] + simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one, + not_false_eq_true, one_apply_ne, zero_smul, add_zero, one_ne_zero, zero_add] + /-- The left-alt-left unit `δᵃₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded `, manifesting the invariance under the `SL(2,ℂ)` action. -/ def leftAltLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded where @@ -55,10 +63,23 @@ def leftAltLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded apply congrArg simp +lemma leftAltLeftUnit_apply_one : leftAltLeftUnit.hom (1 : ℂ) = leftAltLeftUnitVal := by + change leftAltLeftUnit.hom.toFun (1 : ℂ) = leftAltLeftUnitVal + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + leftAltLeftUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] + /-- The alt-left-left unit `δₐᵃ` as an element of `(altLeftHanded ⊗ leftHanded).V`. -/ def altLeftLeftUnitVal : (altLeftHanded ⊗ leftHanded).V := altLeftLeftToMatrix.symm 1 +/-- Expansion of `altLeftLeftUnitVal` into the basis. -/ +lemma altLeftLeftUnitVal_expand_tmul : altLeftLeftUnitVal = + altLeftBasis 0 ⊗ₜ[ℂ] leftBasis 0 + altLeftBasis 1 ⊗ₜ[ℂ] leftBasis 1 := by + simp only [Action.instMonoidalCategory_tensorObj_V, altLeftLeftUnitVal, Fin.isValue] + erw [altLeftLeftToMatrix_symm_expand_tmul] + simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one, + not_false_eq_true, one_apply_ne, zero_smul, add_zero, one_ne_zero, zero_add] + /-- The alt-left-left unit `δₐᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded `, manifesting the invariance under the `SL(2,ℂ)` action. -/ def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded where @@ -87,11 +108,24 @@ def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded simp only [mul_one, ← transpose_mul, SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero, not_false_eq_true, mul_nonsing_inv, transpose_one] +lemma altLeftLeftUnit_apply_one : altLeftLeftUnit.hom (1 : ℂ) = altLeftLeftUnitVal := by + change altLeftLeftUnit.hom.toFun (1 : ℂ) = altLeftLeftUnitVal + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + altLeftLeftUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] + /-- The right-alt-right unit `δ^{dot a}_{dot a}` as an element of `(rightHanded ⊗ altRightHanded).V`. -/ def rightAltRightUnitVal : (rightHanded ⊗ altRightHanded).V := rightAltRightToMatrix.symm 1 +/-- Expansion of `rightAltRightUnitVal` into the basis. -/ +lemma rightAltRightUnitVal_expand_tmul : rightAltRightUnitVal = + rightBasis 0 ⊗ₜ[ℂ] altRightBasis 0 + rightBasis 1 ⊗ₜ[ℂ] altRightBasis 1 := by + simp only [Action.instMonoidalCategory_tensorObj_V, rightAltRightUnitVal, Fin.isValue] + erw [rightAltRightToMatrix_symm_expand_tmul] + simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one, + not_false_eq_true, one_apply_ne, zero_smul, add_zero, one_ne_zero, zero_add] + /-- The right-alt-right unit `δ^{dot a}_{dot a}` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHanded`, manifesting the invariance under the `SL(2,ℂ)` action. -/ @@ -126,11 +160,24 @@ def rightAltRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHa rw [@conjTranspose_nonsing_inv] simp +lemma rightAltRightUnit_apply_one : rightAltRightUnit.hom (1 : ℂ) = rightAltRightUnitVal := by + change rightAltRightUnit.hom.toFun (1 : ℂ) = rightAltRightUnitVal + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + rightAltRightUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] + /-- The alt-right-right unit `δ_{dot a}^{dot a}` as an element of `(rightHanded ⊗ altRightHanded).V`. -/ def altRightRightUnitVal : (altRightHanded ⊗ rightHanded).V := altRightRightToMatrix.symm 1 +/-- Expansion of `altRightRightUnitVal` into the basis. -/ +lemma altRightRightUnitVal_expand_tmul : altRightRightUnitVal = + altRightBasis 0 ⊗ₜ[ℂ] rightBasis 0 + altRightBasis 1 ⊗ₜ[ℂ] rightBasis 1 := by + simp only [Action.instMonoidalCategory_tensorObj_V, altRightRightUnitVal, Fin.isValue] + erw [altRightRightToMatrix_symm_expand_tmul] + simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one, + not_false_eq_true, one_apply_ne, zero_smul, add_zero, one_ne_zero, zero_add] + /-- The alt-right-right unit `δ_{dot a}^{dot a}` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHanded`, manifesting the invariance under the `SL(2,ℂ)` action. -/ @@ -163,5 +210,22 @@ def altRightRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHa rw [@conjTranspose_nonsing_inv] simp +lemma altRightRightUnit_apply_one : altRightRightUnit.hom (1 : ℂ) = altRightRightUnitVal := by + change altRightRightUnit.hom.toFun (1 : ℂ) = altRightRightUnitVal + simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, + altRightRightUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] + +/-! + +## Contraction of the units + +-/ + +lemma contr_leftAltLeftUnitVal (x : leftHanded) : + (λ_ leftHanded).hom.hom + (((leftAltContraction) ▷ leftHanded).hom + ((α_ _ _ leftHanded).inv.hom + (x ⊗ₜ[ℂ] altLeftLeftUnit.hom (1 : ℂ)))) = x := by + sorry end end Fermion diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean index 9a0db6c..8941602 100644 --- a/HepLean/Tensors/Tree/Basic.lean +++ b/HepLean/Tensors/Tree/Basic.lean @@ -64,20 +64,22 @@ structure TensorSpecies where /-- The unit is symmetric. -/ unit_symm (c : C) : ((unit.app (Discrete.mk c)).hom (1 : k)) = - ((FDiscrete.obj (Discrete.mk (τ (c)))) ◁ (FDiscrete.map (Discrete.eqToHom (τ_involution c)))).hom + ((FDiscrete.obj (Discrete.mk (τ (c)))) ◁ + (FDiscrete.map (Discrete.eqToHom (τ_involution c)))).hom ((β_ (FDiscrete.obj (Discrete.mk (τ (τ c)))) (FDiscrete.obj (Discrete.mk (τ (c))))).hom.hom ((unit.app (Discrete.mk (τ c))).hom (1 : k))) /-- On contracting metrics we get back the unit. -/ contr_metric (c : C) : (β_ (FDiscrete.obj (Discrete.mk c)) (FDiscrete.obj (Discrete.mk (τ c)))).hom.hom - (((FDiscrete.obj (Discrete.mk c)) ◁ (λ_ (FDiscrete.obj (Discrete.mk (τ c)))).hom).hom + (((FDiscrete.obj (Discrete.mk c)) ◁ (λ_ (FDiscrete.obj (Discrete.mk (τ c)))).hom).hom (((FDiscrete.obj (Discrete.mk c)) ◁ ((contr.app (Discrete.mk c)) ▷ (FDiscrete.obj (Discrete.mk (τ c))))).hom (((FDiscrete.obj (Discrete.mk c)) ◁ (α_ (FDiscrete.obj (Discrete.mk (c))) (FDiscrete.obj (Discrete.mk (τ c))) (FDiscrete.obj (Discrete.mk (τ c)))).inv).hom ((α_ (FDiscrete.obj (Discrete.mk (c))) (FDiscrete.obj (Discrete.mk (c))) (FDiscrete.obj (Discrete.mk (τ c)) ⊗ FDiscrete.obj (Discrete.mk (τ c)))).hom.hom - ((metric.app (Discrete.mk c)).hom (1 : k) ⊗ₜ[k] (metric.app (Discrete.mk (τ c))).hom (1 : k)))))) + ((metric.app (Discrete.mk c)).hom (1 : k) ⊗ₜ[k] + (metric.app (Discrete.mk (τ c))).hom (1 : k)))))) = (unit.app (Discrete.mk c)).hom (1 : k) noncomputable section