From 9cae20c114d2563bd86a8b8aaf22cb8e7e1448c3 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 28 Oct 2024 14:05:38 +0000
Subject: [PATCH] feat: Lemmas regarding bispinors

---
 .../ComplexLorentz/Bispinors/Basic.lean       | 114 +++++++++++++++++-
 HepLean/Tensors/OverColor/Basic.lean          |   7 ++
 HepLean/Tensors/OverColor/Iso.lean            |   4 +
 .../Tensors/Tree/NodeIdentities/Basic.lean    |  27 +++++
 .../Tensors/Tree/NodeIdentities/Congr.lean    |  53 ++++++++
 5 files changed, 204 insertions(+), 1 deletion(-)
 create mode 100644 HepLean/Tensors/Tree/NodeIdentities/Congr.lean

diff --git a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
index 035e527..52d8e62 100644
--- a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.ComplexLorentz.PauliLower
+import HepLean.Tensors.Tree.NodeIdentities.ProdContr
+import HepLean.Tensors.Tree.NodeIdentities.Congr
+import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
 /-!
 
 ## Bispinors
@@ -33,6 +36,54 @@ lemma tensorNode_contrBispinorUp (p : complexContr) :
     (tensorNode (contrBispinorUp p)).tensor = {p | μ ⊗ pauliCo | μ α β}ᵀ.tensor := by
   rw [contrBispinorUp, tensorNode_tensor]
 
+/-- An up-bispinor is equal to `pauliCo | μ α β ⊗ p | μ`-/
+lemma contrBispinorUp_eq_pauliCo_self (p : complexContr) :
+    {contrBispinorUp p | α β = pauliCo | μ α β ⊗ p | μ}ᵀ := by
+  rw [tensorNode_contrBispinorUp]
+  conv_lhs =>
+    rw [contr_tensor_eq <| prod_comm _ _ _ _]
+    rw [perm_contr]
+    rw [perm_tensor_eq <| contr_swap _ _]
+    rw [perm_perm]
+  apply perm_congr
+  · apply OverColor.Hom.ext
+    ext x
+    match x with
+    | (0 : Fin 2) => rfl
+    | (1 : Fin 2)  => rfl
+  · rfl
+
+set_option maxRecDepth 2000 in
+lemma altRightMetric_contr_contrBispinorUp_assoc (p : complexContr) :
+    {Fermion.altRightMetric | β β' ⊗ contrBispinorUp p | α β =
+    Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β ⊗ p | μ}ᵀ := by
+  conv_lhs =>
+    rw [contr_tensor_eq <| prod_tensor_eq_snd <| contrBispinorUp_eq_pauliCo_self _]
+    rw [contr_tensor_eq <| prod_perm_right  _ _ _ _]
+    rw [perm_contr]
+    rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_assoc _ _ _ _ _ _]
+    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+  conv_rhs =>
+    rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    erw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_contr _ _ _]
+    rw [perm_perm]
+  apply perm_congr (_) rfl
+  · apply OverColor.Hom.fin_ext
+    intro i
+    fin_cases i
+    exact rfl
+    exact rfl
+
 /-- A bispinor `pₐₐ` created from a lorentz vector `p^μ`. -/
 def contrBispinorDown (p : complexContr) :=
   {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
@@ -45,9 +96,70 @@ lemma tensorNode_contrBispinorDown (p : complexContr) :
     Fermion.altRightMetric | β β' ⊗ (contrBispinorUp p) | α β}ᵀ.tensor := by
   rw [contrBispinorDown, tensorNode_tensor]
 
+set_option maxRecDepth 10000 in
+lemma contrBispinorDown_eq_metric_contr_contrBispinorUp  (p : complexContr) :
+    {contrBispinorDown p | α' β' = Fermion.altLeftMetric | α α' ⊗
+    (Fermion.altRightMetric | β β' ⊗ contrBispinorUp p | α β)}ᵀ := by
+  rw [tensorNode_contrBispinorDown]
+  conv_lhs =>
+    rw [contr_tensor_eq <| contr_tensor_eq <| prod_assoc' _ _ _ _ _ _]
+    rw [contr_tensor_eq <| perm_contr _ _]
+    rw [perm_contr]
+    rw [perm_tensor_eq <| contr_contr _ _ _]
+    rw [perm_perm]
+  conv_rhs =>
+    rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _ ]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+  apply perm_congr
+  · apply OverColor.Hom.ext
+    ext x
+    match x with
+    | (0 : Fin 2) => rfl
+    | (1 : Fin 2) => rfl
+  · rfl
+
+set_option maxHeartbeats 400000 in
+set_option maxRecDepth 2000 in
+lemma contrBispinorDown_eq_contr_with_self (p : complexContr) :
+    {contrBispinorDown p | α' β' = (Fermion.altLeftMetric | α α' ⊗
+    (Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β)) ⊗ p | μ}ᵀ := by
+  rw [contrBispinorDown_eq_metric_contr_contrBispinorUp]
+  conv_lhs =>
+    rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| altRightMetric_contr_contrBispinorUp_assoc _]
+    rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_right _ _ _ _]
+    rw [perm_tensor_eq <| perm_contr _ _ ]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <|
+        prod_assoc _ _ _ _ _ _]
+    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+  conv =>
+    rhs
+    rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    erw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_contr _ _ _]
+    rw [perm_perm]
+  apply congrArg
+  apply congrFun
+  apply congrArg
+  apply OverColor.Hom.fin_ext
+  intro i
+  fin_cases i
+  exact rfl
+  exact rfl
+
 /-- Expansion of a `contrBispinorDown` into the original contravariant tensor nested
   between pauli matrices and metrics. -/
-lemma contrBispinorDown_full_nested (p : complexContr) :
+lemma contrBispinorDown_eq_metric_mul_self_mul_pauli (p : complexContr) :
     {contrBispinorDown p | α β}ᵀ.tensor = {Fermion.altLeftMetric | α α' ⊗
     Fermion.altRightMetric | β β' ⊗ (p | μ ⊗ pauliCo | μ α β)}ᵀ.tensor := by
   conv =>
diff --git a/HepLean/Tensors/OverColor/Basic.lean b/HepLean/Tensors/OverColor/Basic.lean
index 59f91a4..b7a2549 100644
--- a/HepLean/Tensors/OverColor/Basic.lean
+++ b/HepLean/Tensors/OverColor/Basic.lean
@@ -45,6 +45,7 @@ variable {C : Type} {f g h : OverColor C}
 lemma ext (m n : f ⟶ g) (h : m.hom = n.hom) : m = n := by
   apply CategoryTheory.Iso.ext h
 
+
 /-- 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
@@ -258,6 +259,12 @@ def mk (f : X → C) : OverColor C := Over.mk f
 lemma mk_hom (f : X → C) : (mk f).hom = f := rfl
 open MonoidalCategory
 
+lemma Hom.fin_ext {n : ℕ} {f g : Fin n → C} (σ σ' : OverColor.mk f ⟶ OverColor.mk g)
+    (h : ∀ (i : Fin n), σ.hom.left i = σ'.hom.left i) : σ = σ' := by
+  apply Hom.ext
+  ext i
+  apply h
+
 end OverColor
 
 end IndexNotation
diff --git a/HepLean/Tensors/OverColor/Iso.lean b/HepLean/Tensors/OverColor/Iso.lean
index 0811396..fcb83cd 100644
--- a/HepLean/Tensors/OverColor/Iso.lean
+++ b/HepLean/Tensors/OverColor/Iso.lean
@@ -61,6 +61,10 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
     subst h
     rfl))
 
+lemma mkIso_refl_hom {c : X → C} : (mkIso (by rfl : c =c)).hom = 𝟙 _ := by
+  simp [mkIso]
+  rfl
+
 @[simp]
 lemma equivToIso_mkIso_hom {c1 c2 : X → C} (h : c1 = c2) :
     Hom.toEquiv (mkIso h).hom = Equiv.refl _ := by
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
index 2553c16..35fdc31 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
@@ -115,6 +115,33 @@ lemma perm_eq_of_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
   change _ = (S.F.map σ.hom ≫ S.F.map σ.inv).hom _
   simp only [Iso.map_hom_inv_id, Action.id_hom, ModuleCat.id_apply]
 
+lemma perm_eq_iff_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
+    (σ : (OverColor.mk c) ⟶  (OverColor.mk c1))
+    {t : TensorTree S c} {t2 : TensorTree S c1} :
+    (perm σ t).tensor = t2.tensor ↔ t.tensor =
+    (perm (equivToHomEq (Hom.toEquiv σ).symm (fun x => Hom.toEquiv_comp_apply σ x)) t2).tensor := by
+  refine Iff.intro (fun h => ?_)  (fun h => ?_)
+  · simp [perm_tensor, ← h]
+    change _ = (S.F.map _ ≫ S.F.map _).hom _
+    rw [← S.F.map_comp]
+    have h1 : (σ ≫ equivToHomEq (Hom.toEquiv σ).symm (fun x => Hom.toEquiv_comp_apply σ x)) = 𝟙 _ := by
+      apply Hom.ext
+      ext x
+      change (Hom.toEquiv σ).symm ((Hom.toEquiv σ) x) = x
+      simp
+    rw [h1]
+    simp
+  · rw [perm_tensor, h]
+    change (S.F.map _ ≫ S.F.map _).hom _ = _
+    rw [← S.F.map_comp]
+    have h1 : (equivToHomEq (Hom.toEquiv σ).symm (fun x => Hom.toEquiv_comp_apply σ x) ≫ σ) = 𝟙 _ := by
+      apply Hom.ext
+      ext x
+      change (Hom.toEquiv σ) ((Hom.toEquiv σ).symm x) = x
+      simp
+    rw [h1]
+    simp
+
 /-!
 
 ## Vector based identities
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Congr.lean b/HepLean/Tensors/Tree/NodeIdentities/Congr.lean
new file mode 100644
index 0000000..cfccdf5
--- /dev/null
+++ b/HepLean/Tensors/Tree/NodeIdentities/Congr.lean
@@ -0,0 +1,53 @@
+/-
+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
+/-!
+
+## Congr results
+
+-/
+
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open OverColor
+open HepLean.Fin
+open TensorProduct
+
+namespace TensorTree
+
+variable {S : TensorSpecies}
+
+/-!
+
+## Congr results
+
+-/
+variable {n m : ℕ}
+
+lemma perm_congr {c1 : Fin n → S.C} {c2 : Fin m → S.C} {T T' : TensorTree S c1}
+    {σ σ' : OverColor.mk c1 ⟶ OverColor.mk c2}
+    (h : σ = σ') (hT : T.tensor = T'.tensor):
+    (perm σ T).tensor = (perm σ' T').tensor := by
+  rw [h]
+  simp only [perm_tensor, hT]
+
+lemma perm_update  {c1 : Fin n → S.C} {c2 : Fin m → S.C} {T  : TensorTree S c1}
+    {σ : OverColor.mk c1 ⟶ OverColor.mk c2} (σ' : OverColor.mk c1 ⟶ OverColor.mk c2)
+    (h : σ = σ') :
+    (perm σ T).tensor = (perm σ' T).tensor := by rw [h]
+
+lemma contr_congr {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ}
+    (i' : Fin n.succ.succ) {j : Fin n.succ} (j' : Fin n.succ)
+    {h : c (i.succAbove j) = S.τ (c i)} {t : TensorTree S c}
+     (hi : i = i' := by decide) (hj : j = j' := by decide)
+     :(contr i j h t).tensor =
+    (perm (mkIso (by rw [hi, hj])).hom (contr i' j' (by rw [← hi, ← hj, h]) t)).tensor := by
+  subst hi
+  subst hj
+  simp [perm_tensor, mkIso_refl_hom]
+
+end TensorTree