Swapping permutations and contractions #
The results here follow from the properties of Monoidal categories and monoidal functors.
def
TensorTree.permProdLeft
{S : TensorSpecies}
{n : ℕ}
{n' : ℕ}
{n2 : ℕ}
{c : Fin n → S.C}
{c' : Fin n' → S.C}
(c2 : Fin n2 → S.C)
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c')
:
IndexNotation.OverColor.mk
(Sum.elim (IndexNotation.OverColor.mk c).hom (IndexNotation.OverColor.mk c2).hom ∘ ⇑finSumFinEquiv.symm) ⟶ IndexNotation.OverColor.mk
(Sum.elim (IndexNotation.OverColor.mk c').hom (IndexNotation.OverColor.mk c2).hom ∘ ⇑finSumFinEquiv.symm)
The permutation that arises when moving a perm node in the left entry through a prod node.
This permutation is defined using right-whiskering and composition with finSumFinEquiv
based-isomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TensorTree.permProdLeft_toEquiv
{S : TensorSpecies}
{n : ℕ}
{n' : ℕ}
{n2 : ℕ}
{c : Fin n → S.C}
{c' : Fin n' → S.C}
(c2 : Fin n2 → S.C)
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c')
:
IndexNotation.OverColor.Hom.toEquiv (TensorTree.permProdLeft c2 σ) = finSumFinEquiv.symm.trans
(((IndexNotation.OverColor.Hom.toEquiv σ).sumCongr (Equiv.refl (Fin n2))).trans finSumFinEquiv)
def
TensorTree.permProdRight
{S : TensorSpecies}
{n : ℕ}
{n' : ℕ}
{n2 : ℕ}
{c : Fin n → S.C}
{c' : Fin n' → S.C}
(c2 : Fin n2 → S.C)
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c')
:
IndexNotation.OverColor.mk
(Sum.elim (IndexNotation.OverColor.mk c2).hom (IndexNotation.OverColor.mk c).hom ∘ ⇑finSumFinEquiv.symm) ⟶ IndexNotation.OverColor.mk
(Sum.elim (IndexNotation.OverColor.mk c2).hom (IndexNotation.OverColor.mk c').hom ∘ ⇑finSumFinEquiv.symm)
The permutation that arises when moving a perm node in the right entry through a prod node.
This permutation is defined using left-whiskering and composition with finSumFinEquiv
based-isomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TensorTree.permProdRight_toEquiv
{S : TensorSpecies}
{n : ℕ}
{n' : ℕ}
{n2 : ℕ}
{c : Fin n → S.C}
{c' : Fin n' → S.C}
(c2 : Fin n2 → S.C)
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c')
:
IndexNotation.OverColor.Hom.toEquiv (TensorTree.permProdRight c2 σ) = finSumFinEquiv.symm.trans
(((Equiv.refl (Fin n2)).sumCongr (IndexNotation.OverColor.Hom.toEquiv σ)).trans finSumFinEquiv)
theorem
TensorTree.prod_perm_left
{S : TensorSpecies}
{n : ℕ}
{n' : ℕ}
{n2 : ℕ}
{c : Fin n → S.C}
{c' : Fin n' → S.C}
(c2 : Fin n2 → S.C)
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c')
(t : TensorTree S c)
(t2 : TensorTree S c2)
:
((TensorTree.perm σ t).prod t2).tensor = (TensorTree.perm (TensorTree.permProdLeft c2 σ) (t.prod t2)).tensor
When a prod acts on a perm node in the left entry, the perm node can be moved through
the prod node via right-whiskering.
theorem
TensorTree.prod_perm_right
{S : TensorSpecies}
{n : ℕ}
{n' : ℕ}
{n2 : ℕ}
{c : Fin n → S.C}
{c' : Fin n' → S.C}
(c2 : Fin n2 → S.C)
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c')
(t2 : TensorTree S c2)
(t : TensorTree S c)
:
(t2.prod (TensorTree.perm σ t)).tensor = (TensorTree.perm (TensorTree.permProdRight c2 σ) (t2.prod t)).tensor
When a prod acts on a perm node in the right entry, the perm node can be moved through
the prod node via left-whiskering.