Merge pull request #180 from HEPLean/Lorentz

refactor: Index notation
2024-10-08 08:00:34 +00:00 · 2024-10-08 08:00:34 +00:00 · 5a34238499
commit 5a34238499
parent 96e911ec27 48a69b56a8
7 changed files with 599 additions and 129 deletions
--- a/HepLean.lean
+++ b/HepLean.lean
@ -90,8 +90,8 @@ import HepLean.SpaceTime.LorentzVector.NormOne
 import HepLean.SpaceTime.MinkowskiMetric
 import HepLean.SpaceTime.SL2C.Basic
 import HepLean.SpaceTime.WeylFermion.Basic
+import HepLean.SpaceTime.WeylFermion.ColorFun
 import HepLean.SpaceTime.WeylFermion.Modules
-import HepLean.SpaceTime.WeylFermion.OverCat
 import HepLean.StandardModel.Basic
 import HepLean.StandardModel.HiggsBoson.Basic
 import HepLean.StandardModel.HiggsBoson.GaugeAction
@ -99,6 +99,7 @@ import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
 import HepLean.StandardModel.HiggsBoson.Potential
 import HepLean.StandardModel.Representations
 import HepLean.Tensors.Basic
+import HepLean.Tensors.ColorCat.Basic
 import HepLean.Tensors.Contraction
 import HepLean.Tensors.EinsteinNotation.Basic
 import HepLean.Tensors.EinsteinNotation.IndexNotation
@ -122,3 +123,5 @@ import HepLean.Tensors.IndexNotation.IndexString
 import HepLean.Tensors.IndexNotation.TensorIndex
 import HepLean.Tensors.MulActionTensor
 import HepLean.Tensors.RisingLowering
+import HepLean.Tensors.Tree.Basic
+import HepLean.Tensors.Tree.Elab
--- a/HepLean/SpaceTime/WeylFermion/ColorFun.lean
+++ b/HepLean/SpaceTime/WeylFermion/ColorFun.lean
@ -3,136 +3,12 @@ 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 Mathlib.CategoryTheory.Category.Basic
-import Mathlib.CategoryTheory.Types
-import Mathlib.CategoryTheory.Monoidal.Category
-import Mathlib.CategoryTheory.Comma.Over
-import Mathlib.CategoryTheory.Core
-import HepLean.SpaceTime.WeylFermion.Basic
-import HepLean.SpaceTime.LorentzVector.Complex
+import HepLean.Tensors.ColorCat.Basic
 /-!

-## Category over color
+## Monodial functor from color cat.

 -/
-
-namespace IndexNotation
-open CategoryTheory
-
-/-- The core of the category of Types over C. -/
-def OverColor (C : Type) := CategoryTheory.Core (CategoryTheory.Over C)
-
-/-- The instance of `OverColor C` as a groupoid. -/
-instance (C : Type) : Groupoid (OverColor C) := coreCategory
-
-namespace OverColor
-
-namespace Hom
-
-variable {C : Type} {f g h : OverColor C}
-
-/-- Given a hom in `OverColor C` the underlying equivalence between types. -/
-def toEquiv (m : f ⟶ g) : f.left ≃ g.left where
-  toFun := m.hom.left
-  invFun := m.inv.left
-  left_inv := by
-    simpa only [Over.comp_left] using congrFun (congrArg (fun x => x.left) m.hom_inv_id)
-  right_inv := by
-    simpa only [Over.comp_left] using congrFun (congrArg (fun x => x.left) m.inv_hom_id)
-
-@[simp]
-lemma toEquiv_comp (m : f ⟶ g) (n : g ⟶ h) : toEquiv (m ≫ n) = (toEquiv m).trans (toEquiv n) := by
-  ext x
-  simp [toEquiv]
-  rfl
-
-lemma toEquiv_symm_apply (m : f ⟶ g) (i : g.left) :
-    f.hom ((toEquiv m).symm i) = g.hom i := by
-  simpa [toEquiv, types_comp] using congrFun m.inv.w i
-
-lemma toEquiv_comp_hom (m : f ⟶ g) : g.hom ∘ (toEquiv m) = f.hom := by
-  ext x
-  simpa [types_comp, toEquiv] using congrFun m.hom.w x
-
-end Hom
-
-instance (C : Type) : MonoidalCategoryStruct (OverColor C) where
-  tensorObj f g := Over.mk (Sum.elim f.hom g.hom)
-  tensorUnit := Over.mk Empty.elim
-  whiskerLeft X Y1 Y2 m := Over.isoMk (Equiv.sumCongr (Equiv.refl X.left) (Hom.toEquiv m)).toIso
-    (by
-      ext x
-      simp only [Functor.id_obj, Functor.const_obj_obj, Over.mk_left, Equiv.toIso_hom, Over.mk_hom,
-        types_comp_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
-      rw [Sum.elim_map, Hom.toEquiv_comp_hom]
-      rfl)
-  whiskerRight m X := Over.isoMk (Equiv.sumCongr (Hom.toEquiv m) (Equiv.refl X.left)).toIso
-    (by
-      ext x
-      simp only [Functor.id_obj, Functor.const_obj_obj, Over.mk_left, Equiv.toIso_hom, Over.mk_hom,
-        types_comp_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
-      rw [Sum.elim_map, Hom.toEquiv_comp_hom]
-      rfl)
-  associator X Y Z := {
-    hom := Over.isoMk (Equiv.sumAssoc X.left Y.left Z.left).toIso (by
-      simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Functor.const_obj_obj, Equiv.sumAssoc,
-        Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp]
-      ext x
-      simp only [Function.comp_apply]
-      cases x with
-      | inl val =>
-        cases val with
-        | inl val_1 => simp_all only [Sum.elim_inl]
-        | inr val_2 => simp_all only [Sum.elim_inl, Sum.elim_inr, Function.comp_apply]
-      | inr val_1 => simp_all only [Sum.elim_inr, Function.comp_apply]),
-    inv := (Over.isoMk (Equiv.sumAssoc X.left Y.left Z.left).toIso (by
-      simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Functor.const_obj_obj, Equiv.sumAssoc,
-        Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp]
-      ext x
-      simp only [Function.comp_apply]
-      cases x with
-      | inl val =>
-        cases val with
-        | inl val_1 => simp_all only [Sum.elim_inl]
-        | inr val_2 => simp_all only [Sum.elim_inl, Sum.elim_inr, Function.comp_apply]
-      | inr val_1 => simp_all only [Sum.elim_inr, Function.comp_apply])).symm,
-    hom_inv_id := by
-      apply CategoryTheory.Iso.ext
-      erw [CategoryTheory.Iso.trans_hom]
-      simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
-      rfl,
-    inv_hom_id := by
-      apply CategoryTheory.Iso.ext
-      erw [CategoryTheory.Iso.trans_hom]
-      simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.inv_hom_id]
-      rfl}
-  leftUnitor X := {
-    hom := Over.isoMk (Equiv.emptySum Empty X.left).toIso
-    inv := (Over.isoMk (Equiv.emptySum Empty X.left).toIso).symm
-    hom_inv_id := by
-      apply CategoryTheory.Iso.ext
-      erw [CategoryTheory.Iso.trans_hom]
-      simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
-      rfl,
-    inv_hom_id := by
-      apply CategoryTheory.Iso.ext
-      erw [CategoryTheory.Iso.trans_hom]}
-  rightUnitor X := {
-    hom := Over.isoMk (Equiv.sumEmpty X.left Empty).toIso
-    inv := (Over.isoMk (Equiv.sumEmpty X.left Empty).toIso).symm
-    hom_inv_id := by
-      apply CategoryTheory.Iso.ext
-      erw [CategoryTheory.Iso.trans_hom]
-      simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
-      rfl,
-    inv_hom_id := by
-      apply CategoryTheory.Iso.ext
-      erw [CategoryTheory.Iso.trans_hom]}
-
-end OverColor
-
-end IndexNotation
-
 namespace Fermion

 noncomputable section
@ -250,6 +126,7 @@ end colorFun

 /-- The functor between `OverColor Color` and `Rep ℂ SL(2, ℂ)` taking a map of colors
  to the corresponding tensor product representation. -/
+@[simps! obj_V_carrier]
 def colorFun : OverColor Color ⥤ Rep ℂ SL(2, ℂ) where
  obj := colorFun.obj'
  map := colorFun.map'
@ -282,5 +159,40 @@ def colorFun : OverColor Color ⥤ Rep ℂ SL(2, ℂ) where
      Equiv.cast_apply, cast_cast, cast_inj]
    rfl

+namespace colorFun
+
+open CategoryTheory
+open MonoidalCategory
+
+@[simp]
+lemma obj_ρ_empty (g : SL(2, ℂ)) : (colorFun.obj (𝟙_ (OverColor Color))).ρ g = LinearMap.id := by
+  erw [colorFun.obj'_ρ]
+  ext x
+  refine PiTensorProduct.induction_on' x (fun r x => ?_) <| fun x y hx hy => by
+    simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
+      Function.comp_apply, hy]
+    erw [hx, hy]
+    rfl
+  simp only [OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj,
+    OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.tprodCoeff_eq_smul_tprod,
+    _root_.map_smul, PiTensorProduct.map_tprod, LinearMap.id_coe, id_eq]
+  apply congrArg
+  apply congrArg
+  funext i
+  exact Empty.elim i
+
+/-- The unit natural transformation. -/
+def ε : 𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ colorFun.obj (𝟙_ (OverColor Color)) where
+  hom := (PiTensorProduct.isEmptyEquiv Empty).symm.toLinearMap
+  comm M := by
+    refine LinearMap.ext (fun x => ?_)
+    simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorUnit_left,
+      OverColor.instMonoidalCategoryStruct_tensorUnit_hom, Action.instMonoidalCategory_tensorUnit_V,
+      Action.tensorUnit_ρ', Functor.id_obj, Category.id_comp, LinearEquiv.coe_coe]
+    erw [obj_ρ_empty M]
+    rfl
+
+end colorFun
+
 end
 end Fermion
--- a/HepLean/Tensors/Basic.lean
+++ b/HepLean/Tensors/Basic.lean
@ -541,8 +541,10 @@ def domCoprod : MultilinearMap R (fun x => 𝓣.ColorModule (Sum.elim cX cY x))
    (PiTensorProduct.tprod R (𝓣.inrPureTensor f))
  map_add' f xy v1 v2:= by
    match xy with
-    | Sum.inl x => simp [← TensorProduct.add_tmul]
-    | Sum.inr y => simp [← TensorProduct.tmul_add]
+    | Sum.inl x => simp only [Sum.elim_inl, inlPureTensor_update_left, MultilinearMap.map_add,
+      inrPureTensor_update_left, ← add_tmul]
+    | Sum.inr y => simp only [Sum.elim_inr, inlPureTensor_update_right, inrPureTensor_update_right,
+      MultilinearMap.map_add, ← tmul_add]
  map_smul' f xy r p := by
    match xy with
    | Sum.inl x => simp [TensorProduct.tmul_smul, TensorProduct.smul_tmul]
--- a/HepLean/Tensors/ColorCat/Basic.lean
+++ b/HepLean/Tensors/ColorCat/Basic.lean
@ -0,0 +1,251 @@
+/-
+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 Mathlib.CategoryTheory.Category.Basic
+import Mathlib.CategoryTheory.Types
+import Mathlib.CategoryTheory.Monoidal.Category
+import Mathlib.CategoryTheory.Comma.Over
+import Mathlib.CategoryTheory.Core
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
+import HepLean.SpaceTime.WeylFermion.Basic
+import HepLean.SpaceTime.LorentzVector.Complex
+/-!
+
+## Over category.
+
+-/
+
+namespace IndexNotation
+open CategoryTheory
+
+/-- The core of the category of Types over C. -/
+def OverColor (C : Type) := CategoryTheory.Core (CategoryTheory.Over C)
+
+/-- The instance of `OverColor C` as a groupoid. -/
+instance (C : Type) : Groupoid (OverColor C) := coreCategory
+
+namespace OverColor
+
+namespace Hom
+
+variable {C : Type} {f g h : OverColor C}
+
+/-- Given a hom in `OverColor C` the underlying equivalence between types. -/
+def toEquiv (m : f ⟶ g) : f.left ≃ g.left where
+  toFun := m.hom.left
+  invFun := m.inv.left
+  left_inv := by
+    simpa only [Over.comp_left] using congrFun (congrArg (fun x => x.left) m.hom_inv_id)
+  right_inv := by
+    simpa only [Over.comp_left] using congrFun (congrArg (fun x => x.left) m.inv_hom_id)
+
+@[simp]
+lemma toEquiv_id (f : OverColor C) : toEquiv (𝟙 f) = Equiv.refl f.left := by
+  ext x
+  simp [toEquiv]
+  rfl
+
+@[simp]
+lemma toEquiv_comp (m : f ⟶ g) (n : g ⟶ h) : toEquiv (m ≫ n) = (toEquiv m).trans (toEquiv n) := by
+  ext x
+  simp [toEquiv]
+  rfl
+
+lemma toEquiv_symm_apply (m : f ⟶ g) (i : g.left) :
+    f.hom ((toEquiv m).symm i) = g.hom i := by
+  simpa [toEquiv, types_comp] using congrFun m.inv.w i
+
+lemma toEquiv_comp_hom (m : f ⟶ g) : g.hom ∘ (toEquiv m) = f.hom := by
+  ext x
+  simpa [types_comp, toEquiv] using congrFun m.hom.w x
+
+end Hom
+
+section monoidal
+
+/-!
+
+## The monoidal structure on `OverColor C`.
+
+The category `OverColor C` can, through the disjoint union, be given the structure of a
+symmetric monoidal category.
+
+-/
+
+@[simps!]
+instance (C : Type) : MonoidalCategoryStruct (OverColor C) where
+  tensorObj f g := Over.mk (Sum.elim f.hom g.hom)
+  tensorUnit := Over.mk Empty.elim
+  whiskerLeft X Y1 Y2 m := Over.isoMk (Equiv.sumCongr (Equiv.refl X.left) (Hom.toEquiv m)).toIso
+    (by
+      ext x
+      simp only [Functor.id_obj, Functor.const_obj_obj, Over.mk_left, Equiv.toIso_hom, Over.mk_hom,
+        types_comp_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
+      rw [Sum.elim_map, Hom.toEquiv_comp_hom]
+      rfl)
+  whiskerRight m X := Over.isoMk (Equiv.sumCongr (Hom.toEquiv m) (Equiv.refl X.left)).toIso
+    (by
+      ext x
+      simp only [Functor.id_obj, Functor.const_obj_obj, Over.mk_left, Equiv.toIso_hom, Over.mk_hom,
+        types_comp_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
+      rw [Sum.elim_map, Hom.toEquiv_comp_hom]
+      rfl)
+  associator X Y Z := {
+    hom := Over.isoMk (Equiv.sumAssoc X.left Y.left Z.left).toIso (by
+      ext x
+      match x with
+      | Sum.inl (Sum.inl x) => rfl
+      | Sum.inl (Sum.inr x) => rfl
+      | Sum.inr x => rfl),
+    inv := (Over.isoMk (Equiv.sumAssoc X.left Y.left Z.left).toIso (by
+      ext x
+      match x with
+      | Sum.inl (Sum.inl x) => rfl
+      | Sum.inl (Sum.inr x) => rfl
+      | Sum.inr x => rfl)).symm,
+    hom_inv_id := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl (Sum.inl x) => rfl
+      | Sum.inl (Sum.inr x) => rfl
+      | Sum.inr x => rfl,
+    inv_hom_id := by
+      apply CategoryTheory.Iso.ext
+      erw [CategoryTheory.Iso.trans_hom]
+      simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.inv_hom_id]
+      rfl}
+  leftUnitor X := {
+    hom := Over.isoMk (Equiv.emptySum Empty X.left).toIso
+    inv := (Over.isoMk (Equiv.emptySum Empty X.left).toIso).symm
+    hom_inv_id := by
+      apply CategoryTheory.Iso.ext
+      erw [CategoryTheory.Iso.trans_hom]
+      simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
+      rfl,
+    inv_hom_id := by
+      apply CategoryTheory.Iso.ext
+      erw [CategoryTheory.Iso.trans_hom]}
+  rightUnitor X := {
+    hom := Over.isoMk (Equiv.sumEmpty X.left Empty).toIso
+    inv := (Over.isoMk (Equiv.sumEmpty X.left Empty).toIso).symm
+    hom_inv_id := by
+      apply CategoryTheory.Iso.ext
+      erw [CategoryTheory.Iso.trans_hom]
+      simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
+      rfl,
+    inv_hom_id := by
+      apply CategoryTheory.Iso.ext
+      erw [CategoryTheory.Iso.trans_hom]}
+
+instance (C : Type) : MonoidalCategory (OverColor C) where
+    tensorHom_def f g := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => rfl
+    tensor_id X Y := CategoryTheory.Iso.ext <| (Iso.eq_inv_comp _).mp rfl
+    tensor_comp f1 f2 g1 g2 := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl x => rfl
+      | Sum.inr x => rfl
+    whiskerLeft_id X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl x => rfl
+      | Sum.inr x => rfl
+    id_whiskerRight X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl x => rfl
+      | Sum.inr x => rfl
+    associator_naturality {X1 X2 X3 Y1 Y2 Y3} f1 f2 f3 :=
+        CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl (Sum.inl x) => rfl
+      | Sum.inl (Sum.inr x) => rfl
+      | Sum.inr x => rfl
+    leftUnitor_naturality f :=
+        CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl x => exact Empty.elim x
+      | Sum.inr x => rfl
+    rightUnitor_naturality f :=
+        CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl x => rfl
+      | Sum.inr x => exact Empty.elim x
+    pentagon f g h i := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl (Sum.inl (Sum.inl x)) => rfl
+      | Sum.inl (Sum.inl (Sum.inr x)) => rfl
+      | Sum.inl (Sum.inr x) => rfl
+      | Sum.inr x => rfl
+    triangle f g := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl (Sum.inl x) => rfl
+      | Sum.inl (Sum.inr x) => exact Empty.elim x
+      | Sum.inr x => rfl
+
+instance (C : Type) : BraidedCategory (OverColor C) where
+  braiding f g := {
+    hom := Over.isoMk (Equiv.sumComm f.left g.left).toIso
+    inv := (Over.isoMk (Equiv.sumComm f.left g.left).toIso).symm
+    hom_inv_id := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl x => rfl
+      | Sum.inr x => rfl,
+    inv_hom_id := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+      match x with
+      | Sum.inl x => rfl
+      | Sum.inr x => rfl}
+  braiding_naturality_right X Y1 Y2 f := CategoryTheory.Iso.ext <| Over.OverMorphism.ext
+      <| funext fun x => by
+    match x with
+    | Sum.inl x => rfl
+    | Sum.inr x => rfl
+  braiding_naturality_left X f := CategoryTheory.Iso.ext <| Over.OverMorphism.ext
+      <| funext fun x => by
+    match x with
+    | Sum.inl x => rfl
+    | Sum.inr x => rfl
+  hexagon_forward X1 X2 X3 := CategoryTheory.Iso.ext <| Over.OverMorphism.ext
+      <| funext fun x => by
+    match x with
+    | Sum.inl (Sum.inl x) => rfl
+    | Sum.inl (Sum.inr x) => rfl
+    | Sum.inr x => rfl
+  hexagon_reverse X1 X2 X3 := CategoryTheory.Iso.ext <| Over.OverMorphism.ext
+      <| funext fun x => by
+    match x with
+    | Sum.inr (Sum.inl x) => rfl
+    | Sum.inr (Sum.inr x) => rfl
+    | Sum.inl x => rfl
+
+instance (C : Type) : SymmetricCategory (OverColor C) where
+  toBraidedCategory := instBraidedCategory C
+  symmetry X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+    match x with
+    | Sum.inl x => rfl
+    | Sum.inr x => rfl
+
+end monoidal
+
+/-- Make an object of `OverColor C` from a map `X → C`. -/
+def mk (f : X → C) : OverColor C := Over.mk f
+
+open MonoidalCategory
+
+/-- The isomorphism between `c : X → C` and `c ∘ e.symm` as objects in `OverColor C` for an
+  equivalence `e`. -/
+def equivToIso {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ e.symm) := {
+  hom := Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl),
+  inv := (Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl)).symm,
+  hom_inv_id := by
+    apply CategoryTheory.Iso.ext
+    erw [CategoryTheory.Iso.trans_hom]
+    simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
+    rfl,
+  inv_hom_id := by
+    apply CategoryTheory.Iso.ext
+    erw [CategoryTheory.Iso.trans_hom]
+    simp only [Iso.symm_hom, Iso.inv_hom_id]
+    rfl}
+
+end OverColor
+
+end IndexNotation
--- a/HepLean/Tensors/IndexNotation/Basic.lean
+++ b/HepLean/Tensors/IndexNotation/Basic.lean
@ -17,6 +17,11 @@ The first character `ᵘ` specifies the color of the index, and the subsequent c

 Strings of indices e.g. `ᵘ¹²ᵤ₄₃`` are defined elsewhere.

+## Note
+
+Index notation is currently being refactored. Much of the content here will likely be replaced
+or removed. See the HepLean.Tensors.Tree.Basic for the current approach of the index notation.
+
 -/

 open Lean
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@ -0,0 +1,106 @@
+/-
+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.ColorCat.Basic
+/-!
+
+## Tensor trees
+
+-/
+
+open IndexNotation
+open CategoryTheory
+
+/-- The sturcture of a type of tensors e.g. Lorentz tensors, Einstien tensors,
+  complex Lorentz tensors.
+  Note: This structure is not fully defined yet. -/
+structure TensorStruct where
+  /-- The colors of indices e.g. up or down. -/
+  C : Type
+  /-- The symmetry group acting on these tensor e.g. the Lorentz group or SL(2,ℂ). -/
+  G : Type
+  /-- An instance of `G` as a group. -/
+  G_group : Group G
+  /-- The field over which we want to consider the tensors to live in, usually `ℝ` or `ℂ`. -/
+  k : Type
+  /-- An instance of `k` as a commutative ring. -/
+  k_commRing : CommRing k
+  /-- A `MonoidalFunctor` from `OverColor C` giving the rep corresponding to a map of colors
+    `X → C`. -/
+  F : MonoidalFunctor (OverColor C) (Rep k G)
+  /-- A map from `C` to `C`. An involution. -/
+  τ : C → C
+  /-- A specification of the dimension of each color in C. This will be used for explicit
+    evaluation of tensors. -/
+  evalNo : C → ℕ
+
+namespace TensorStruct
+
+variable (S : TensorStruct)
+
+instance : CommRing S.k := S.k_commRing
+
+instance : Group S.G := S.G_group
+
+end TensorStruct
+
+/-- A syntax tree for tensor expressions. -/
+inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Type where
+  | tensorNode {n : ℕ} {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : TensorTree S c
+  | add {n : ℕ} {c : Fin n → S.C} : TensorTree S c → TensorTree S c → TensorTree S c
+  | perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
+      (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) : TensorTree S c1
+  | prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
+    (t : TensorTree S c) (t1 : TensorTree S c1) : TensorTree S (Sum.elim c c1 ∘ finSumFinEquiv.symm)
+  | scale {n : ℕ} {c : Fin n → S.C} : S.k → TensorTree S c → TensorTree S c
+  | mult {n m : ℕ} {c : Fin n.succ → S.C} {c1 : Fin m.succ → S.C} :
+    (i : Fin n.succ) → (j : Fin m.succ) → TensorTree S c → TensorTree S c1 →
+    TensorTree S (Sum.elim (c ∘ Fin.succAbove i) (c1 ∘ Fin.succAbove j) ∘ finSumFinEquiv.symm)
+  | contr {n : ℕ} {c : Fin n.succ.succ → S.C} : (i : Fin n.succ.succ) →
+    (j : Fin n.succ) → TensorTree S c → TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
+  | jiggle {n : ℕ} {c : Fin n → S.C} : (i : Fin n) → TensorTree S c →
+    TensorTree S (Function.update c i (S.τ (c i)))
+  | eval {n : ℕ} {c : Fin n.succ → S.C} :
+    (i : Fin n.succ) → (x : Fin (S.evalNo (c i))) → TensorTree S c →
+    TensorTree S (c ∘ Fin.succAbove i)
+
+namespace TensorTree
+
+variable {S : TensorStruct} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c)
+
+open MonoidalCategory
+open TensorProduct
+
+/-- The number of nodes in a tensor tree. -/
+def size : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → ℕ := fun
+  | tensorNode _ => 1
+  | add t1 t2 => t1.size + t2.size + 1
+  | perm _ t => t.size + 1
+  | scale _ t => t.size + 1
+  | prod t1 t2 => t1.size + t2.size + 1
+  | mult _ _ t1 t2 => t1.size + t2.size + 1
+  | contr _ _ t => t.size + 1
+  | jiggle _ t => t.size + 1
+  | eval _ _ t => t.size + 1
+
+noncomputable section
+
+/-- The underlying tensor a tensor tree corresponds to.
+  Note: This function is not fully defined yet. -/
+def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (OverColor.mk c) := fun
+  | tensorNode t => t
+  | add t1 t2 => t1.tensor + t2.tensor
+  | perm σ t => (S.F.map σ).hom t.tensor
+  | scale a t => a • t.tensor
+  | prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
+    ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor))
+  | _ => 0
+
+lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :
+    (tensorNode T).tensor = T := rfl
+
+end
+
+end TensorTree
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@ -0,0 +1,191 @@
+/-
+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.Tree.Basic
+import Lean.Elab.Term
+/-!
+
+## Elaboration of tensor trees
+
+This file turns tensor expressions into tensor trees.
+
+-/
+open Lean
+open Lean.Elab.Term
+
+open Lean
+open Lean.Meta
+open Lean.Elab
+open Lean.Elab.Term
+open Lean Meta Elab Tactic
+
+/-!
+
+## Indexies
+
+-/
+
+/-- A syntax category for indices of tensor expressions. -/
+declare_syntax_cat indexExpr
+
+/-- A basic index is a ident. -/
+syntax ident : indexExpr
+
+/-- An index can be a num, which will be used to evaluate the tensor. -/
+syntax num : indexExpr
+
+/-- Notation to discribe the jiggle of a tensor index. -/
+syntax "τ(" ident ")" : indexExpr
+
+/-- Bool which is ture if an index is a num. -/
+def indexExprIsNum (stx : Syntax) : Bool :=
+  match stx with
+  | `(indexExpr|$_:num) => true
+  | _ => false
+
+/-- If an index is a num - the undelrying natural number. -/
+def indexToNum (stx : Syntax) : TermElabM Nat :=
+  match stx with
+  | `(indexExpr|$a:num) =>
+    match a.raw.isNatLit? with
+    | some n => return n
+    | none => throwError "Expected a natural number literal."
+  | _ =>
+    throwError "Unsupported tensor expression syntax in indexToNum: {stx}"
+
+/-- When an index is not a num, the corresponding ident. -/
+def indexToIdent (stx : Syntax) : TermElabM Ident :=
+  match stx with
+  | `(indexExpr|$a:ident) => return a
+  | `(indexExpr| τ($a:ident)) => return a
+  | _ =>
+    throwError "Unsupported tensor expression syntax in indexToIdent: {stx}"
+
+/-- Takes a pair ``a b : ℕ × TSyntax `indexExpr``. If `a.1 < b.1` and `a.2 = b.2` then
+  outputs `some (a.1, b.1)`, otherwise `none`. -/
+def indexPosEq (a b : ℕ × TSyntax `indexExpr) : TermElabM (Option (ℕ × ℕ)) := do
+  let a' ← indexToIdent a.2
+  let b' ← indexToIdent b.2
+  if a.1 < b.1 ∧ Lean.TSyntax.getId a' = Lean.TSyntax.getId b' then
+    return some (a.1, b.1)
+  else
+    return none
+
+/-- Bool which is true if an index is of the form τ(i) that is, to be dualed. -/
+def indexToDual (stx : Syntax) : Bool :=
+  match stx with
+  | `(indexExpr| τ($_)) => true
+  | _ => false
+/-!
+
+## Tensor expressions
+
+-/
+
+/-- A syntax category for tensor expressions. -/
+declare_syntax_cat tensorExpr
+
+/-- The syntax for a tensor node. -/
+syntax term "|" (ppSpace indexExpr)* : tensorExpr
+
+/-- The syntax for tensor prod two tensor nodes. -/
+syntax tensorExpr "⊗" tensorExpr : tensorExpr
+
+/-- Allowing brackets to be used in a tensor expression. -/
+syntax "(" tensorExpr ")" : tensorExpr
+
+/-!
+
+## For tensor nodes.
+
+The operations are done in the following order:
+- evaluation.
+- dualization.
+- contraction.
+-/
+
+namespace TensorNode
+
+/-- The indices of a tensor node. Before contraction, dualisation, and evaluation. -/
+partial def getIndicesNode (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
+  match stx with
+  | `(tensorExpr| $_:term | $[$args]*) => do
+      let indices ← args.toList.mapM fun arg => do
+        match arg with
+        | `(indexExpr|$t:indexExpr) => pure t
+      return indices
+  | _ =>
+    throwError "Unsupported tensor expression syntax in getIndicesNode: {stx}"
+
+/-- The positions in getIndicesNode which get evaluated, and the value they take. -/
+partial def getEvalPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do
+  let ind ← getIndicesNode stx
+  let indEnum := ind.enum
+  let evals := indEnum.filter (fun x => indexExprIsNum x.2)
+  let evals2 ← (evals.mapM (fun x => indexToNum x.2))
+  return List.zip (evals.map (fun x => x.1)) evals2
+
+/-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.eval` to the given term. -/
+def evalSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
+  l.foldl (fun T' (x1, x2) => Syntax.mkApp (mkIdent ``TensorTree.eval)
+    #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x2), T']) T
+
+/-- The positions in getIndicesNode which get dualized. -/
+partial def getDualPos (stx : Syntax) : TermElabM (List ℕ) := do
+  let ind ← getIndicesNode stx
+  let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x)
+  let indEnum := indFilt.enum
+  let duals := indEnum.filter (fun x => indexToDual x.2)
+  return duals.map (fun x => x.1)
+
+/-- For each element of `l : List ℕ` applies `TensorTree.jiggle` to the given term. -/
+def dualSyntax (l : List ℕ) (T : Term) : Term :=
+  l.foldl (fun T' x => Syntax.mkApp (mkIdent ``TensorTree.jiggle)
+    #[Syntax.mkNumLit (toString x), T']) T
+
+/-- The pairs of positions in getIndicesNode which get contracted. -/
+partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do
+  let ind ← getIndicesNode stx
+  let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x)
+  let indEnum := indFilt.enum
+  let bind := List.bind indEnum (fun a => indEnum.map (fun b => (a, b)))
+  let filt ← bind.filterMapM (fun x => indexPosEq x.1 x.2)
+  if ¬ ((filt.map Prod.fst).Nodup ∧ (filt.map Prod.snd).Nodup) then
+    throwError "To many contractions"
+  return filt
+
+/-- The list of indices after contraction. -/
+def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
+  let ind ← getIndicesNode stx
+  let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x)
+  return ind.filter (fun x => indFilt.count x ≤ 1)
+
+/-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.contr` to the given term. -/
+def contrSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
+  l.foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr)
+    #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), T']) T
+
+/-- An elaborator for tensor nodes. This is to be generalized. -/
+def elaborateTensorNode (stx : Syntax) : TermElabM Expr := do
+  match stx with
+  | `(tensorExpr| $T:term | $[$args]*) => do
+      let tensorNodeSyntax := Syntax.mkApp (mkIdent ``TensorTree.tensorNode) #[T]
+      let evalSyntax := evalSyntax (← getEvalPos stx) tensorNodeSyntax
+      let dualSyntax := dualSyntax (← getDualPos stx) evalSyntax
+      let contrSyntax := contrSyntax (← getContrPos stx) dualSyntax
+      let tensorExpr ← elabTerm contrSyntax none
+      return tensorExpr
+  | _ =>
+    throwError "Unsupported tensor expression syntax in elaborateTensorNode: {stx}"
+
+/-- Syntax turning a tensor expression into a term. -/
+syntax (name := tensorExprSyntax) "{" tensorExpr "}ᵀ" : term
+
+elab_rules (kind:=tensorExprSyntax) : term
+  | `(term| {$e:tensorExpr}ᵀ) => do
+    let tensorTree ← elaborateTensorNode e
+    return tensorTree
+
+end TensorNode