Commutativity of two contractions

The order of two contractions can be swapped, once the indices have been accordingly adjusted.

structure TensorTree.ContrQuartet {S : TensorSpecies} {n : ℕ} (c : Fin n.succ.succ.succ.succ → S.C) : Type

A structure containing two pairs of indices (i, j) and (k, l) to be sequentially contracted in a tensor.

• i : Fin n.succ.succ.succ.succ

  The first index of the first pair to be contracted.

• j : Fin n.succ.succ.succ

  The second index of the first pair to be contracted.

• k : Fin n.succ.succ

  The first index of the second pair to be contracted.

• l : Fin n.succ

  The second index of the second pair to be contracted.

• hij : c (self.i.succAbove self.j) = S.τ (c self.i)

  The condition on the first pair of indices permitting their contraction.

• hkl : (c ∘ self.i.succAbove ∘ self.j.succAbove) (self.k.succAbove self.l) = S.τ ((c ∘ self.i.succAbove ∘ self.j.succAbove) self.k)

  The condition on the second pair of indices permitting their contraction.

def TensorTree.ContrQuartet.swapI {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : Fin n.succ.succ.succ.succ

On swapping the order of contraction (notionally (i, j) - (k, l) vs (k, l) - (i, j)), this is the new i index.

Equations

• q.swapI = q.i.succAbove (q.j.succAbove q.k)

def TensorTree.ContrQuartet.swapJ {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : Fin n.succ.succ.succ

On swapping the order of contraction (notionally (i, j) - (k, l) vs (k, l) - (i, j)), this is the new j index.

Equations

• q.swapJ = (PhysLean.Fin.predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove ((PhysLean.Fin.predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)

def TensorTree.ContrQuartet.swapK {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : Fin n.succ.succ

On swapping the order of contraction (notionally (i, j) - (k, l) vs (k, l) - (i, j)), this is the new k index.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.ContrQuartet.swapL {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : Fin n.succ

On swapping the order of contraction (notionally (i, j) - (k, l) vs (k, l) - (i, j)), this is the new l index.

Equations

• q.swapL = PhysLean.Fin.predAboveI ((PhysLean.Fin.predAboveI (q.j.succAbove q.k) q.j).succAbove q.l) (PhysLean.Fin.predAboveI (q.j.succAbove q.k) q.j)

theorem TensorTree.ContrQuartet.swap_map_eq {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) (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)))

@[simp]

theorem TensorTree.ContrQuartet.swapI_neq_i {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : ¬q.swapI = q.i

@[simp]

theorem TensorTree.ContrQuartet.swapI_neq_succAbove {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : ¬q.swapI = q.i.succAbove q.j

@[simp]

theorem TensorTree.ContrQuartet.swapI_neq_i_j_k_l_succAbove {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : ¬q.swapI = q.i.succAbove (q.j.succAbove (q.k.succAbove q.l))

theorem TensorTree.ContrQuartet.swapJ_swapI_succAbove {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : q.swapI.succAbove q.swapJ = q.i.succAbove (q.j.succAbove (q.k.succAbove q.l))

theorem TensorTree.ContrQuartet.swapJ_eq_swapI_predAbove {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : q.swapJ = PhysLean.Fin.predAboveI q.swapI (q.i.succAbove (q.j.succAbove (q.k.succAbove q.l)))

@[simp]

theorem TensorTree.ContrQuartet.swapK_swapJ_succAbove {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : q.swapJ.succAbove q.swapK = PhysLean.Fin.predAboveI q.swapI q.i

@[simp]

theorem TensorTree.ContrQuartet.swapK_swapJ_swapI_succAbove {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : q.swapI.succAbove (PhysLean.Fin.predAboveI q.swapI q.i) = q.i

@[simp]

theorem TensorTree.ContrQuartet.swapL_swapK_swapJ_swapI_succAbove {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : q.swapI.succAbove (q.swapJ.succAbove (q.swapK.succAbove q.swapL)) = q.i.succAbove q.j

def TensorTree.ContrQuartet.swap {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : ContrQuartet c

The ContrQuartet corresponding to swapping the order of contraction (notionally (i, j) - (k, l) vs (k, l) - (i, j)).

Equations

• q.swap = { i := q.swapI, j := q.swapJ, k := q.swapK, l := q.swapL, hij := ⋯, hkl := ⋯ }

def TensorTree.ContrQuartet.contrMapFst {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : S.F.obj (IndexNotation.OverColor.mk c) ⟶ S.F.obj (IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))

The contraction map for the first pair of indices.

Equations

• q.contrMapFst = S.contrMap c q.i q.j ⋯

def TensorTree.ContrQuartet.contrMapSnd {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : S.F.obj (IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) ⟶ S.F.obj (IndexNotation.OverColor.mk ((c ∘ q.i.succAbove ∘ q.j.succAbove) ∘ q.k.succAbove ∘ q.l.succAbove))

The contraction map for the second pair of indices.

Equations

• q.contrMapSnd = S.contrMap (c ∘ q.i.succAbove ∘ q.j.succAbove) q.k q.l ⋯

def TensorTree.ContrQuartet.contrSwapHom {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : IndexNotation.OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘ q.swap.k.succAbove ∘ q.swap.l.succAbove) ⟶ IndexNotation.OverColor.mk fun (x : Fin n) => c (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove x))))

The homomorphism one must apply on swapping the order of contractions.

Equations

• q.contrSwapHom = (IndexNotation.OverColor.mkIso ⋯).hom

theorem TensorTree.ContrQuartet.contrSwapHom_contrMapSnd_tprod {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) (x : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c).left) → CoeSort.coe (S.FD.obj { as := (IndexNotation.OverColor.mk c).hom i })) : (CategoryTheory.ConcreteCategory.hom ((IndexNotation.OverColor.lift.obj S.FD).map q.contrSwapHom).hom) ((CategoryTheory.ConcreteCategory.hom q.swap.contrMapSnd.hom) ((PiTensorProduct.tprod S.k) fun (k : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk (c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove)).left) => x (q.swap.i.succAbove (q.swap.j.succAbove k)))) = S.castToField ((CategoryTheory.ConcreteCategory.hom (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] (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.Discrete.eqToHom ⋯)).hom) (x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove q.swap.l)))))) • (CategoryTheory.ConcreteCategory.hom ((IndexNotation.OverColor.lift.obj S.FD).map q.contrSwapHom).hom) ((PiTensorProduct.tprod S.k) fun (k : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘ q.swap.k.succAbove ∘ q.swap.l.succAbove)).left) => x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove (q.swap.l.succAbove k)))))

theorem TensorTree.ContrQuartet.contrSwapHom_tprod {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) (x : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c).left) → ↑(S.FD.obj { as := (IndexNotation.OverColor.mk c).hom i }).V) : ((PiTensorProduct.tprod S.k) fun (k : Fin n) => x (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove k))))) = (CategoryTheory.ConcreteCategory.hom ((IndexNotation.OverColor.lift.obj S.FD).map q.contrSwapHom).hom) ((PiTensorProduct.tprod S.k) fun (k : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘ q.swap.k.succAbove ∘ q.swap.l.succAbove)).left) => x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove (q.swap.l.succAbove k)))))

theorem TensorTree.ContrQuartet.contrMapFst_contrMapSnd_swap {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) : CategoryTheory.CategoryStruct.comp q.contrMapFst q.contrMapSnd = CategoryTheory.CategoryStruct.comp q.swap.contrMapFst (CategoryTheory.CategoryStruct.comp q.swap.contrMapSnd (S.F.map q.contrSwapHom))

theorem TensorTree.ContrQuartet.contr_contr {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c) (t : TensorTree S c) : (contr q.k q.l ⋯ (contr q.i q.j ⋯ t)).tensor = (perm q.contrSwapHom (contr q.swapK q.swapL ⋯ (contr q.swapI q.swapJ ⋯ t))).tensor

def TensorTree.contrContrPerm {S : TensorSpecies} {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)) : IndexNotation.OverColor.mk ((c ∘ { i := i, j := j, k := k, l := l, hij := hij, hkl := hkl }.swapI.succAbove ∘ { i := i, j := j, k := k, l := l, hij := hij, hkl := hkl }.swapJ.succAbove) ∘ { i := i, j := j, k := k, l := l, hij := hij, hkl := hkl }.swapK.succAbove ∘ { i := i, j := j, k := k, l := l, hij := hij, hkl := hkl }.swapL.succAbove) ⟶ IndexNotation.OverColor.mk ((c ∘ i.succAbove ∘ j.succAbove) ∘ k.succAbove ∘ l.succAbove)

The homomorphism one must apply on swapping the order of contractions. This is identical to ContrQuartet.contrSwapHom except manifestly between the correct types.

Equations

• TensorTree.contrContrPerm hij hkl = { i := i, j := j, k := k, l := l, hij := hij, hkl := hkl }.contrSwapHom

@[simp]

theorem TensorTree.contrContrPerm_hom_left_apply {S : TensorSpecies} {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)) (x : Fin n) : (contrContrPerm hij hkl).hom.left x = x

theorem TensorTree.contr_contr {S : TensorSpecies} {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 (contrContrPerm hij hkl) (contr { i := i, j := j, k := k, l := l, hij := hij, hkl := hkl }.swapK { i := i, j := j, k := k, l := l, hij := hij, hkl := hkl }.swapL ⋯ (contr { i := i, j := j, k := k, l := l, hij := hij, hkl := hkl }.swapI { i := i, j := j, k := k, l := l, hij := hij, hkl := hkl }.swapJ ⋯ t))).tensor

Contraction nodes commute on adjusting indices.