Contracting the shuffle of two odd twists

The comparison map of Deligne's (2.11.1) at the free module of the odd line against itself is a shuffle of two morphisms into R ⊗ 1-bar followed by the contraction of the two odd legs. Every such morphism is a morphism into R with an odd leg attached, and the whole composite then splits: the algebra factors multiply, and what is left is a pure coherence identity between the two ways of contracting the two odd legs.

The four instances of that coherence identity — one for each pair of parities — are the content of this file. Two of them carry a sign, and the sign is the self-braiding of the odd line.

theorem RS.shuffle_contract {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] {A B A' B' : D} (y : A' ⟶ R) (z : B' ⟶ R) (pA : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A' L.obj) (pB : B ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B' L.obj) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp pA (CategoryTheory.MonoidalCategoryStruct.whiskerRight y L.obj)) (CategoryTheory.CategoryStruct.comp pB (CategoryTheory.MonoidalCategoryStruct.whiskerRight z L.obj))) (CategoryTheory.CategoryStruct.comp (freeModShuffle R L.obj L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom pA pB) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ A' L.obj B' L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj A' B') L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj A' B')).hom))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom y z) CategoryTheory.MonObj.mul)

Splitting off the algebra factors. If two morphisms into R ⊗ 1-bar are a morphism into R with an odd leg attached, then shuffling them and contracting the two odd legs multiplies the two morphisms into R, after a pure contraction of the odd legs.

The four contraction identities

theorem RS.tensorμ_oddLine {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (A : D) : CategoryTheory.MonoidalCategory.tensorμ A L.obj L.obj L.obj = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj A L.obj) (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj L.obj))

The middle-four interchange across two odd lines is minus the identity: its only braiding is the self-braiding of the line.

theorem RS.oddContract_neg {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) {A A' : D} (pA : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A' L.obj) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom pA L.sq.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ A' L.obj L.obj L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj A' L.obj) L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj A' L.obj)).hom))) = -pA

Contraction against a coevaluation carries a sign: the two odd legs cross.

theorem RS.oddContract_pos {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) {A A' : D} (pA : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A' L.obj) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom pA (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ A' L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj A' (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj A' (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight pA L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A' L.obj L.obj).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A' L.sq.hom))

Contraction against a unitor carries no sign: the free odd leg passes only the unit.

theorem RS.oddContract_ee {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom L.sq.inv L.sq.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ L.obj L.obj L.obj L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj L.obj) L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj L.obj)).hom))) = -L.sq.inv

The even–even contraction: a sign.

theorem RS.oddContract_oe {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv L.sq.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj L.obj L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj) L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj)).hom))) = -(CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv

The odd–even contraction: a sign.

theorem RS.oddContract_oo {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) : CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))).hom))) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv

The odd–odd contraction: no sign.

theorem RS.oddContract_eo {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom L.sq.inv (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ L.obj L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))).hom))) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv

The even–odd contraction: no sign; it is the triangle identity of the odd line.