The commutativity of Permutations and contractions. #
There is very likely a better way to do this using TensorSpecies.contrMap_tprod
.
theorem
TensorSpecies.contrFin1Fin1_naturality
(S : TensorSpecies)
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
(h : c1 (i.succAbove j) = S.τ (c1 i))
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.extractTwoAux' i j σ)).hom
(S.contrFin1Fin1 c1 i j h).hom.hom = CategoryTheory.CategoryStruct.comp
(S.contrFin1Fin1 c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
(IndexNotation.OverColor.Hom.toEquiv σ)).symm
j)
⋯).hom.hom
((IndexNotation.OverColor.Discrete.pairτ S.FD S.τ).map (CategoryTheory.Discrete.eqToHom ⋯)).hom
theorem
TensorSpecies.contrIso_comm_aux_1
(S : TensorSpecies)
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (S.F.map σ).hom
(S.F.map (IndexNotation.OverColor.equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom)
(S.F.map (IndexNotation.OverColor.mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom = CategoryTheory.CategoryStruct.comp
(S.F.map
(IndexNotation.OverColor.equivToIso
(HepLean.Fin.finExtractTwo ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
(IndexNotation.OverColor.Hom.toEquiv σ)).symm
j))).hom).hom
(CategoryTheory.CategoryStruct.comp
(S.F.map
(IndexNotation.OverColor.mkSum
(c ∘ ⇑(HepLean.Fin.finExtractTwo ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
(IndexNotation.OverColor.Hom.toEquiv σ)).symm
j)).symm)).hom).hom
(S.F.map
(CategoryTheory.MonoidalCategory.tensorHom (IndexNotation.OverColor.extractTwoAux' i j σ)
(IndexNotation.OverColor.extractTwoAux i j σ))).hom)
theorem
TensorSpecies.contrIso_comm_aux_2
(S : TensorSpecies)
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
CategoryTheory.CategoryStruct.comp
(S.F.map
(CategoryTheory.MonoidalCategory.tensorHom (IndexNotation.OverColor.extractTwoAux' i j σ)
(IndexNotation.OverColor.extractTwoAux i j σ))).hom
(CategoryTheory.Functor.Monoidal.μIso S.F
(IndexNotation.OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
(IndexNotation.OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Functor.Monoidal.μIso S.F
(IndexNotation.OverColor.mk
((c ∘ ⇑(HepLean.Fin.finExtractTwo ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)).symm) ∘ Sum.inl))
(IndexNotation.OverColor.mk
((c ∘ ⇑(HepLean.Fin.finExtractTwo ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)).symm) ∘ Sum.inr))).inv.hom
(CategoryTheory.MonoidalCategory.tensorHom (S.F.map (IndexNotation.OverColor.extractTwoAux' i j σ))
(S.F.map (IndexNotation.OverColor.extractTwoAux i j σ))).hom
theorem
TensorSpecies.contrIso_comm_aux_3
(S : TensorSpecies)
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
CategoryTheory.CategoryStruct.comp
(((Action.functorCategoryEquivalence (ModuleCat S.k) (MonCat.of S.G)).symm.inverse.map
(S.F.map (IndexNotation.OverColor.extractTwoAux i j σ))).app
PUnit.unit)
(S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom = CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom
(S.F.map (IndexNotation.OverColor.extractTwo i j σ)).hom
def
TensorSpecies.contrIsoComm
(S : TensorSpecies)
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
CategoryTheory.MonoidalCategory.tensorObj
((IndexNotation.OverColor.Discrete.pairτ S.FD S.τ).obj { as := c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) })
(S.F.obj
(IndexNotation.OverColor.mk
(c ∘ Fin.succAbove ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ∘ Fin.succAbove ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)))) ⟶ CategoryTheory.MonoidalCategory.tensorObj ((IndexNotation.OverColor.Discrete.pairτ S.FD S.τ).obj { as := c1 i })
(S.F.obj (IndexNotation.OverColor.mk (c1 ∘ i.succAbove ∘ j.succAbove)))
A helper function used to proof the relation between perm and contr.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TensorSpecies.contrIso_comm_aux_5
(S : TensorSpecies)
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
(h : c1 (i.succAbove j) = S.τ (c1 i))
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (S.F.map (IndexNotation.OverColor.extractTwoAux' i j σ))
(S.F.map (IndexNotation.OverColor.extractTwoAux i j σ))).hom
(CategoryTheory.MonoidalCategory.tensorHom (S.contrFin1Fin1 c1 i j h).hom.hom
(S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom
(S.contrFin1Fin1 c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
(IndexNotation.OverColor.Hom.toEquiv σ)).symm
j)
⋯).hom.hom
(S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom)
(S.contrIsoComm σ).hom
theorem
TensorSpecies.contrIso_comm_map
(S : TensorSpecies)
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
{h : c1 (i.succAbove j) = S.τ (c1 i)}
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
CategoryTheory.CategoryStruct.comp (S.F.map σ) (S.contrIso c1 i j h).hom = CategoryTheory.CategoryStruct.comp
(S.contrIso c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j) ⋯).hom
(S.contrIsoComm σ)
theorem
TensorSpecies.contrMap_naturality
(S : TensorSpecies)
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
{h : c1 (i.succAbove j) = S.τ (c1 i)}
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
CategoryTheory.CategoryStruct.comp (S.F.map σ) (S.contrMap c1 i j h) = CategoryTheory.CategoryStruct.comp
(S.contrMap c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j) ⋯)
(S.F.map (IndexNotation.OverColor.extractTwo i j σ))
Contraction commutes with S.F.map σ
on removing corresponding indices from σ
.
theorem
TensorTree.perm_contr
{S : TensorSpecies}
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
{h : c1 (i.succAbove j) = S.τ (c1 i)}
(t : TensorTree S c)
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
(TensorTree.contr i j h (TensorTree.perm σ t)).tensor = (TensorTree.perm (IndexNotation.OverColor.extractTwo i j σ)
(TensorTree.contr ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)
((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j) ⋯ t)).tensor
Permuting indices, and then contracting is equivalent to contracting and then permuting, once care is taking about ensuring one is contracting the same idices.
theorem
TensorTree.perm_contr_congr_mkIso_cond
{S : TensorSpecies}
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
{σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1}
{i' : Fin n.succ.succ}
{j' : Fin n.succ}
(hi : i' = (IndexNotation.OverColor.Hom.toEquiv σ).symm i)
(hj : j' = (IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)
:
c ∘ i'.succAbove ∘ j'.succAbove = c ∘ Fin.succAbove ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ∘ Fin.succAbove ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)
theorem
TensorTree.perm_contr_congr_contr_cond
{S : TensorSpecies}
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
(h : c1 (i.succAbove j) = S.τ (c1 i))
{σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1}
{i' : Fin n.succ.succ}
{j' : Fin n.succ}
(hi : i' = (IndexNotation.OverColor.Hom.toEquiv σ).symm i)
(hj : j' = (IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)
:
c (i'.succAbove j') = S.τ (c i')
theorem
TensorTree.perm_contr_congr
{S : TensorSpecies}
{n : ℕ}
{c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ}
{j : Fin n.succ}
{h : c1 (i.succAbove j) = S.τ (c1 i)}
{t : TensorTree S c}
{σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1}
(i' : Fin n.succ.succ)
(j' : Fin n.succ)
(hi : i' = (IndexNotation.OverColor.Hom.toEquiv σ).symm i := by decide)
(hj : j' = (IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j := by decide)
:
(TensorTree.contr i j h (TensorTree.perm σ t)).tensor = (TensorTree.perm
(CategoryTheory.CategoryStruct.comp (IndexNotation.OverColor.mkIso ⋯).hom
(IndexNotation.OverColor.extractTwo i j σ))
(TensorTree.contr i' j' ⋯ t)).tensor