LeanPool.RegtsSevenster.RS.Classical.Deligne.TwistCoherence

source

theorem RS.twist_shuffle_coherence {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (V R A W S : D) :

The twist-shuffle coherence: extracting A from the twisted factor V ⊗ R, interchanging, and reinserting it between R and S agrees with associating A into W ⊗ S and interchanging. The block braiding β_ (V ⊗ R) A contributes crossings of A past R and past V; the latter cancels against β_ A V by symmetry, the former is conjugated through the interchange block by naturality of the braiding and cancels against (β_ R A).inv, and the residual word is the interchange of V ⊗ R with W ⊗ (A ⊗ S).

source

theorem RS.twist_shuffle_coherence_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (V R A W S : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (CategoryTheory.MonoidalCategoryStruct.tensorObj R (CategoryTheory.MonoidalCategoryStruct.tensorObj A S)) ⟶ Z) :

The twist-shuffle coherence: extracting A from the twisted factor V ⊗ R, interchanging, and reinserting it between R and S agrees with associating A into W ⊗ S and interchanging. The block braiding β_ (V ⊗ R) A contributes crossings of A past R and past V; the latter cancels against β_ A V by symmetry, the former is conjugated through the interchange block by naturality of the braiding and cancels against (β_ R A).inv, and the residual word is the interchange of V ⊗ R with W ⊗ (A ⊗ S).

source

theorem RS.twist_act_coherence {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A V R W S : D) :

The twist-act coherence: extracting A from the twisted factor V ⊗ R before the interchange agrees with interchanging first and then extracting A from the product V ⊗ W. Both words consist of the crossings of A past V, of R past W, and of A past W, each occurring exactly once; the two sides differ only in the order of the first two, which act on disjoint factors and are exchanged as whiskerings.

source

theorem RS.twist_act_coherence_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A V R W S : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj A R) S) ⟶ Z) :

The twist-act coherence: extracting A from the twisted factor V ⊗ R before the interchange agrees with interchanging first and then extracting A from the product V ⊗ W. Both words consist of the crossings of A past V, of R past W, and of A past W, each occurring exactly once; the two sides differ only in the order of the first two, which act on disjoint factors and are exchanged as whiskerings.

Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.TwistCoherence

The twist-shuffle coherence #