DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Add contr_contr theorem

Browse source
This commit is contained in:
jstoobysmith 2024-10-19 08:33:49 +00:00
parent 0bbc3f4019
commit 90dd337aab
5 changed files with 257 additions and 154 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/Mathematics/Fin.lean
View file

@ -68,7 +68,7 @@ lemma succsAbove_predAboveI {i x : Fin n.succ.succ} (h : i ≠ x) :
omega
lemma predAbove_eq_iff {i x : Fin n.succ.succ} (h : i ≠ x) (y : Fin n.succ) :
lemma predAboveI_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
@ -87,6 +87,7 @@ lemma predAboveI_ge {i x : Fin n.succ.succ} (h : i.val < x.val) :
simp [predAboveI, h]
omega
lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) :
i.succAbove (j.succAbove x) =
(i.succAbove j).succAbove ((predAboveI (i.succAbove j) i).succAbove x) := by

2
HepLean/Tensors/OverColor/Iso.lean
View file

@ -204,7 +204,7 @@ lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : F
rw [succsAbove_predAboveI, succsAbove_predAboveI]
exact hy
simp
rw [predAbove_eq_iff]
rw [predAboveI_eq_iff]
simp [y]
erw [← Equiv.symm_apply_eq ]
have h0 : (Hom.toEquiv σ).symm (i.succAbove j) =

42
HepLean/Tensors/Tree/Basic.lean
View file

@ -205,7 +205,7 @@ corresponding to the contraction of the `i`th index with the `i.succAbove j` ind
def contrMap {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)) :
S.F.obj (OverColor.mk c) ⟶
(OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
(S.contrIso c i j h).hom ≫
(tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
(MonoidalCategory.leftUnitor _).hom
@ -218,7 +218,7 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
(S.contrMap c i j h).hom (PiTensorProduct.tprod S.k x) =
(S.castToField ((S.contr.app (Discrete.mk (c i))).hom ((x i) ⊗ₜ[S.k]
(S.FDiscrete.map (Discrete.eqToHom h)).hom (x (i.succAbove j)) )): S.k)
• (PiTensorProduct.tprod S.k (fun k => x (i.succAbove (j.succAbove k)))) := by
• (PiTensorProduct.tprod S.k (fun k => x (i.succAbove (j.succAbove k))) : S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))) := by
rw [contrMap, contrIso]
simp only [Nat.succ_eq_add_one, S.F_def, Iso.trans_hom, Functor.mapIso_hom, Iso.symm_hom,
tensorIso_hom, Monoidal.tensorUnit_obj, tensorHom_id,
@ -477,44 +477,6 @@ lemma prod_tensor_eq_snd {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
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]
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]
end
end TensorTree

84
HepLean/Tensors/Tree/NodeIdentities/Basic.lean Normal file
View file

@ -0,0 +1,84 @@
/-
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
/-!
## Basic node identities
This file contains the basic node identities for tensor trees.
More compliciated identities appear in there own files.
-/
open IndexNotation
open CategoryTheory
open MonoidalCategory
open OverColor
open HepLean.Fin
open TensorProduct
namespace TensorTree
variable {S : TensorStruct}
/-!
## Equality of constructors.
-/
informal_lemma constVecNode_eq_vecNode where
math :≈ "A constVecNode has equal tensor to the vecNode with the map evaluated at 1."
deps :≈ [``constVecNode, ``vecNode]
informal_lemma constTwoNode_eq_twoNode where
math :≈ "A constTwoNode has equal tensor to the twoNode with the map evaluated at 1."
deps :≈ [``constTwoNode, ``twoNode]
informal_lemma constThreeNode_eq_threeNode where
math :≈ "A constThreeNode has equal tensor to the threeNode with the map evaluated at 1."
deps :≈ [``constThreeNode, ``threeNode]
/-!
## Negation
-/
@[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]
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]
end TensorTree

280
HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
View file

@ -8,6 +8,8 @@ import HepLean.Tensors.Tree.Basic
## Commutativity of two contractions
This file is currently a work-in-progress.
-/
open IndexNotation
@ -16,10 +18,6 @@ open MonoidalCategory
open OverColor
open HepLean.Fin
namespace TensorStruct
end TensorStruct
namespace TensorTree
variable {S : TensorStruct}
@ -37,22 +35,26 @@ variable {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c)
def swapI : Fin n.succ.succ.succ.succ := q.i.succAbove (q.j.succAbove q.k)
def swapJ : Fin n.succ.succ.succ := (predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove
((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
/-
(predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
predAboveI
def swapK : Fin n.succ.succ := predAboveI
((predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove
((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l))
(predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i)
predAboveI ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l) (predAboveI (q.j.succAbove q.k) q.j)
-/
def swapJ : Fin n.succ.succ.succ := predAboveI q.swapI (q.i.succAbove (q.j.succAbove (q.k.succAbove q.l)))
def swapL : Fin n.succ := predAboveI ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
(predAboveI (q.j.succAbove q.k) q.j)
def swapK : Fin n.succ.succ := predAboveI q.swapJ (predAboveI q.swapI q.i)
def swapL : Fin n.succ := predAboveI q.swapK (predAboveI q.swapJ (predAboveI q.swapI (q.i.succAbove q.j)))
lemma swap_map_eq (x : Fin n) : (q.swapI.succAbove (q.swapJ.succAbove
(q.swapK.succAbove (q.swapL.succAbove x)))) =
(q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove x)))) := by
rw [succAbove_succAbove_predAboveI q.j q.k]
rw [succAbove_succAbove_predAboveI q.i]
apply congrArg
rw [succAbove_succAbove_predAboveI (predAboveI (q.j.succAbove q.k) q.j)]
rw [succAbove_succAbove_predAboveI (predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i)]
congr
@[simp]
lemma swapI_neq_i : ¬ q.swapI = q.i := by
@ -72,136 +74,190 @@ lemma swapI_neq_i_j_k_l_succAbove : ¬ q.swapI = q.i.succAbove (q.j.succAbove (q
apply Function.Injective.ne Fin.succAbove_right_injective
exact Fin.ne_succAbove q.k q.l
@[simp]
lemma swapJ_neq_predAboveI_swapI_i : ¬ q.swapJ = predAboveI q.swapI q.i := by
simp [swapJ]
erw [predAbove_eq_iff]
rw [succsAbove_predAboveI]
· exact Fin.succAbove_ne q.i (q.j.succAbove (q.k.succAbove q.l))
· apply Function.Injective.ne Fin.succAbove_right_injective
apply Function.Injective.ne Fin.succAbove_right_injective
exact Fin.ne_succAbove q.k q.l
· simp only [Nat.succ_eq_add_one, ne_eq, swapI_neq_i, not_false_eq_true]
lemma swapJ_neq_predAboveI_swapI_i_succAbove_j :
¬q.swapJ = predAboveI q.swapI (q.i.succAbove q.j) := by
simp [swapJ]
erw [predAbove_eq_iff]
rw [succsAbove_predAboveI]
· apply Function.Injective.ne Fin.succAbove_right_injective
exact Fin.succAbove_ne q.j (q.k.succAbove q.l)
· exact swapI_neq_i_j_k_l_succAbove q
· exact swapI_neq_succAbove q
@[simp]
lemma swapJ_swapI_succAbove : q.swapI.succAbove q.swapJ = (q.i.succAbove (q.j.succAbove (q.k.succAbove q.l))) := by
lemma swapJ_swapI_succAbove : q.swapI.succAbove q.swapJ = q.i.succAbove
(q.j.succAbove (q.k.succAbove q.l)) := by
simp [swapI, swapJ]
rw [succsAbove_predAboveI]
apply Function.Injective.ne Fin.succAbove_right_injective
simp
apply Function.Injective.ne Fin.succAbove_right_injective
exact Fin.ne_succAbove q.k q.l
rw [← succAbove_succAbove_predAboveI]
rw [← succAbove_succAbove_predAboveI]
lemma swapJ_eq_swapI_predAbove : q.swapJ = predAboveI q.swapI (q.i.succAbove
(q.j.succAbove (q.k.succAbove q.l))) := by
rw [predAboveI_eq_iff]
exact swapJ_swapI_succAbove q
exact swapI_neq_i_j_k_l_succAbove q
@[simp]
lemma swapK_swapJ_succAbove : (q.swapJ).succAbove (q.swapK) = predAboveI q.swapI q.i := by
simp [swapJ, swapK]
lemma swapK_swapJ_succAbove : (q.swapJ.succAbove q.swapK) = predAboveI q.swapI q.i := by
rw [swapJ, swapK]
rw [succsAbove_predAboveI]
simp
erw [predAbove_eq_iff]
rw [succsAbove_predAboveI]
· exact Fin.succAbove_ne q.i (q.j.succAbove (q.k.succAbove q.l))
· apply Function.Injective.ne Fin.succAbove_right_injective
apply Function.Injective.ne Fin.succAbove_right_injective
exact Fin.ne_succAbove q.k q.l
· simp only [Nat.succ_eq_add_one, ne_eq, swapI_neq_i, not_false_eq_true]
rfl
exact Fin.succAbove_ne (predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i)
((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
@[simp]
lemma swapK_swapJ_swapI_succAbove : (q.swapI).succAbove ( predAboveI q.swapI q.i) = q.i := by
lemma swapK_swapJ_swapI_succAbove : (q.swapI).succAbove (predAboveI q.swapI q.i) = q.i := by
rw [succsAbove_predAboveI]
simp
@[simp]
lemma swapL_swapK_succAbove : (q.swapK).succAbove (q.swapL) =
predAboveI q.swapJ (predAboveI q.swapI (q.i.succAbove q.j)) := by
simp [swapK, swapL]
rw [succsAbove_predAboveI]
simp
erw [predAbove_eq_iff]
rw [succsAbove_predAboveI]
· erw [predAbove_eq_iff]
· rw [succsAbove_predAboveI]
· exact Fin.ne_succAbove q.i q.j
· exact swapI_neq_i q
· simp only [Nat.succ_eq_add_one, ne_eq, swapI_neq_succAbove, not_false_eq_true]
· exact swapJ_neq_predAboveI_swapI_i q
· exact swapJ_neq_predAboveI_swapI_i_succAbove_j q
@[simp]
lemma swapL_swapK_swapJ_succAbove :
(q.swapJ).succAbove (predAboveI q.swapJ (predAboveI q.swapI (q.i.succAbove q.j))) =
(predAboveI q.swapI (q.i.succAbove q.j)) := by
rw [succsAbove_predAboveI]
simp
exact swapJ_neq_predAboveI_swapI_i_succAbove_j q
@[simp]
lemma swapL_swapK_swapJ_swapI_succAbove :
(q.swapI).succAbove (predAboveI q.swapI (q.i.succAbove q.j)) = (q.i.succAbove q.j) := by
simp [swapI]
rw [succsAbove_predAboveI]
apply Function.Injective.ne Fin.succAbove_right_injective
lemma swapL_swapK_swapJ_swapI_succAbove : q.swapI.succAbove (q.swapJ.succAbove (q.swapK.succAbove q.swapL)) =
q.i.succAbove q.j := by
rw [swapJ, swapK]
rw [← succAbove_succAbove_predAboveI]
rw [swapI]
rw [← succAbove_succAbove_predAboveI]
apply congrArg
rw [swapL]
rw [succsAbove_predAboveI, succsAbove_predAboveI]
exact Fin.succAbove_ne q.j q.k
exact Fin.succAbove_ne (predAboveI (q.j.succAbove q.k) q.j) q.l
@[simp]
def swap : ContrQuartet c where
i := q.swapI
j := q.swapJ
k := q.swapK
l := q.swapL
hij := by
simpa using q.hkl
rw [swapJ_swapI_succAbove, swapI]
simpa using q.hkl
hkl := by
simpa using q.hij
lemma swap_map_eq (x : Fin n ): (q.swap.i.succAbove (q.swap.j.succAbove
(q.swap.k.succAbove (q.swap.l.succAbove x)))) =
(q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove x)))) := by
rw [succAbove_succAbove_predAboveI q.j q.k]
rw [succAbove_succAbove_predAboveI q.i]
apply congrArg
rw [succAbove_succAbove_predAboveI (predAboveI (q.j.succAbove q.k) q.j)]
rw [succAbove_succAbove_predAboveI (predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i)]
congr
noncomputable section
def contrMapFst := S.contrMap c q.i q.j q.hij
def contrMapSnd := S.contrMap (c ∘ q.i.succAbove ∘ q.j.succAbove) q.k q.l q.hkl
lemma contrMap_swap :
q.contrMapFst ≫ q.contrMapSnd = q.swap.contrMapFst ≫ q.swap.contrMapSnd
≫ S.F.map (OverColor.mkIso (by sorry)).hom := by sorry
def contrSwapHom : (OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘ q.swap.k.succAbove ∘ q.swap.l.succAbove)) ⟶
(OverColor.mk fun x => c (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove x))))):=
(mkIso (funext fun x => congrArg c (swap_map_eq q x))).hom
lemma contrSwapHom_contrMapSnd_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) → CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c).hom i })) :
((lift.obj S.FDiscrete).map q.contrSwapHom).hom
(q.swap.contrMapSnd.hom ((PiTensorProduct.tprod S.k) fun k => x (q.swap.i.succAbove (q.swap.j.succAbove k))))
= ((S.castToField
((S.contr.app { as := (c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) q.swap.k }).hom
(x (q.swap.i.succAbove (q.swap.j.succAbove q.swap.k)) ⊗ₜ[S.k]
(S.FDiscrete.map (Discrete.eqToHom q.swap.hkl)).hom
(x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove q.swap.l))))))) •
((lift.obj S.FDiscrete).map q.contrSwapHom).hom ((PiTensorProduct.tprod S.k) fun k =>
x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove (q.swap.l.succAbove k)))))) := by
rw [contrMapSnd,TensorStruct.contrMap_tprod]
change ((lift.obj S.FDiscrete).map q.contrSwapHom).hom
(_ • ((PiTensorProduct.tprod S.k) fun k =>
x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove (q.swap.l.succAbove k))
)): S.F.obj (OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘
q.swap.k.succAbove ∘ q.swap.l.succAbove)) )) = _
rw [map_smul]
rfl
lemma contrSwapHom_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) → CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c).hom i })) :
((PiTensorProduct.tprod S.k) fun k => x (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove k))))) =
((lift.obj S.FDiscrete).map q.contrSwapHom).hom
((PiTensorProduct.tprod S.k) fun k =>
x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove (q.swap.l.succAbove k))))) := by
rw [lift.map_tprod]
apply congrArg
funext i
simp
rw [lift.discreteFunctorMapEqIso]
change _ = (S.FDiscrete.map (Discrete.eqToIso _).hom).hom _
have h1' {a b : Fin n.succ.succ.succ.succ} (h : a = b) :
x b = (S.FDiscrete.map (Discrete.eqToIso (by rw [h])).hom).hom (x a) := by
subst h
simp
exact h1' (q.swap_map_eq i)
lemma contrMapFst_contrMapSnd_swap :
q.contrMapFst ≫ q.contrMapSnd = q.swap.contrMapFst ≫ q.swap.contrMapSnd ≫
S.F.map q.contrSwapHom := by
ext x
change q.contrMapSnd.hom (q.contrMapFst.hom x) = (S.F.map q.contrSwapHom).hom
(q.swap.contrMapSnd.hom (q.swap.contrMapFst.hom 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]
simp only [Nat.succ_eq_add_one, Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
map_smul]
apply congrArg
rw [contrMapFst, contrMapFst]
change q.contrMapSnd.hom ((S.contrMap c q.i q.j _).hom ((PiTensorProduct.tprod S.k) x)) =
(S.F.map q.contrSwapHom).hom
(q.swap.contrMapSnd.hom ((S.contrMap c q.swap.i q.swap.j _).hom ((PiTensorProduct.tprod S.k) x)))
rw [TensorStruct.contrMap_tprod, TensorStruct.contrMap_tprod]
simp only [Nat.succ_eq_add_one, Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, Discrete.functor_obj_eq_as,
Function.comp_apply, map_smul]
change _ •
q.contrMapSnd.hom ((PiTensorProduct.tprod S.k) fun k => x (q.i.succAbove (q.j.succAbove k))) =
S.castToField
_ •
((lift.obj S.FDiscrete).map q.contrSwapHom).hom
(q.swap.contrMapSnd.hom ((PiTensorProduct.tprod S.k) fun k => x (q.swap.i.succAbove (q.swap.j.succAbove k))))
rw [contrMapSnd, TensorStruct.contrMap_tprod, q.contrSwapHom_contrMapSnd_tprod]
rw [smul_smul, smul_smul]
congr 1
/- The contractions. -/
· nth_rewrite 1 [mul_comm]
congr 1
· congr 3
have h1' {a b d: Fin n.succ.succ.succ.succ} (hbd : b =d) (h : c d = S.τ (c a)) (h' : c b = S.τ (c a)) :
(S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
(S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
subst hbd
rfl
refine h1' ?_ ?_ ?_
erw [swapJ_swapI_succAbove]
rfl
· congr 1
simp
have h' {a a' b b' : Fin n.succ.succ.succ.succ} (hab : c b = S.τ (c a))
(hab' : c b' = S.τ (c a')) (ha : a = a') (hb : b= b') :
(S.contr.app { as := c a }).hom (x a ⊗ₜ[S.k] (S.FDiscrete.map (Discrete.eqToHom hab)).hom (x b)) =
(S.contr.app { as := c a' }).hom (x a' ⊗ₜ[S.k]
(S.FDiscrete.map (Discrete.eqToHom hab')).hom
(x b')) := by
subst ha hb
rfl
apply h'
· simp only [Nat.succ_eq_add_one, swap, swapK_swapJ_succAbove, swapK_swapJ_swapI_succAbove]
· simp only [Nat.succ_eq_add_one, swap, Function.comp_apply,
swapL_swapK_swapJ_swapI_succAbove]
/- The tensor-/
· exact q.contrSwapHom_tprod _
lemma contr_contr (t : TensorTree S c) :
(contr q.k q.l q.hkl (contr q.i q.j q.hij t)).tensor =
(perm q.contrSwapHom (contr q.swapK q.swapL q.swap.hkl (contr q.swapI q.swapJ q.swap.hij t))).tensor := by
simp only [contr_tensor, perm_tensor]
trans (q.contrMapFst ≫ q.contrMapSnd).hom t.tensor
simp only [Nat.succ_eq_add_one, contrMapFst, contrMapSnd, Action.comp_hom, ModuleCat.coe_comp,
Function.comp_apply]
rw [contrMapFst_contrMapSnd_swap]
simp only [Nat.succ_eq_add_one, contrMapFst, contrMapSnd, Action.comp_hom, ModuleCat.coe_comp,
Function.comp_apply, swap]
apply congrArg
apply congrArg
apply congrArg
rfl
end
end ContrQuartet
theorem contr_contr {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C}
(i : Fin n.succ.succ.succ.succ) (j : Fin n.succ.succ.succ)
(k : Fin n.succ.succ) (l : Fin n.succ)
(hij : c (i.succAbove j) = S.τ (c i))
(hkl : (c ∘ i.succAbove ∘ j.succAbove) (k.succAbove l) = S.τ ((c ∘ i.succAbove ∘ j.succAbove) k))
(t : TensorTree S c) :
(contr k l hkl (contr i j hij t)).tensor =
(
contr (i.succAbove (j.succAbove k))
(predAboveI (i.succAbove (j.succAbove k)) (i.succAbove (j.succAbove (k.succAbove l))))
(by sorry) t).tensor := by sorry
/-- Contraction nodes commute on adjusting indices. -/
theorem contr_contr {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n.succ.succ.succ.succ}
{j : Fin n.succ.succ.succ} {k : Fin n.succ.succ} {l : Fin n.succ}
(hij : c (i.succAbove j) = S.τ (c i)) (hkl : (c ∘ i.succAbove ∘ j.succAbove) (k.succAbove l) = S.τ ((c ∘ i.succAbove ∘ j.succAbove) k))
(t : TensorTree S c) :
(contr k l hkl (contr i j hij t)).tensor =
(perm (ContrQuartet.mk i j k l hij hkl).contrSwapHom
(contr (ContrQuartet.mk i j k l hij hkl).swapK (ContrQuartet.mk i j k l hij hkl).swapL
(ContrQuartet.mk i j k l hij hkl).swap.hkl (contr (ContrQuartet.mk i j k l hij hkl).swapI (ContrQuartet.mk i j k l hij hkl).swapJ (ContrQuartet.mk i j k l hij hkl).swap.hij t))).tensor := by
exact ContrQuartet.contr_contr (ContrQuartet.mk i j k l hij hkl) t
end TensorTree
end IndexNotation