feat: Refactor Index notation

HepLean/Tensors/ComplexLorentz/Basic.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.OverColor.Basic
+import HepLean.Mathematics.PiTensorProduct
+/-!
+
+## Complex Lorentz tensors
+
+-/
+
+namespace Fermion
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+
+/-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
+inductive Color
+  | upL : Color
+  | downL : Color
+  | upR : Color
+  | downR : Color
+  | up : Color
+  | down : Color
+
+def τ : Color → Color
+  | Color.upL => Color.downL
+  | Color.downL => Color.upL
+  | Color.upR => Color.downR
+  | Color.downR => Color.upR
+  | Color.up => Color.down
+  | Color.down => Color.up
+
+def evalNo : Color → ℕ
+  | Color.upL => 2
+  | Color.downL => 2
+  | Color.upR => 2
+  | Color.downR => 2
+  | Color.up => 4
+  | Color.down => 4
+
+noncomputable section
+/-- The corresponding representations associated with a color. -/
+def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) :=
+  match c with
+  | Color.upL => Fermion.altLeftHanded
+  | Color.downL => Fermion.leftHanded
+  | Color.upR => Fermion.altRightHanded
+  | Color.downR => Fermion.rightHanded
+  | Color.up => Lorentz.complexContr
+  | Color.down => Lorentz.complexCo
+
+end
+end Fermion

HepLean/Tensors/ComplexLorentz/ColorFun.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
+import HepLean.Tensors.ComplexLorentz.Basic
 import HepLean.Tensors.OverColor.Basic
 import HepLean.Mathematics.PiTensorProduct
 /-!
@@ -21,40 +22,6 @@ open TensorProduct
 open IndexNotation
 open CategoryTheory
 
-/-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
-inductive Color
-  | upL : Color
-  | downL : Color
-  | upR : Color
-  | downR : Color
-  | up : Color
-  | down : Color
-
-def τ : Color → Color
-  | Color.upL => Color.downL
-  | Color.downL => Color.upL
-  | Color.upR => Color.downR
-  | Color.downR => Color.upR
-  | Color.up => Color.down
-  | Color.down => Color.up
-
-def evalNo : Color → ℕ
-  | Color.upL => 2
-  | Color.downL => 2
-  | Color.upR => 2
-  | Color.downR => 2
-  | Color.up => 4
-  | Color.down => 4
-/-- The corresponding representations associated with a color. -/
-def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) :=
-  match c with
-  | Color.upL => altLeftHanded
-  | Color.downL => leftHanded
-  | Color.upR => altRightHanded
-  | Color.downR => rightHanded
-  | Color.up => Lorentz.complexContr
-  | Color.down => Lorentz.complexCo
-
 /-- The linear equivalence between `colorToRep c1` and `colorToRep c2` when `c1 = c2`. -/
 def colorToRepCongr {c1 c2 : Color} (h : c1 = c2) : colorToRep c1 ≃ₗ[ℂ] colorToRep c2 where
   toFun := Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)
@@ -192,6 +159,12 @@ lemma map_tprod {X Y : OverColor Color} (p : (i : X.left) → (colorToRep (X.hom
       ((PiTensorProduct.tprod ℂ) p)) = _
   rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod]
 
+lemma obj_ρ_tprod (f : OverColor Color) (M : SL(2, ℂ))
+    (x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) :
+    (colorFun.obj f).ρ M ((PiTensorProduct.tprod ℂ) x) =
+    PiTensorProduct.tprod ℂ (fun i => (colorToRep (f.hom i)).ρ M (x i)) := by
+  exact obj'_ρ_tprod _ _ _
+
 @[simp]
 lemma obj_ρ_empty (g : SL(2, ℂ)) : (colorFun.obj (𝟙_ (OverColor Color))).ρ g = LinearMap.id := by
   erw [colorFun.obj'_ρ]

HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean

@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.OverColor.Basic
+import HepLean.Tensors.OverColor.Functors
+import HepLean.Tensors.COmplexLorentz.ColorFun
+import HepLean.Mathematics.PiTensorProduct
+/-!
+
+## The contraction monoidal natural transformation
+
+-/
+
+namespace Fermion
+
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+
+def tensorateContrPair (c : OverColor Color) : (OverColor.contrPair Color τ ⊗⋙ colorFunMon).obj c ≅
+    (colorFunMon.obj c) ⊗ colorFunMon.obj ((OverColor.map τ).obj c) :=
+  (colorFunMon.μIso c ((OverColor.map τ).obj c)).symm
+
+namespace pairwiseRepFun
+
+def obj' (c : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of {
+  toFun := fun M => PiTensorProduct.map (fun x =>
+    TensorProduct.map ((colorToRep (c.hom x)).ρ M) ((colorToRep (τ (c.hom x))).ρ M)),
+  map_one' := by
+    simp
+  map_mul' := fun x y => by
+    simp only [Functor.id_obj, _root_.map_mul]
+    ext x' : 2
+    simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply]
+    apply congrArg
+    funext i
+    change _ = (TensorProduct.map _ _ ∘ₗ TensorProduct.map _ _ ) (x' i)
+    rw [← TensorProduct.map_comp]
+    rfl}
+
+/-- Given a morphism in `OverColor Color` the corresopnding linear equivalence between `obj' _`
+  induced by reindexing. -/
+def mapToLinearEquiv' {f g : OverColor Color} (m : f ⟶ g) : (obj' f).V ≃ₗ[ℂ] (obj' g).V :=
+  (PiTensorProduct.reindex ℂ (fun x => (colorToRep (f.hom x)).V ⊗[ℂ] (colorToRep (τ (f.hom x))).V)
+  (OverColor.Hom.toEquiv m)).trans
+  (PiTensorProduct.congr (fun i =>
+    TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))
+    ((colorToRepCongr (congrArg τ (OverColor.Hom.toEquiv_symm_apply m i))))))
+
+lemma mapToLinearEquiv'_tprod {f g : OverColor Color} (m : f ⟶ g)
+    (x : (i : f.left) → (colorToRep (f.hom i)).V ⊗[ℂ] (colorToRep (τ (f.hom i))).V) :
+    mapToLinearEquiv' m (PiTensorProduct.tprod ℂ x) =
+    PiTensorProduct.tprod ℂ fun i =>
+    (TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i ))
+    (colorToRepCongr (mapToLinearEquiv'.proof_4 m i ))) (x ((OverColor.Hom.toEquiv m).symm i)) := by
+  simp [mapToLinearEquiv']
+  change (PiTensorProduct.congr fun i => TensorProduct.congr (colorToRepCongr _) (colorToRepCongr _))
+    ((PiTensorProduct.reindex ℂ (fun x => ↑(colorToRep (f.hom x)).V ⊗[ℂ] ↑(colorToRep (τ (f.hom x))).V)
+        (OverColor.Hom.toEquiv m))
+      ((PiTensorProduct.tprod ℂ) x)) = _
+  rw [PiTensorProduct.reindex_tprod]
+  erw [PiTensorProduct.congr_tprod]
+  rfl
+
+
+end pairwiseRepFun
+
+def pairwiseRep (c : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of {
+  toFun := fun M => PiTensorProduct.map (fun x =>
+    TensorProduct.map ((colorToRep (c.hom x)).ρ M) ((colorToRep (τ (c.hom x))).ρ M )),
+  map_one' := by
+    simp
+  map_mul' := fun x y => by
+    simp only [Functor.id_obj, _root_.map_mul]
+    ext x' : 2
+    simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply]
+    apply congrArg
+    funext i
+    change _ = (TensorProduct.map _ _ ∘ₗ TensorProduct.map _ _ ) (x' i)
+    rw [← TensorProduct.map_comp]
+    rfl}
+
+def contrPairPairwiseRep (c : OverColor Color) :
+    (colorFunMon.obj c) ⊗ colorFunMon.obj ((OverColor.map τ).obj c) ⟶
+    pairwiseRep c where
+  hom := TensorProduct.lift (PiTensorProduct.map₂ (fun x =>
+      TensorProduct.mk ℂ (colorToRep (c.hom x)).V (colorToRep (τ (c.hom x))).V))
+  comm M := by
+    refine HepLean.PiTensorProduct.induction_tmul (fun x y => ?_)
+    simp only [Functor.id_obj, CategoryStruct.comp, Action.instMonoidalCategory_tensorObj_V,
+      Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+      Action.FunctorCategoryEquivalence.functor_obj_obj, Action.tensor_ρ', LinearMap.coe_comp,
+      Function.comp_apply]
+    change (TensorProduct.lift
+      (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V ↑(colorToRep (τ (c.hom x))).V))
+      ((TensorProduct.map  _ _)
+      ((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y)) = _
+    rw [TensorProduct.map_tmul]
+    erw [colorFun.obj_ρ_tprod, colorFun.obj_ρ_tprod]
+    simp only [Functor.id_obj, lift.tmul]
+    erw [PiTensorProduct.map₂_tprod_tprod]
+    change _ = ((pairwiseRep c).ρ M)
+      ((TensorProduct.lift
+        (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V ↑(colorToRep (τ (c.hom x))).V))
+      ((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y))
+    simp only [mk_apply, Functor.id_obj, lift.tmul]
+    rw [PiTensorProduct.map₂_tprod_tprod]
+    simp only [pairwiseRep, Functor.id_obj, Rep.coe_of, Rep.of_ρ, MonoidHom.coe_mk, OneHom.coe_mk,
+      mk_apply]
+    erw [PiTensorProduct.map_tprod]
+    rfl
+
+
+end
+end Fermion

HepLean/Tensors/ComplexLorentz/Examples.lean

@@ -32,7 +32,10 @@ def upDown : Fin 2 → complexLorentzTensor.C
 
 variable (T S : complexLorentzTensor.F.obj (OverColor.mk upDown))
 
-#check {T | i i}ᵀ.dot
+/-
+#check {T | i m ⊗ S | m l}ᵀ.dot
+#check {T | i m ⊗ S | l τ(m)}ᵀ.dot
+-/
 end complexLorentzTensor
 
 end