feat: lemmas relating to index notation

2024-10-17 11:43:33 +00:00 · 2024-10-17 11:43:33 +00:00 · 672cc1ed8b
commit 672cc1ed8b
parent ac11a510cf
11 changed files with 510 additions and 17 deletions
--- a/HepLean/Tensors/ComplexLorentz/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basic.lean
@ -38,6 +38,46 @@ inductive Color
  | up : Color
  | down : Color

+instance : DecidableEq Color := fun x y =>
+  match x, y with
+  | Color.upL, Color.upL => isTrue rfl
+  | Color.downL, Color.downL => isTrue rfl
+  | Color.upR, Color.upR => isTrue rfl
+  | Color.downR, Color.downR => isTrue rfl
+  | Color.up, Color.up => isTrue rfl
+  | Color.down, Color.down => isTrue rfl
+  /- The false -/
+  | Color.upL, Color.downL => isFalse fun h => Color.noConfusion h
+  | Color.upL, Color.upR => isFalse fun h => Color.noConfusion h
+  | Color.upL, Color.downR => isFalse fun h => Color.noConfusion h
+  | Color.upL, Color.up => isFalse fun h => Color.noConfusion h
+  | Color.upL, Color.down => isFalse fun h => Color.noConfusion h
+  | Color.downL, Color.upL => isFalse fun h => Color.noConfusion h
+  | Color.downL, Color.upR => isFalse fun h => Color.noConfusion h
+  | Color.downL, Color.downR => isFalse fun h => Color.noConfusion h
+  | Color.downL, Color.up => isFalse fun h => Color.noConfusion h
+  | Color.downL, Color.down => isFalse fun h => Color.noConfusion h
+  | Color.upR, Color.upL => isFalse fun h => Color.noConfusion h
+  | Color.upR, Color.downL => isFalse fun h => Color.noConfusion h
+  | Color.upR, Color.downR => isFalse fun h => Color.noConfusion h
+  | Color.upR, Color.up => isFalse fun h => Color.noConfusion h
+  | Color.upR, Color.down => isFalse fun h => Color.noConfusion h
+  | Color.downR, Color.upL => isFalse fun h => Color.noConfusion h
+  | Color.downR, Color.downL => isFalse fun h => Color.noConfusion h
+  | Color.downR, Color.upR => isFalse fun h => Color.noConfusion h
+  | Color.downR, Color.up => isFalse fun h => Color.noConfusion h
+  | Color.downR, Color.down => isFalse fun h => Color.noConfusion h
+  | Color.up, Color.upL => isFalse fun h => Color.noConfusion h
+  | Color.up, Color.downL => isFalse fun h => Color.noConfusion h
+  | Color.up, Color.upR => isFalse fun h => Color.noConfusion h
+  | Color.up, Color.downR => isFalse fun h => Color.noConfusion h
+  | Color.up, Color.down => isFalse fun h => Color.noConfusion h
+  | Color.down, Color.upL => isFalse fun h => Color.noConfusion h
+  | Color.down, Color.downL => isFalse fun h => Color.noConfusion h
+  | Color.down, Color.upR => isFalse fun h => Color.noConfusion h
+  | Color.down, Color.downR => isFalse fun h => Color.noConfusion h
+  | Color.down, Color.up => isFalse fun h => Color.noConfusion h
+
 noncomputable section

 /-- The tensor structure for complex Lorentz tensors. -/
@ -104,5 +144,7 @@ def complexLorentzTensor : TensorStruct where
    | Color.up => 4
    | Color.down => 4

+instance : DecidableEq complexLorentzTensor.C := Fermion.instDecidableEqColor
+
 end
 end Fermion
--- a/HepLean/Tensors/ComplexLorentz/Examples.lean
+++ b/HepLean/Tensors/ComplexLorentz/Examples.lean
@ -45,13 +45,23 @@ example :
 lemma fin_three_expand {R : Type} (f : Fin 3 → R) : f = ![f 0, f 1, f 2]:= by
  funext x
  fin_cases x <;> rfl
-/-
+
+open Lean
+open Lean.Elab.Term
+
+open Lean
+open Lean.Meta
+open Lean.Elab
+open Lean.Elab.Term
+open Lean Meta Elab Tactic
+open IndexNotation
+
 example : True :=
-  let f :=
-    {Lorentz.coMetric |
-      μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ PauliMatrix.asConsTensor | ν α' β'}ᵀ
+  let f := {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ PauliMatrix.asConsTensor | ν α' β'}ᵀ
+  have h1 : {Lorentz.coMetric | μ ν = Lorentz.coMetric | μ ν}ᵀ := by
+    sorry
  sorry
-/
+
 end Fermion

 end
--- a/HepLean/Tensors/ComplexLorentz/Lemmas.lean
+++ b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
@ -0,0 +1,91 @@
+/-
+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.Elab
+import HepLean.Tensors.ComplexLorentz.Basic
+import Mathlib.LinearAlgebra.TensorProduct.Basis
+/-!
+
+## Lemmas related to complex Lorentz tensors.
+
+-/
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+open TensorTree
+open OverColor.Discrete
+noncomputable section
+
+namespace Fermion
+
+lemma coMetric_expand : {Lorentz.coMetric | μ ν}ᵀ.tensor =
+    (PiTensorProduct.tprod ℂ (fun i => Fin.cases (Lorentz.complexCoBasis (Sum.inl 0))
+        (fun i => Fin.cases (Lorentz.complexCoBasis (Sum.inl 0)) (fun i => i.elim0) i) i) :
+        complexLorentzTensor.F.obj (OverColor.mk ![Color.down, Color.down]))
+    - (PiTensorProduct.tprod ℂ (fun i => Fin.cases (Lorentz.complexCoBasis (Sum.inr 0))
+        (fun i => Fin.cases (Lorentz.complexCoBasis (Sum.inr 0)) (fun i => i.elim0) i) i) :
+        complexLorentzTensor.F.obj (OverColor.mk ![Color.down, Color.down]))
+    - (PiTensorProduct.tprod ℂ (fun i => Fin.cases (Lorentz.complexCoBasis (Sum.inr 1))
+        (fun i => Fin.cases (Lorentz.complexCoBasis (Sum.inr 1)) (fun i => i.elim0) i) i) :
+        complexLorentzTensor.F.obj (OverColor.mk ![Color.down, Color.down]))
+    - (PiTensorProduct.tprod ℂ (fun i => Fin.cases (Lorentz.complexCoBasis (Sum.inr 2))
+        (fun i => Fin.cases (Lorentz.complexCoBasis (Sum.inr 2)) (fun i => i.elim0) i) i) :
+        complexLorentzTensor.F.obj (OverColor.mk ![Color.down, Color.down])) := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Functor.id_obj, Fin.isValue]
+  erw [Lorentz.coMetric_apply_one, Lorentz.coMetricVal_expand_tmul]
+  simp only [Fin.isValue, map_sub]
+  congr 1
+  congr 1
+  congr 1
+  all_goals
+    erw [pairIsoSep_tmul]
+    rfl
+
+lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, perm_tensor]
+  rw [coMetric_expand]
+  simp only [TensorStruct.F, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, Fin.isValue,
+    map_sub]
+  congr 1
+  congr 1
+  congr 1
+  all_goals
+    erw [OverColor.lift.map_tprod]
+    apply congrArg
+    funext i
+    match i with
+    | (0 : Fin 2) => rfl
+    | (1 : Fin 2) => rfl
+
+open TensorTree in
+
+lemma coMetric_prod_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V)
+    (S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V)
+    (hA : (twoNodeE complexLorentzTensor Color.up Color.up A).tensor =
+      (TensorTree.neg (perm
+      (OverColor.equivToHomEq (Equality.finMapToEquiv ![1, 0] ![1, 0]) (by decide))
+      (twoNodeE complexLorentzTensor  Color.up  Color.up A))).tensor)
+    (hs : {S | μ ν = S | ν μ}ᵀ) : {A | μ ν ⊗ S | μ ν}ᵀ.tensor = 0 := by
+  have h1 : {A | μ ν ⊗ S | μ ν}ᵀ.tensor = - {A | μ ν ⊗ S | μ ν}ᵀ.tensor := by
+    nth_rewrite 1 [contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_fst hA))]
+    rw [contr_tensor_eq (contr_tensor_eq (neg_fst_prod _ _))]
+    rw [contr_tensor_eq (neg_contr _)]
+    rw [neg_contr]
+    rw [neg_tensor]
+    apply congrArg
+    sorry
+    sorry
+
+end Fermion
+
+end
--- a/HepLean/Tensors/OverColor/Discrete.lean
+++ b/HepLean/Tensors/OverColor/Discrete.lean
@ -7,6 +7,7 @@ import HepLean.Tensors.OverColor.Basic
 import HepLean.Tensors.OverColor.Lift
 import HepLean.Mathematics.PiTensorProduct
 import HepLean.Tensors.OverColor.Iso
+import LLMLean
 /-!

 # Discrete color category
@ -48,6 +49,64 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverCol
    fin_cases x
    rfl

+def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ≅
+    (lift.obj F).obj (OverColor.mk ![c1,c2]) := by
+  symm
+  apply ((lift.obj F).mapIso fin2Iso).trans
+  apply ((lift.obj F).μIso _ _).symm.trans
+  apply tensorIso ?_ ?_
+  · symm
+    apply (forgetLiftApp F c1).symm.trans
+    refine (lift.obj F).mapIso (mkIso ?_)
+    funext x
+    fin_cases x
+    rfl
+  · symm
+    apply (forgetLiftApp F c2).symm.trans
+    refine (lift.obj F).mapIso (mkIso ?_)
+    funext x
+    fin_cases x
+    rfl
+
+lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discrete.mk c2)) :
+    (pairIsoSep F).hom.hom (x ⊗ₜ[k] y) =
+    PiTensorProduct.tprod k (Fin.cases x (Fin.cases y (fun i  => Fin.elim0 i))) := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Action.instMonoidalCategory_tensorObj_V,
+    pairIsoSep, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
+    forgetLiftApp, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom,
+    tensorIso_inv, Iso.trans_inv, Iso.symm_inv, Functor.mapIso_hom, tensor_comp,
+    MonoidalFunctor.μIso_hom, Functor.mapIso_inv, Category.assoc,
+    LaxMonoidalFunctor.μ_natural_assoc, Action.comp_hom, Action.instMonoidalCategory_tensorHom_hom,
+    Action.mkIso_inv_hom, LinearEquiv.toModuleIso_inv, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    ModuleCat.coe_comp, Function.comp_apply, ModuleCat.MonoidalCategory.hom_apply, Functor.id_obj]
+  erw [forgetLiftAppV_symm_apply F c1, forgetLiftAppV_symm_apply F c2]
+  change ((lift.obj F).map fin2Iso.inv).hom
+    (((lift.obj F).map ((mkIso _).hom ⊗ (mkIso _).hom)).hom
+      (((lift.obj F).μ (mk fun _ => c1) (mk fun _ => c2)).hom
+        (((PiTensorProduct.tprod k) fun _ => x) ⊗ₜ[k] (PiTensorProduct.tprod k) fun x => y))) = _
+  rw [lift.obj_μ_tprod_tmul F (mk fun _ => c1) (mk fun _ => c2)]
+  change ((lift.obj F).map fin2Iso.inv).hom
+    (((lift.obj F).map ((mkIso _).hom ⊗ (mkIso _).hom)).hom
+      ((PiTensorProduct.tprod k) _))  = _
+  rw [lift.map_tprod]
+  change ((lift.obj F).map fin2Iso.inv).hom ((PiTensorProduct.tprod k) fun i => _) = _
+  rw [lift.map_tprod]
+  congr
+  funext i
+  match i with
+  | (0 : Fin 2) =>
+    simp [fin2Iso, HepLean.PiTensorProduct.elimPureTensor, mkIso, mkSum]
+    exact (LinearEquiv.eq_symm_apply _).mp rfl
+  | (1 : Fin 2) =>
+    simp [fin2Iso, HepLean.PiTensorProduct.elimPureTensor, mkIso, mkSum]
+    exact (LinearEquiv.eq_symm_apply _).mp rfl
+
+
+
+
+
+
 /-- The functor taking `c` to `F c ⊗ F (τ c)`. -/
 def pairτ (τ : C → C) : Discrete C ⥤ Rep k G :=
  F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F)
--- a/HepLean/Tensors/OverColor/Iso.lean
+++ b/HepLean/Tensors/OverColor/Iso.lean
@ -26,6 +26,11 @@ open MonoidalCategory
 def equivToIso {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ e.symm) :=
  Hom.toIso (Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl))

+def equivToHom {c : X → C} (e : X ≃ Y) : mk c ⟶ mk (c ∘ e.symm) :=
+  (equivToIso e).hom
+
+
+
 /-- Given a map `X ⊕ Y → C`, the isomorphism `mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr)`. -/
 def mkSum (c : X ⊕ Y → C) : mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr) :=
  Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
@ -40,6 +45,10 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
    subst h
    rfl))

+def equivToHomEq {c : X → C} {c1 : Y → C} (e : X ≃ Y) (h : ∀ x, c1 x = (c ∘ e.symm ) x := by decide) :
+    mk c ⟶ mk c1 :=
+  (equivToHom e).trans (mkIso (funext fun x => (h x).symm)).hom
+
 /-- The isomorphism splitting a `mk c` for `Fin 2 → C` into the tensor product of
  the `Fin 1 → C` maps defined by `c 0` and `c 1`. -/
 def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
--- a/HepLean/Tensors/OverColor/Lift.lean
+++ b/HepLean/Tensors/OverColor/Lift.lean
@ -646,6 +646,25 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ MonoidalFunctor (OverColor
    erw [lift.mapApp'_tprod]
    rfl

+namespace lift
+
+lemma map_tprod (F :  Discrete C ⥤ Rep k G ) {X Y : OverColor C} (f : X ⟶ Y)
+    (p : (i : X.left) → F.obj (Discrete.mk <| X.hom i)) :
+    ((lift.obj F).map f).hom (PiTensorProduct.tprod k p) =
+    PiTensorProduct.tprod k fun (i : Y.left) => discreteFunctorMapEqIso F
+    (OverColor.Hom.toEquiv_comp_inv_apply f i) (p ((OverColor.Hom.toEquiv f).symm i)) := by
+  simp [lift, obj']
+  erw [objMap'_tprod]
+
+lemma obj_μ_tprod_tmul (F :  Discrete C ⥤ Rep k G ) (X Y : OverColor C)
+    (p : (i : X.left) → (F.obj (Discrete.mk <| X.hom i)))
+    (q : (i : Y.left) → F.obj (Discrete.mk <| Y.hom i)) :
+    ((lift.obj F).μ X Y).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 μ_tmul_tprod F p q
+
+end lift
 /-- The natural inclusion of `Discrete C` into `OverColor C`. -/
 def incl : Discrete C ⥤ OverColor C := Discrete.functor fun c =>
  OverColor.mk (fun (_ : Fin 1) => c)
@ -670,6 +689,12 @@ def forgetLiftAppV (c : C) : ((lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) =>
  (PiTensorProduct.subsingletonEquiv 0 :
    (⨂[k] (_ : Fin 1), (F.obj (Discrete.mk c))) ≃ₗ[k] F.obj (Discrete.mk c))

+@[simp]
+lemma forgetLiftAppV_symm_apply (c : C) (x : (F.obj (Discrete.mk c)).V) :
+    (forgetLiftAppV F c).symm x = PiTensorProduct.tprod k (fun _ => x) := by
+  simp [forgetLiftAppV]
+  erw [PiTensorProduct.subsingletonEquiv_symm_apply]
+
 /-- The `forgetLiftAppV` function takes an object `c` of type `C` and returns a isomorphism
 between the objects obtained by applying the lift of `F` and that obtained by applying
 `F`. -/
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@ -7,6 +7,7 @@ import HepLean.Tensors.OverColor.Iso
 import HepLean.Tensors.OverColor.Discrete
 import HepLean.Tensors.OverColor.Lift
 import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
+import LLMLean
 /-!

 ## Tensor trees
@ -119,7 +120,7 @@ inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Typ
  | vecNode {c : S.C} (v : S.FDiscrete.obj (Discrete.mk c)) : TensorTree S ![c]
  /-- A node consisting of a two tensor. -/
  | twoNode {c1 c2 : S.C}
-    (v : S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
+    (v : (S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)).V) :
    TensorTree S ![c1, c2]
  /-- A node consisting of a three tensor. -/
  | threeNode {c1 c2 c3 : S.C}
@ -147,6 +148,8 @@ inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Typ
  | 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)
  | smul {n : ℕ} {c : Fin n → S.C} : S.k → TensorTree S c → TensorTree S c
+  /-- The negative of a node. -/
+  | neg {n : ℕ} {c : Fin n → S.C} : TensorTree S c → TensorTree S c
  | contr {n : ℕ} {c : Fin n.succ.succ → S.C} : (i : Fin n.succ.succ) →
    (j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c →
    TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
@ -163,7 +166,7 @@ open TensorProduct

 /-- The node `twoNode` of a tensor tree, with all arguments explicit. -/
 abbrev twoNodeE (S : TensorStruct) (c1 c2 : S.C)
-    (v : S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
+    (v : (S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)).V) :
    TensorTree S ![c1, c2] := twoNode v

 /-- The node `constTwoNodeE` of a tensor tree, with all arguments explicit. -/
@ -189,6 +192,7 @@ def size : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → ℕ := fun
  | constThreeNode _ => 1
  | add t1 t2 => t1.size + t2.size + 1
  | perm _ t => t.size + 1
+  | neg t => t.size + 1
  | smul _ t => t.size + 1
  | prod t1 t2 => t1.size + t2.size + 1
  | contr _ _ _ t => t.size + 1
@ -200,17 +204,104 @@ noncomputable section
  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
+  | constTwoNode t => (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom (t.hom (1 : S.k))
  | add t1 t2 => t1.tensor + t2.tensor
  | perm σ t => (S.F.map σ).hom t.tensor
+  | neg t => - t.tensor
  | smul a t => a • t.tensor
  | prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
    ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor))
  | contr i j h t => (S.contrMap _ i j h).hom t.tensor
  | _ => 0

-lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :
+/-!
+
+## Tensor on different nodes.
+
+-/
+
+@[simp]
+lemma tensoreNode_tensor {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :
    (tensorNode T).tensor = T := rfl

+@[simp]
+lemma constTwoNode_tensor {c1 c2 : S.C}
+    (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
+    (constTwoNode v).tensor = (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom (v.hom (1 : S.k)) :=
+  rfl
+
+lemma prod_tensor {c1 : Fin n → S.C} {c2 : Fin m → S.C} (t1 : TensorTree S c1) (t2 : TensorTree S c2) :
+    (prod t1 t2).tensor = (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
+    ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor))  := rfl
+
+lemma add_tensor (t1 t2 : TensorTree S c) : (add t1 t2).tensor = t1.tensor + t2.tensor := rfl
+
+lemma perm_tensor (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) :
+    (perm σ t).tensor = (S.F.map σ).hom t.tensor := rfl
+
+lemma contr_tensor {n : ℕ} {c : Fin n.succ.succ → S.C}  {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = S.τ (c i)}
+    (t : TensorTree S c) : (contr i j h t).tensor = (S.contrMap c i j h).hom t.tensor := rfl
+
+lemma neg_tensor (t : TensorTree S c) : (neg t).tensor = - t.tensor := rfl
+
+/-!
+
+## Equality of tensors and rewrites.
+
+-/
+lemma contr_tensor_eq {n : ℕ} {c : Fin n.succ.succ → S.C} {T1 T2 : TensorTree S c}
+    (h : T1.tensor = T2.tensor) {i : Fin n.succ.succ} {j : Fin n.succ}
+    {h' : c (i.succAbove j) = S.τ (c i)} :
+    (contr i j h' T1).tensor = (contr i j h' T2).tensor := by
+  simp only [Nat.succ_eq_add_one, contr_tensor]
+  rw [h]
+
+lemma prod_tensor_eq_fst {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
+    {T1  T1' : TensorTree S c} { T2 : TensorTree S c1}
+    (h : T1.tensor = T1'.tensor) :
+    (prod T1 T2).tensor = (prod T1' T2).tensor := by
+  simp [prod_tensor]
+  rw [h]
+
+lemma prod_tensor_eq_snd {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
+    {T1 : TensorTree S c} {T2 T2' : TensorTree S c1}
+    (h : T2.tensor = T2'.tensor) :
+    (prod T1 T2).tensor = (prod T1 T2').tensor := by
+  simp [prod_tensor]
+  rw [h]
+
+/-!
+
+## Negation lemmas
+
+We define the simp lemmas here so that negation is always moved to the top of the tree.
+-/
+
+@[simp]
+lemma neg_neg (t : TensorTree S c) : (neg (neg t)).tensor = t.tensor := by
+  simp only [neg_tensor, _root_.neg_neg]
+
+@[simp]
+lemma neg_fst_prod  {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
+    (T2 : TensorTree S c2) :
+    (prod (neg T1) T2).tensor = (neg (prod T1 T2)).tensor := by
+  simp only [prod_tensor, Functor.id_obj, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, neg_tensor, neg_tmul, map_neg]
+
+@[simp]
+lemma neg_snd_prod  {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
+    (T2 : TensorTree S c2) :
+    (prod T1 (neg T2)).tensor = (neg (prod T1 T2)).tensor := by
+  simp only [prod_tensor, Functor.id_obj, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, neg_tensor, tmul_neg, map_neg]
+
+@[simp]
+lemma neg_contr {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = S.τ (c i)}
+    (t : TensorTree S c) : (contr i j h (neg t)).tensor = (neg (contr i j h t)).tensor := by
+  simp only [Nat.succ_eq_add_one, contr_tensor, neg_tensor, map_neg]
+
 end

 end TensorTree
--- a/HepLean/Tensors/Tree/Dot.lean
+++ b/HepLean/Tensors/Tree/Dot.lean
@ -49,6 +49,10 @@ def dotString (m : ℕ) (nt : ℕ) : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTr
    let edge2 := " node" ++ toString m ++ " -> node" ++ toString (2 * t1.size + m + 2) ++ ";\n"
    prodNode ++ dotString (m + 1) nt t1 ++ dotString (2 * t1.size + m + 2) (nt + 1) t2
      ++ edge1 ++ edge2
+  | neg t =>
+    let negNode := " node" ++ toString m ++ " [label=\"neg\", shape=box];\n"
+    let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
+    negNode ++ dotString (m + 1) nt t ++ edge1
  | smul k t =>
    let smulNode := " node" ++ toString m ++ " [label=\"smul\", shape=box];\n"
    let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@ -108,6 +108,9 @@ syntax "(" tensorExpr ")" : tensorExpr
 /-- Scalar multiplication for tensors. -/
 syntax term "•" tensorExpr : tensorExpr

+/-- Equality. -/
+syntax tensorExpr "=" tensorExpr : tensorExpr
+
 namespace TensorNode

 /-!
@ -160,6 +163,17 @@ def stringToType (str : String) : TermElabM Expr := do
  | Except.error _ => throwError "Could not create type from string (stringToType). "
  | Except.ok stx => elabTerm stx none

+/-- The construction of an expression corresponding to the type of a given string once parsed. -/
+def stringToTerm (str : String) : TermElabM Term := do
+  let env ← getEnv
+  let stx := Parser.runParserCategory env `term str
+  match stx with
+  | Except.error _ => throwError "Could not create type from string (stringToType). "
+  | Except.ok stx =>
+    match stx with
+    | `(term| $e) => return e
+
+
 /-- The syntax associated with a terminal node of a tensor tree. -/
 def termNodeSyntax (T : Term) : TermElabM Term := do
  let expr ← elabTerm T none
@ -167,6 +181,7 @@ def termNodeSyntax (T : Term) : TermElabM Term := do
  let strType := toString type
  let n := (String.splitOn strType "CategoryTheory.MonoidalCategoryStruct.tensorObj").length
  let const := (String.splitOn strType "Quiver.Hom").length
+  println! "n: {n}, const: {const}"
  match n, const with
  | 1, 1 =>
    match type with
@ -183,14 +198,26 @@ def termNodeSyntax (T : Term) : TermElabM Term := do
    | true => return Syntax.mkApp (mkIdent ``TensorTree.twoNodeE)
                #[mkIdent ``Fermion.complexLorentzTensor,
                mkIdent ``Fermion.Color.upL, mkIdent ``Fermion.Color.up, T]
-    | _ => return Syntax.mkApp (mkIdent ``TensorTree.twoNode) #[T]
+    | _ =>
+    match ← isDefEq type (← stringToType "ModuleCat.carrier
+      (Lorentz.complexContr ⊗ Lorentz.complexContr).V") with
+    | true =>
+      return Syntax.mkApp (mkIdent ``TensorTree.twoNodeE) #[mkIdent ``Fermion.complexLorentzTensor,
+        mkIdent ``Fermion.Color.up, mkIdent ``Fermion.Color.up, T]
+    | _ =>
+    match ← isDefEq type (← stringToType "ModuleCat.carrier
+      (Lorentz.complexCo ⊗ Lorentz.complexCo).V") with
+    | true =>
+      return Syntax.mkApp (mkIdent ``TensorTree.twoNodeE) #[mkIdent ``Fermion.complexLorentzTensor,
+        mkIdent ``Fermion.Color.down, mkIdent ``Fermion.Color.down, T]
+    | _ =>
+      return Syntax.mkApp (mkIdent ``TensorTree.twoNode) #[T]
  | 3, 1 => return Syntax.mkApp (mkIdent ``TensorTree.threeNode) #[T]
  | 1, 2 => return Syntax.mkApp (mkIdent ``TensorTree.constVecNode) #[T]
  | 2, 2 =>
    match ← isDefEq type (← stringToType
      "𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Lorentz.complexCo ⊗ Lorentz.complexCo") with
    | true =>
-      println! "here"
      return Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[
        mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.down,
        mkIdent ``Fermion.Color.down, T]
@ -237,11 +264,25 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
  let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x)
  return ind.filter (fun x => indFilt.count x ≤ 1)

+def toPairs (l : List ℕ) : List (ℕ × ℕ) :=
+  match l with
+  | x1 :: x2 :: xs => (x1, x2) :: toPairs xs
+  | []             => []
+  | [x]     => [(x, 0)]
+
+def contrListAdjust (l : List (ℕ × ℕ)) : List (ℕ × ℕ ) :=
+  let l' := l.bind (fun p => [p.1, p.2])
+  let l'' := List.mapAccumr
+    (fun  x  (prev : List ℕ) =>
+      let e := prev.countP (fun y => y < x)
+      (x :: prev, x - e)) l'.reverse []
+  toPairs l''.2.reverse
+
 /-- 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), mkIdent ``rfl, T']) T
+  (contrListAdjust l).foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr)
+    #[Syntax.mkNumLit (toString x0),
+    Syntax.mkNumLit (toString x1), mkIdent ``rfl, T']) T

 /-- Creates the syntax associated with a tensor node. -/
 def syntaxFull (stx : Syntax) : TermElabM Term := do
@ -250,7 +291,7 @@ def syntaxFull (stx : Syntax) : TermElabM Term := do
      let indices ← getIndices stx
      let rawIndex ← getNoIndicesExact T
      if indices.length ≠ rawIndex then
-        throwError "The number of indices does not match the tensor {T}."
+        throwError "The expected number of indices {rawIndex} does not match the tensor {T}."
      let tensorNodeSyntax ← termNodeSyntax T
      let evalSyntax := evalSyntax (← getEvalPos stx) tensorNodeSyntax
      let contrSyntax := contrSyntax (← getContrPos stx) evalSyntax
@ -303,8 +344,8 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do

 /-- 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), mkIdent ``rfl, T']) T
+  (TensorNode.contrListAdjust l).foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr)
+    #[Syntax.mkNumLit (toString x0), Syntax.mkNumLit (toString x1), mkIdent ``rfl, T']) T

 /-- The syntax associated with a product of tensors. -/
 def prodSyntax (T1 T2 : Term) : Term :=
@ -316,6 +357,8 @@ partial def syntaxFull (stx : Syntax) : TermElabM Term := do
  | `(tensorExpr| $_:term | $[$args]*) => TensorNode.syntaxFull stx
  | `(tensorExpr| $a:tensorExpr ⊗ $b:tensorExpr) => do
      let prodSyntax := prodSyntax (← syntaxFull a) (← syntaxFull b)
+      println! (← getContrPos stx)
+      println! TensorNode.contrListAdjust (← getContrPos stx)
      let contrSyntax := contrSyntax (← getContrPos stx) prodSyntax
      return contrSyntax
  | `(tensorExpr| ($a:tensorExpr)) => do
@ -323,6 +366,90 @@ partial def syntaxFull (stx : Syntax) : TermElabM Term := do
  | _ =>
    throwError "Unsupported tensor expression syntax in elaborateTensorNode: {stx}"

+end ProdNode
+
+partial def getIndicesFull (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
+  match stx with
+  | `(tensorExpr| $_:term | $[$args]*) => do
+      return (← TensorNode.withoutContr stx)
+  | `(tensorExpr| $_:tensorExpr ⊗ $_:tensorExpr) => do
+      return (← ProdNode.withoutContr stx)
+  | `(tensorExpr| ($a:tensorExpr)) => do
+      return (← getIndicesFull a)
+  | _ =>
+    throwError "Unsupported tensor expression syntax in getIndicesProd: {stx}"
+
+namespace Equality
+
+/-!
+
+## For equality.
+
+-/
+
+/-- Gets the indices associated with the LHS of an equality. -/
+partial def getIndicesLeft (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
+  match stx with
+  | `(tensorExpr| $a:tensorExpr = $_:tensorExpr) => do
+      return (← getIndicesFull a)
+  | _ =>
+    throwError "Unsupported tensor expression syntax in getIndicesProd: {stx}"
+
+/-- Gets the indices associated with the RHS of an equality. -/
+partial def getIndicesRight (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
+  match stx with
+  | `(tensorExpr| $_:tensorExpr = $a:tensorExpr) => do
+      return (← getIndicesFull a)
+  | _ =>
+    throwError "Unsupported tensor expression syntax in getIndicesProd: {stx}"
+
+def getPermutation (l1 l2 : List (TSyntax `indexExpr)) : TermElabM (List (ℕ)) := do
+  let l1' ← l1.mapM (fun x => indexToIdent x)
+  let l2' ← l2.mapM (fun x => indexToIdent x)
+  let l1enum := l1'.enum
+  let l2'' := l2'.filterMap (fun x => l1enum.find? (fun y => Lean.TSyntax.getId y.2 = Lean.TSyntax.getId x))
+  return l2''.map fun x => x.1
+
+def finMapToEquiv (f1 f2 : Fin n → Fin n) (h : ∀ x, f1 (f2 x) = x := by decide)
+  (h' : ∀ x, f2 (f1 x) = x := by decide) : Fin n ≃ Fin n where
+  toFun := f1
+  invFun := f2
+  left_inv := h'
+  right_inv := h
+
+def getPermutationSyntax (l1 l2 : List (TSyntax `indexExpr)) : TermElabM Term := do
+  let lPerm ← getPermutation l1 l2
+  let l2Perm ← getPermutation l1 l2
+  let permString := "![" ++ String.intercalate  ", " (lPerm.map toString) ++ "]"
+  let perm2String := "![" ++ String.intercalate  ", " (l2Perm.map toString) ++ "]"
+  let P1 ← TensorNode.stringToTerm permString
+  let P2 ← TensorNode.stringToTerm perm2String
+  let stx := Syntax.mkApp (mkIdent ``finMapToEquiv) #[P1, P2]
+  return stx
+
+def equalSyntax (permSyntax : Term) (T1 T2 : Term) : TermElabM Term := do
+  let X1 := Syntax.mkApp (mkIdent ``TensorTree.tensor) #[T1]
+  let P := Syntax.mkApp (mkIdent ``OverColor.equivToHomEq) #[permSyntax]
+  let X2' := Syntax.mkApp (mkIdent ``TensorTree.perm) #[P, T2]
+  let X2 := Syntax.mkApp (mkIdent ``TensorTree.tensor) #[X2']
+  return Syntax.mkApp (mkIdent ``Eq) #[X1, X2]
+
+/-- Creates the syntax associated with a tensor node. -/
+partial def syntaxFull (stx : Syntax) : TermElabM Term := do
+  match stx with
+  | `(tensorExpr| $_:term | $[$args]*) => ProdNode.syntaxFull stx
+  | `(tensorExpr| $_:tensorExpr ⊗ $_:tensorExpr) => ProdNode.syntaxFull stx
+  | `(tensorExpr| ($a:tensorExpr)) => do
+      return (← syntaxFull a)
+  | `(tensorExpr| $a:tensorExpr = $b:tensorExpr) => do
+      let indicesLeft ← getIndicesLeft stx
+      let indicesRight ← getIndicesRight stx
+      let permSyntax ← getPermutationSyntax indicesLeft indicesRight
+      let equalSyntax ← equalSyntax permSyntax (← syntaxFull a) (← syntaxFull b)
+      return equalSyntax
+  | _ =>
+    throwError "Unsupported tensor expression syntax in elaborateTensorNode: {stx}"
+
 /-- An elaborator for tensor nodes. This is to be generalized. -/
 def elaborateTensorNode (stx : Syntax) : TermElabM Expr := do
  let tensorExpr ← elabTerm (← syntaxFull stx) none
@ -354,6 +481,6 @@ variable (𝓣 : TensorTree S c4)

 #check {(T4 | i j l a ⊗ T5 | i j k c d) ⊗ T5 | i1 i2 i3 e f}ᵀ
 -/
-end ProdNode
+end Equality

 end TensorTree