feat: Start permutation contraction comm

HepLean/Mathematics/Fin.lean

@@ -0,0 +1,245 @@
+/-
+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.LinearAlgebra.PiTensorProduct
+import Mathlib.Tactic.Polyrith
+import Mathlib.Tactic.Linarith
+/-!
+# Fin lemmas
+
+The purpose of this file is to define some results Fin currently
+in Mathlib.
+
+At some point these should either be up-streamed to Mathlib or replaced with definitions already
+in Mathlib.
+
+-/
+namespace HepLean.Fin
+
+open Fin
+variable {n : Nat}
+
+def predAboveI (i x : Fin n.succ.succ) : Fin n.succ :=
+  if h : x.val < i.val then
+    ⟨x.val, by omega⟩
+  else
+    ⟨x.val - 1, by
+      by_cases hx : x = 0
+      · omega
+      · omega⟩
+
+lemma predAboveI_self  (i : Fin n.succ.succ) : predAboveI i i = ⟨i.val - 1, by omega⟩ := by
+  simp [predAboveI]
+
+@[simp]
+lemma predAboveI_succAbove (i : Fin n.succ.succ) (x : Fin n.succ) :
+    predAboveI i (Fin.succAbove i x) = x := by
+  simp [predAboveI, Fin.succAbove, Fin.ext_iff]
+  split_ifs
+  · rfl
+  · rename_i h1 h2
+    simp [Fin.lt_def] at h1 h2
+    omega
+  · rfl
+lemma succsAbove_predAboveI {i x : Fin n.succ.succ} (h : i ≠ x) :
+    Fin.succAbove i (predAboveI i x) = x := by
+  simp [Fin.succAbove, predAboveI, Fin.ext_iff]
+  split_ifs
+  · rfl
+  · rename_i h1 h2
+    rw [Fin.lt_def] at h1 h2
+    simp
+    simp at h2
+    rw [Fin.le_def] at h2
+    omega
+  · rename_i h1 h2
+    simp at h1
+    rw [Fin.le_def] at h1
+    rw [Fin.lt_def] at h2
+    simp at h2
+    omega
+  · rename_i h1 h2
+    simp
+    simp at h1
+    rw [Fin.le_def] at h1
+    omega
+
+
+lemma predAbove_eq_iff {i x : Fin n.succ.succ} (h : i ≠ x) (y : Fin n.succ) :
+    y = predAboveI i x  ↔ i.succAbove y  = x := by
+  apply Iff.intro
+  · intro h
+    subst h
+    rw [succsAbove_predAboveI h]
+  · intro h
+    rw [← h]
+    simp
+
+lemma predAboveI_lt {i x : Fin n.succ.succ} (h : x.val < i.val) :
+    predAboveI i x = ⟨x.val, by omega⟩ := by
+  simp [predAboveI, h]
+
+lemma predAboveI_ge {i x : Fin n.succ.succ} (h : i.val < x.val) :
+    predAboveI i x = ⟨x.val - 1, by omega⟩ := by
+  simp [predAboveI, h]
+  omega
+
+/-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
+  `i`th component. -/
+def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
+  (finCongr (by omega : n.succ = i + 1 + (n - i))).trans <|
+  finSumFinEquiv.symm.trans <|
+  (Equiv.sumCongr (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin i) (Fin 1)))
+    (Equiv.refl (Fin (n-i)))).trans <|
+  (Equiv.sumAssoc (Fin 1) (Fin i) (Fin (n - i))).trans <|
+  Equiv.sumCongr (Equiv.refl (Fin 1)) (finSumFinEquiv.trans (finCongr (by omega)))
+
+lemma finExtractOne_apply_eq {n : ℕ} (i : Fin n.succ) :
+    finExtractOne i i = Sum.inl 0 := by
+  simp [finExtractOne]
+  have h1 : Fin.cast (finExtractOne.proof_1 i) i = Fin.castAdd ((n - ↑i) ) ⟨i.1, lt_add_one i.1⟩ := by
+    simp [Fin.ext_iff]
+  rw [h1, finSumFinEquiv_symm_apply_castAdd]
+  simp
+  have h2 : @Fin.mk (↑i + 1) ↑i (lt_add_one i.1) = Fin.natAdd i.val 1 := by
+    simp [Fin.ext_iff]
+  rw [h2, finSumFinEquiv_symm_apply_natAdd]
+  rfl
+
+lemma finExtractOne_symm_inr {n : ℕ} (i : Fin n.succ) :
+    (finExtractOne i).symm ∘ Sum.inr = i.succAbove := by
+  ext x
+  simp only [Nat.succ_eq_add_one, finExtractOne, Function.comp_apply, Equiv.symm_trans_apply,
+    finCongr_symm, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply,
+    Equiv.coe_refl, Sum.map_inr, finCongr_apply, Fin.coe_cast]
+  change (finSumFinEquiv
+    (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id
+    ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - i))).symm
+    (Sum.inr (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)))))).val = _
+  by_cases hi : x.1 < i.1
+  · have h1 : (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)) =
+        Sum.inl ⟨x, hi⟩ := by
+      rw [← finSumFinEquiv_symm_apply_castAdd]
+      apply congrArg
+      ext
+      simp
+    rw [h1]
+    simp only [Nat.succ_eq_add_one, Equiv.sumAssoc_symm_apply_inr_inl, Sum.map_inl,
+      Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.sumComm_symm, Equiv.sumComm_apply,
+      Sum.swap_inr, finSumFinEquiv_apply_left, Fin.castAdd_mk]
+    rw [Fin.succAbove]
+    split
+    · rfl
+    rename_i hn
+    simp_all only [Nat.succ_eq_add_one, not_lt, Fin.le_def, Fin.coe_castSucc, Fin.val_succ,
+      self_eq_add_right, one_ne_zero]
+    omega
+  · have h1 : (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)) =
+        Sum.inr ⟨x - i, by omega⟩ := by
+      rw [← finSumFinEquiv_symm_apply_natAdd]
+      apply congrArg
+      ext
+      simp only [Nat.succ_eq_add_one, Fin.coe_cast, Fin.natAdd_mk]
+      omega
+    rw [h1, Fin.succAbove]
+    split
+    · rename_i hn
+      simp_all [Fin.lt_def]
+    simp only [Nat.succ_eq_add_one, Equiv.sumAssoc_symm_apply_inr_inr, Sum.map_inr, id_eq,
+      finSumFinEquiv_apply_right, Fin.natAdd_mk, Fin.val_succ]
+    omega
+
+@[simp]
+lemma finExtractOne_symm_inr_apply {n : ℕ} (i : Fin n.succ) (x : Fin n) :
+    (finExtractOne i).symm (Sum.inr x) = i.succAbove x := calc
+  _ = ((finExtractOne i).symm ∘ Sum.inr) x := rfl
+  _ = i.succAbove x := by rw [finExtractOne_symm_inr]
+
+@[simp]
+lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
+    (finExtractOne i).symm (Sum.inl 0) = i := by
+  simp only [Nat.succ_eq_add_one, finExtractOne, Fin.isValue, Equiv.symm_trans_apply, finCongr_symm,
+    Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply, Equiv.coe_refl,
+    Sum.map_inl, id_eq, Equiv.sumAssoc_symm_apply_inl, Equiv.sumComm_symm, Equiv.sumComm_apply,
+    Sum.swap_inl, finSumFinEquiv_apply_right, finSumFinEquiv_apply_left, finCongr_apply]
+  ext
+  rfl
+
+
+def finExtractOnPermHom (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
+   Fin n.succ → Fin n.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
+
+lemma finExtractOnPermHom_inv (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
+  (finExtractOnPermHom (σ i) σ.symm) ∘ (finExtractOnPermHom i σ)  = id := by
+  funext x
+  simp [finExtractOnPermHom]
+  by_cases h : σ (i.succAbove x) < σ i
+  · rw [predAboveI_lt h, Fin.succAbove_of_castSucc_lt]
+    · simp
+    · simp_all [Fin.lt_def]
+  have hσ : σ (i.succAbove x) ≠ σ i := by
+    simp only [Nat.succ_eq_add_one, ne_eq, EmbeddingLike.apply_eq_iff_eq]
+    exact Fin.succAbove_ne i x
+  have hn : σ i < σ (i.succAbove x) := by omega
+  rw [predAboveI_ge hn]
+  rw [Fin.succAbove_of_le_castSucc]
+  · simp
+    trans  predAboveI i (σ.symm (σ (i.succAbove x)))
+    · congr
+      exact Nat.sub_add_cancel (Fin.lt_of_le_of_lt (Fin.zero_le (σ i)) hn)
+    simp
+  rw [Fin.le_def]
+  simp
+  omega
+
+def finExtractOnePerm (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
+    Fin n.succ ≃ Fin n.succ where
+  toFun x :=  finExtractOnPermHom i σ x
+  invFun x := finExtractOnPermHom (σ i) σ.symm x
+  left_inv x := by
+    simpa using congrFun (finExtractOnPermHom_inv i σ) x
+  right_inv x := by
+    simpa using congrFun (finExtractOnPermHom_inv (σ i) σ.symm) x
+
+
+/-- The equivalence of types `Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n` extracting
+  the `i` and `(i.succAbove j)`. -/
+def finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
+    Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n :=
+  (finExtractOne i).trans <|
+  (Equiv.sumCongr (Equiv.refl (Fin 1)) (finExtractOne j)).trans <|
+  (Equiv.sumAssoc (Fin 1) (Fin 1) (Fin n)).symm
+
+@[simp]
+lemma finExtractTwo_apply_fst {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
+    finExtractTwo i j i = Sum.inl (Sum.inl 0) := by
+  simp [finExtractTwo]
+  simp [finExtractOne_apply_eq]
+
+lemma finExtractTwo_symm_inr {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
+    (finExtractTwo i j).symm ∘ Sum.inr = i.succAbove ∘ j.succAbove := by
+  rw [finExtractTwo]
+  ext1 x
+  simp
+
+@[simp]
+lemma finExtractTwo_symm_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) :
+    (finExtractTwo i j).symm (Sum.inr x) = i.succAbove (j.succAbove x) := by
+  rw [finExtractTwo]
+  simp
+
+@[simp]
+lemma finExtractTwo_symm_inl_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
+    (finExtractTwo i j).symm (Sum.inl (Sum.inr 0)) = i.succAbove j := by
+  rw [finExtractTwo]
+  simp
+
+@[simp]
+lemma finExtractTwo_symm_inl_inl_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
+    (finExtractTwo i j).symm (Sum.inl (Sum.inl 0)) = i := by
+  rw [finExtractTwo]
+  simp
+
+end HepLean.Fin

HepLean/Tensors/OverColor/Basic.lean

@@ -42,6 +42,9 @@ namespace Hom
 
 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
@@ -75,6 +78,10 @@ lemma toEquiv_comp_inv_apply (m : f ⟶ g) (i : g.left) :
     f.hom ((OverColor.Hom.toEquiv m).symm i) = g.hom i := by
   simpa [toEquiv, types_comp] using congrFun m.inv.w i
 
+lemma toEquiv_comp_apply (m : f ⟶ g) (i : f.left) :
+    f.hom i = g.hom ((toEquiv m) i) := by
+  simpa [toEquiv, types_comp] using (congrFun m.hom.w i).symm
+
 /-- Given a morphism in `OverColor C`, the corresponding isomorphism. -/
 def toIso (m : f ⟶ g) : f ≅ g := {
   hom := m,
@@ -253,6 +260,8 @@ end monoidal
 /-- Make an object of `OverColor C` from a map `X → C`. -/
 def mk (f : X → C) : OverColor C := Over.mk f
 
+@[simp]
+lemma mk_hom (f : X → C) : (mk f).hom = f := rfl
 open MonoidalCategory
 
 end OverColor

HepLean/Tensors/OverColor/Iso.lean

@@ -5,6 +5,8 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.OverColor.Functors
 import HepLean.Tensors.OverColor.Lift
+import HepLean.Mathematics.Fin
+import LLMLean
 /-!
 
 ## Isomorphisms in the OverColor category
@@ -14,7 +16,7 @@ namespace IndexNotation
 namespace OverColor
 open CategoryTheory
 open MonoidalCategory
-
+open HepLean.Fin
 /-!
 
 ## Useful equivalences.
@@ -63,106 +65,149 @@ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
     fin_cases x
     rfl
 
-/-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
-  `i`th component. -/
-def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
-  (finCongr (by omega : n.succ = i + 1 + (n - i))).trans <|
-  finSumFinEquiv.symm.trans <|
-  (Equiv.sumCongr (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin i) (Fin 1)))
-    (Equiv.refl (Fin (n-i)))).trans <|
-  (Equiv.sumAssoc (Fin 1) (Fin i) (Fin (n - i))).trans <|
-  Equiv.sumCongr (Equiv.refl (Fin 1)) (finSumFinEquiv.trans (finCongr (by omega)))
-
-lemma finExtractOne_symm_inr {n : ℕ} (i : Fin n.succ) :
-    (finExtractOne i).symm ∘ Sum.inr = i.succAbove := by
-  ext x
-  simp only [Nat.succ_eq_add_one, finExtractOne, Function.comp_apply, Equiv.symm_trans_apply,
-    finCongr_symm, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply,
-    Equiv.coe_refl, Sum.map_inr, finCongr_apply, Fin.coe_cast]
-  change (finSumFinEquiv
-    (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id
-    ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - i))).symm
-    (Sum.inr (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)))))).val = _
-  by_cases hi : x.1 < i.1
-  · have h1 : (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)) =
-        Sum.inl ⟨x, hi⟩ := by
-      rw [← finSumFinEquiv_symm_apply_castAdd]
-      apply congrArg
-      ext
-      simp
-    rw [h1]
-    simp only [Nat.succ_eq_add_one, Equiv.sumAssoc_symm_apply_inr_inl, Sum.map_inl,
-      Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.sumComm_symm, Equiv.sumComm_apply,
-      Sum.swap_inr, finSumFinEquiv_apply_left, Fin.castAdd_mk]
-    rw [Fin.succAbove]
-    split
+def extractOne {n : ℕ} (i : Fin n.succ.succ)
+    {c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
+    mk (c1  ∘ Fin.succAbove ((Hom.toEquiv σ).symm i)) ⟶ mk (c2 ∘ Fin.succAbove i) :=
+  equivToHomEq ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))) (by
+    intro x
+    simp_all only [Nat.succ_eq_add_one, Function.comp_apply]
+    have h1 := Hom.toEquiv_comp_inv_apply σ (i.succAbove x)
+    simp at h1
+    rw [← h1]
+    apply congrArg
+    simp [finExtractOnePerm, finExtractOnPermHom]
+    erw [Equiv.apply_symm_apply]
+    rw [succsAbove_predAboveI]
     · rfl
-    rename_i hn
-    simp_all only [Nat.succ_eq_add_one, not_lt, Fin.le_def, Fin.coe_castSucc, Fin.val_succ,
-      self_eq_add_right, one_ne_zero]
-    omega
-  · have h1 : (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)) =
-        Sum.inr ⟨x - i, by omega⟩ := by
-      rw [← finSumFinEquiv_symm_apply_natAdd]
-      apply congrArg
-      ext
-      simp only [Nat.succ_eq_add_one, Fin.coe_cast, Fin.natAdd_mk]
-      omega
-    rw [h1, Fin.succAbove]
-    split
-    · rename_i hn
-      simp_all [Fin.lt_def]
-    simp only [Nat.succ_eq_add_one, Equiv.sumAssoc_symm_apply_inr_inr, Sum.map_inr, id_eq,
-      finSumFinEquiv_apply_right, Fin.natAdd_mk, Fin.val_succ]
-    omega
+    simp
+    erw [Equiv.apply_eq_iff_eq]
+    exact (Fin.succAbove_ne i x).symm)
 
 @[simp]
-lemma finExtractOne_symm_inr_apply {n : ℕ} (i : Fin n.succ) (x : Fin n) :
-    (finExtractOne i).symm (Sum.inr x) = i.succAbove x := calc
-  _ = ((finExtractOne i).symm ∘ Sum.inr) x := rfl
-  _ = i.succAbove x := by rw [finExtractOne_symm_inr]
-
-@[simp]
-lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
-    (finExtractOne i).symm (Sum.inl 0) = i := by
-  simp only [Nat.succ_eq_add_one, finExtractOne, Fin.isValue, Equiv.symm_trans_apply, finCongr_symm,
-    Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply, Equiv.coe_refl,
-    Sum.map_inl, id_eq, Equiv.sumAssoc_symm_apply_inl, Equiv.sumComm_symm, Equiv.sumComm_apply,
-    Sum.swap_inl, finSumFinEquiv_apply_right, finSumFinEquiv_apply_left, finCongr_apply]
-  ext
+lemma extractOne_homToEquiv {n : ℕ} (i : Fin n.succ.succ)
+    {c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
+    Hom.toEquiv (extractOne i σ) = (finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)) := by
   rfl
 
-/-- The equivalence of types `Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n` extracting
-  the `i` and `(i.succAbove j)`. -/
-def finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
-    Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n :=
-  (finExtractOne i).trans <|
-  (Equiv.sumCongr (Equiv.refl (Fin 1)) (finExtractOne j)).trans <|
-  (Equiv.sumAssoc (Fin 1) (Fin 1) (Fin n)).symm
+def extractTwo {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
+    {c1 c2 : Fin n.succ.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
+    mk (c1  ∘ Fin.succAbove ((Hom.toEquiv σ).symm i) ∘
+      Fin.succAbove (((Hom.toEquiv (extractOne i σ))).symm j)) ⟶
+    mk (c2 ∘ Fin.succAbove i ∘ Fin.succAbove j) :=
+  equivToHomEq (Equiv.refl _) (by simp) ≫ extractOne j (extractOne i σ) ≫
+  equivToHomEq (Equiv.refl _) (by simp)
 
-lemma finExtractTwo_symm_inr {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
-    (finExtractTwo i j).symm ∘ Sum.inr = i.succAbove ∘ j.succAbove := by
-  rw [finExtractTwo]
-  ext1 x
-  simp
+def extractTwoAux {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
+    {c c1 : Fin n.succ.succ.succ → C} (σ : mk c ⟶ mk c1) :
+    mk ((c ∘ ⇑(finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)).symm) ∘ Sum.inr) ⟶
+    mk ((c1 ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inr) :=
+  equivToHomEq (Equiv.refl _) (by simp) ≫ extractTwo i j σ ≫ equivToHomEq (Equiv.refl _) (by simp)
 
-@[simp]
-lemma finExtractTwo_symm_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) :
-    (finExtractTwo i j).symm (Sum.inr x) = i.succAbove (j.succAbove x) := by
-  rw [finExtractTwo]
-  simp
+def extractTwoAux' {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
+    {c c1 : Fin n.succ.succ.succ → C} (σ : mk c ⟶ mk c1) :
+  mk ((c ∘ ⇑(finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)).symm) ∘ Sum.inl) ⟶
+  mk ((c1 ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) :=
+  equivToHomEq (Equiv.refl _) (by
+    intro x
+    simp
+    match x with
+    | Sum.inl 0=>
+      simp
+      have h1 := Hom.toEquiv_comp_inv_apply σ i
+      simpa using h1.symm
+    | Sum.inr 0 =>
+      simp
+      have h1 := Hom.toEquiv_comp_inv_apply σ (i.succAbove j)
+      simp at h1
+      rw [← h1]
+      congr
+      simp [finExtractOnePerm, finExtractOnPermHom]
+      erw [Equiv.apply_symm_apply]
+      rw [succsAbove_predAboveI]
+      rfl
+      simp
+      erw [Equiv.apply_eq_iff_eq]
+      exact (Fin.succAbove_ne i j).symm)
 
-@[simp]
-lemma finExtractTwo_symm_inl_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
-    (finExtractTwo i j).symm (Sum.inl (Sum.inr 0)) = i.succAbove j := by
-  rw [finExtractTwo]
-  simp
-
-@[simp]
-lemma finExtractTwo_symm_inl_inl_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
-    (finExtractTwo i j).symm (Sum.inl (Sum.inl 0)) = i := by
-  rw [finExtractTwo]
+lemma extractTwo_finExtractTwo  {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
+    {c c1 : Fin n.succ.succ.succ → C} (σ : mk c ⟶ mk c1) :
+    σ ≫ (equivToIso (HepLean.Fin.finExtractTwo i j)).hom ≫ (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom =
+    (equivToIso (HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) (((Hom.toEquiv (extractOne i σ))).symm j))).hom
+    ≫ (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) (((Hom.toEquiv (extractOne i σ))).symm j)).symm)).hom
+    ≫ ((extractTwoAux' i j σ) ⊗ (extractTwoAux i j σ)) := by
+  apply IndexNotation.OverColor.Hom.ext
+  ext x
+  simp [CategoryStruct.comp,extractTwoAux', extractTwoAux, mkSum,equivToIso, Hom.toIso]
+  change ((finExtractTwo i j) ((Hom.toEquiv σ) x)) = Sum.map id ((finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
+            (finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))))
+    (((finExtractTwo ((Hom.toEquiv σ).symm i)
+    ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)) x))
+  simp [extractTwo]
+  obtain ⟨k, hk⟩ := (finExtractTwo ((Hom.toEquiv σ).symm i)
+      ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)).symm.surjective x
+  subst hk
   simp
+  match k with
+  | Sum.inl (Sum.inl 0) =>
+    simp
+  | Sum.inl (Sum.inr 0) =>
+    simp
+    have h1 : ((Hom.toEquiv σ)  (Fin.succAbove
+        ((Hom.toEquiv σ).symm i)
+        ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))) =
+        i.succAbove j := by
+      simp [finExtractOnePerm, finExtractOnPermHom]
+      erw [Equiv.apply_symm_apply]
+      rw [succsAbove_predAboveI]
+      exact Equiv.apply_symm_apply (Hom.toEquiv σ) (i.succAbove j)
+      simp
+      erw [Equiv.apply_eq_iff_eq]
+      exact (Fin.succAbove_ne i j).symm
+    rw [h1]
+    erw [Equiv.apply_eq_iff_eq_symm_apply ]
+    simp
+  | Sum.inr x =>
+    simp
+    erw [Equiv.apply_eq_iff_eq_symm_apply ]
+    simp
+    simp [finExtractOnePerm, finExtractOnPermHom]
+    erw [Equiv.apply_symm_apply]
+    have h1 : (predAboveI i ((Hom.toEquiv σ)
+            (Fin.succAbove ((Hom.toEquiv σ).symm i)
+              (predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j)))))) = j  := by
+        rw [succsAbove_predAboveI]
+        · erw [Equiv.apply_symm_apply]
+          simp
+        · simp
+          erw [Equiv.apply_eq_iff_eq]
+          exact (Fin.succAbove_ne i j).symm
+    erw [h1]
+    let y := (Hom.toEquiv σ)  (Fin.succAbove ((Hom.toEquiv σ).symm i)
+      ((predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))).succAbove x))
+    change y = i.succAbove  (j.succAbove  (predAboveI j (predAboveI i y)))
+    have hy : i ≠ y := by
+      simp [y]
+      erw [← Equiv.symm_apply_eq ]
+      exact (Fin.succAbove_ne _ _).symm
+    rw [succsAbove_predAboveI, succsAbove_predAboveI]
+    exact hy
+    simp
+    rw [predAbove_eq_iff]
+    simp [y]
+    erw [← Equiv.symm_apply_eq ]
+    have h0 : (Hom.toEquiv σ).symm (i.succAbove j) =
+      Fin.succAbove ((Hom.toEquiv σ).symm i)
+        (predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))) := by
+      rw [succsAbove_predAboveI]
+      simp
+      erw [Equiv.apply_eq_iff_eq]
+      exact (Fin.succAbove_ne i j).symm
+    by_contra hn
+    have hn' := hn.symm.trans h0
+    erw [ Fin.succAbove_right_injective.eq_iff] at hn'
+    exact Fin.succAbove_ne
+             (predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))) x hn'
+    exact hy
 
 /-- The isomorphism between a `Fin 1 ⊕ Fin 1 → C` satisfying the condition
   `c (Sum.inr 0) = τ (c (Sum.inl 0))`

HepLean/Tensors/Tree/Basic.lean

@@ -74,11 +74,11 @@ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C)
     S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FDiscrete S.τ).obj
       (Discrete.mk (c i))) ⊗
       (OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
-  (S.F.mapIso (OverColor.equivToIso (OverColor.finExtractTwo i j))).trans <|
-  (S.F.mapIso (OverColor.mkSum (c ∘ (OverColor.finExtractTwo i j).symm))).trans <|
+  (S.F.mapIso (OverColor.equivToIso (HepLean.Fin.finExtractTwo i j))).trans <|
+  (S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractTwo i j).symm))).trans <|
   (S.F.μIso _ _).symm.trans <| by
   refine tensorIso ?_ (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
-  apply (S.F.mapIso (OverColor.mkSum (((c ∘ ⇑(OverColor.finExtractTwo i j).symm) ∘ Sum.inl)))).trans
+  apply (S.F.mapIso (OverColor.mkSum (((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)))).trans
   apply (S.F.μIso _ _).symm.trans
   apply tensorIso ?_ ?_
   · symm
@@ -96,6 +96,52 @@ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C)
     fin_cases x
     simp [h]
 
+open OverColor
+lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ.succ → S.C} {c1 : Fin n.succ.succ.succ → S.C}
+    {i : Fin n.succ.succ.succ} {j : Fin n.succ.succ}
+    (h : c1 (i.succAbove j) = S.τ (c1 i)) (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
+    c (Fin.succAbove ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)) =
+    S.τ (c ((Hom.toEquiv σ).symm i)) := by
+  have h1 := Hom.toEquiv_comp_apply σ
+  simp at h1
+  rw [h1, h1]
+  simp
+  rw [← h]
+  congr
+  simp [HepLean.Fin.finExtractOnePerm, HepLean.Fin.finExtractOnPermHom]
+  erw [Equiv.apply_symm_apply]
+  rw [HepLean.Fin.succsAbove_predAboveI]
+  erw [Equiv.apply_symm_apply]
+  simp
+  erw [Equiv.apply_eq_iff_eq]
+  exact (Fin.succAbove_ne i j).symm
+
+open OverColor in
+lemma contrIso_comm_map {n : ℕ} {c c1 : Fin n.succ.succ.succ → S.C}
+    {i : Fin n.succ.succ.succ} {j : Fin n.succ.succ}
+    {h : c1 (i.succAbove j) = S.τ (c1 i)}
+    (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
+  (S.F.map σ) ≫ (S.contrIso c1 i j h).hom =
+  (S.contrIso c ((OverColor.Hom.toEquiv σ).symm i)
+    (((Hom.toEquiv (extractOne i σ))).symm j) (S.perm_contr_cond h σ)).hom  ≫
+    (((Discrete.pairτ S.FDiscrete S.τ).map (Discrete.eqToHom (Hom.toEquiv_comp_inv_apply σ i)
+      : (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶ (Discrete.mk (c1 i)) )) ⊗ (S.F.map (extractTwo i j σ)))  := by
+  ext Z
+  simp
+  rw [contrIso]
+  simp
+  have h1 : ((S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom ((S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ((S.F.map σ).hom Z)))
+    = ((S.F.map σ) ≫ (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom) ≫ (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom)).hom Z := by
+      rfl
+  have h1' : ((S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom ((S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ((S.F.map σ).hom Z)))
+    = ((S.F.map (σ ≫ (equivToIso (HepLean.Fin.finExtractTwo i j)).hom ≫ (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom))).hom Z := by
+    rw [h1]
+    simp
+  rw [h1']
+  rw [extractTwo_finExtractTwo]
+  simp
+  sorry
+
 /--
 `contrMap` is a function that takes a natural number `n`, a function `c` from
 `Fin n.succ.succ` to `S.C`, an index `i` of type `Fin n.succ.succ`, an index `j` of type
@@ -302,6 +348,33 @@ lemma neg_contr {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j
     (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]
 
+lemma neg_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
+    (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) :
+    (perm σ (neg t)).tensor = (neg (perm σ t)).tensor := by
+  simp only [perm_tensor, neg_tensor, map_neg]
+
+/-!
+
+## Permutation lemmas
+
+-/
+
+
+lemma perm_contr {n : ℕ} {c : Fin n.succ.succ.succ → S.C} {c1 : Fin n.succ.succ.succ → S.C}
+    {i : Fin n.succ.succ.succ} {j : Fin n.succ.succ}
+    {h : c1 (i.succAbove j) = S.τ (c1 i)} (t : TensorTree S c)
+    (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
+    ((contr i j h (perm σ t))).tensor
+    = (perm (extractTwo i j σ) (contr ((OverColor.Hom.toEquiv σ).symm i)
+    (((Hom.toEquiv (extractOne i σ))).symm j) (perm_contr_cond h σ) t)).tensor := by
+  rw [contr_tensor, perm_tensor]
+  rw [TensorStruct.contrMap]
+  change (
+        (S.contr.app { as := c1 i } ⊗
+            𝟙 ((OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c1 ∘ i.succAbove ∘ j.succAbove)))) ≫
+          (λ_ ((OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c1 ∘ i.succAbove ∘ j.succAbove)))).hom).hom
+    ((S.contrIso c1 i j h).hom.hom ((S.F.map σ).hom t.tensor)) = _
+
 end
 
 end TensorTree