feat: contr and prod for basis

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.

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 =