Swapping indices in a contraction

Swapping the indices in a single contraction.

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

On swapping the indices of a contraction (notionally (i, j) vs (j, i)), this is the new i index.

Equations

• q.swapI = q.i.succAbove q.j

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

On swapping the indices of a contraction (notionally (i, j) vs (j, i)), this is the new j index.

Equations

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

theorem TensorTree.ContrPair.swap_map_eq {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (x : Fin n) : q.swapI.succAbove (q.swapJ.succAbove x) = q.i.succAbove (q.j.succAbove x)

@[simp]

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

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

The ContrPair corresponding to swapping the indices, notionally (i, j) vs (j, i).

Equations

• q.swap = { i := q.swapI, j := q.swapJ, h := ⋯ }

theorem TensorTree.ContrPair.swapI_color {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) : c q.swapI = S.τ (c q.i)

@[simp]

theorem TensorTree.ContrPair.predAboveI_i_swapI {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) : PhysLean.Fin.predAboveI q.i q.swapI = q.j

theorem TensorTree.ContrPair.swap_swap {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) : q.swap.swap = q

def TensorTree.ContrPair.contrSwapHom {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) : IndexNotation.OverColor.mk (c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ⟶ IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)

The homomorphism one must apply on swapping indices in a contraction.

Equations

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

@[simp]

theorem TensorTree.ContrPair.contrSwapHom_toEquiv {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) : IndexNotation.OverColor.Hom.toEquiv q.contrSwapHom = Equiv.refl (Fin n)

@[simp]

theorem TensorTree.ContrPair.contrSwapHom_hom_left_apply {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (x : Fin n) : q.contrSwapHom.hom.left x = x

theorem TensorTree.ContrPair.contrMap_swap {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) : q.contrMap = CategoryTheory.CategoryStruct.comp q.swap.contrMap (S.F.map q.contrSwapHom)

theorem TensorTree.ContrPair.contr_swap {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (t : TensorTree S c) : (contr q.i q.j ⋯ t).tensor = (perm q.contrSwapHom (contr q.swapI q.swapJ ⋯ t)).tensor

theorem TensorTree.contr_swap {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (hij : c (i.succAbove j) = S.τ (c i)) (t : TensorTree S c) : (contr i j hij t).tensor = (perm { i := i, j := j, h := hij }.contrSwapHom (contr { i := i, j := j, h := hij }.swapI { i := i, j := j, h := hij }.swapJ ⋯ t)).tensor

Swapping the nodes of a contraction.