From b70e9bd005aa45f0ad00bb0720489cfbd9fe9da0 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 23 Oct 2024 10:50:14 +0000 Subject: [PATCH] feat: contr and prod for basis --- HepLean/Tensors/ComplexLorentz/Basis.lean | 54 ++++++++++++++++++++--- HepLean/Tensors/OverColor/Lift.lean | 30 ++++++++++++- 2 files changed, 76 insertions(+), 8 deletions(-) diff --git a/HepLean/Tensors/ComplexLorentz/Basis.lean b/HepLean/Tensors/ComplexLorentz/Basis.lean index 545ad9a..ce9c1da 100644 --- a/HepLean/Tensors/ComplexLorentz/Basis.lean +++ b/HepLean/Tensors/ComplexLorentz/Basis.lean @@ -79,21 +79,63 @@ lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C} eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, LinearEquiv.ofLinear_apply] rw [basis_eq_FDiscrete] -lemma contr_basisVector {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} - {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : - (contr i j h (tensorNode (basisVector c b))).tensor = (if (b i).val = ((b (i.succAbove j))).val then (1 : ℂ) else 0) • - basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j) - (fun k => b (i.succAbove (j.succAbove k))) := by +lemma contr_basisVector {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} + {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} + (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : + (contr i j h (tensorNode (basisVector c b))).tensor = (if (b i).val = (b (i.succAbove j)).val + then (1 : ℂ) else 0) • basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j) + (fun k => b (i.succAbove (j.succAbove k))) := by rw [contr_tensor] simp only [Nat.succ_eq_add_one, tensorNode_tensor] rw [basisVector] erw [TensorSpecies.contrMap_tprod] congr 1 rw [basis_eq_FDiscrete] - simp + simp only [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, + Function.comp_apply] erw [basis_contr] rfl +def prodBasisVecEquiv {n m : ℕ} {c : Fin n → complexLorentzTensor.C} + {c1 : Fin m → complexLorentzTensor.C} (i : Fin n ⊕ Fin m) : + Sum.elim (fun i => Fin (complexLorentzTensor.repDim (c i))) (fun i => Fin (complexLorentzTensor.repDim (c1 i))) + i ≃ Fin (complexLorentzTensor.repDim ((Sum.elim c c1 i))) := + match i with + | Sum.inl _ => Equiv.refl _ + | Sum.inr _ => Equiv.refl _ + +lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C} + {c1 : Fin m → complexLorentzTensor.C} + (b : Π k, Fin (complexLorentzTensor.repDim (c k))) + (b1 : Π k, Fin (complexLorentzTensor.repDim (c1 k))) : + (prod (tensorNode (basisVector c b)) (tensorNode (basisVector c1 b1))).tensor = + basisVector (Sum.elim c c1 ∘ finSumFinEquiv.symm) (fun i => + prodBasisVecEquiv (finSumFinEquiv.symm i) + ((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))) := by + rw [prod_tensor] + simp + rw [basisVector, basisVector] + simp [TensorSpecies.F_def] + have h1 := OverColor.lift.μ_tmul_tprod_mk complexLorentzTensor.FDiscrete + (fun i => (complexLorentzTensor.basis (c i)) (b i)) + (fun i => (complexLorentzTensor.basis (c1 i)) (b1 i)) + erw [h1] + erw [OverColor.lift.map_tprod] + apply congrArg + funext i + obtain ⟨k, hk⟩ := finSumFinEquiv.surjective i + subst hk + simp only [Functor.id_obj, OverColor.mk_hom, Function.comp_apply, + OverColor.lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, + Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply] + erw [← (Equiv.apply_eq_iff_eq_symm_apply finSumFinEquiv).mp rfl] + match k with + | Sum.inl k => rfl + | Sum.inr k => rfl + + /-! ## Useful expansions. diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean index a25f3f0..bbb08ec 100644 --- a/HepLean/Tensors/OverColor/Lift.lean +++ b/HepLean/Tensors/OverColor/Lift.lean @@ -207,6 +207,13 @@ def discreteSumEquiv {X Y : OverColor C} (i : X.left ⊕ Y.left) : | Sum.inl _ => LinearEquiv.refl _ _ | Sum.inr _ => LinearEquiv.refl _ _ +def discreteSumEquiv' {X Y : Type} {cX : X → C} {cY : Y → C} (i : X ⊕ Y) : + Sum.elim (fun i => F.obj (Discrete.mk (cX i))) + (fun i => F.obj (Discrete.mk (cY i))) i ≃ₗ[k] F.obj (Discrete.mk ((Sum.elim cX cY) i)) := + match i with + | Sum.inl _ => LinearEquiv.refl _ _ + | Sum.inr _ => LinearEquiv.refl _ _ + /-- The equivalence of modules corresonding to the tensorate. -/ def μModEquiv (X Y : OverColor C) : (objObj' F X ⊗ objObj' F Y).V ≃ₗ[k] objObj' F (X ⊗ Y) := @@ -258,8 +265,27 @@ lemma μ_tmul_tprod {X Y : OverColor C} (p : (i : X.left) → F.obj (Discrete.mk (q : (i : Y.left) → (F.obj <| Discrete.mk (Y.hom i))) : (μ F X Y).hom.hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) = (PiTensorProduct.tprod k) fun i => - discreteSumEquiv F i (HepLean.PiTensorProduct.elimPureTensor p q i) := by - exact μModEquiv_tmul_tprod F p q + discreteSumEquiv F i (HepLean.PiTensorProduct.elimPureTensor p q i) := + μModEquiv_tmul_tprod F p q + +lemma μ_tmul_tprod_mk {X Y : Type} {cX : X → C} {cY : Y → C} + (p : (i : X) → F.obj (Discrete.mk <| cX i)) + (q : (i : Y) → (F.obj <| Discrete.mk (cY i))) : + (μ F (OverColor.mk cX) (OverColor.mk cY)).hom.hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) + = (PiTensorProduct.tprod k) fun i => + discreteSumEquiv' F i (HepLean.PiTensorProduct.elimPureTensor p q i) := by + let q' : (i : (OverColor.mk cY).left) → (F.obj <| Discrete.mk ((OverColor.mk cY).hom i)) := q + let p' : (i : (OverColor.mk cX).left) → (F.obj <| Discrete.mk ((OverColor.mk cX).hom i)) := p + have h1 := μModEquiv_tmul_tprod F p' q' + simp at h1 + erw [h1] + simp [p', q'] + apply congrArg + funext i + match i with + | Sum.inl i => rfl + | Sum.inr i => rfl + lemma μ_natural_left {X Y : OverColor C} (f : X ⟶ Y) (Z : OverColor C) : MonoidalCategory.whiskerRight (objMap' F f) (objObj' F Z) ≫ (μ F Y Z).hom =