Tensoring a mixed sum with the odd line

Tensoring the mixed sum L.mix p q with the odd line exchanges the two kinds of summand: each unit summand becomes a line, by the right unitor, and each line summand becomes a unit, by the square of the line. Reindexing along the swap of the summand labels therefore identifies L.obj ⊗ L.mix p q with the mixed sum L.mix q p of q copies of the unit and p copies of the line.

noncomputable def RS.OddLine.twistSummandIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (p q : ℕ) (j : Fin p ⊕ Fin q) : L.mixFun q p ((Equiv.sumComm (Fin p) (Fin q)) j) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj (L.mixFun p q j)

Tensoring a summand of L.mix p q with the line gives the summand of L.mix q p at the swapped index: a unit summand becomes a line, a line summand becomes a unit.

Equations

• L.twistSummandIso p q (Sum.inl val) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).symm
• L.twistSummandIso p q (Sum.inr val) = L.sq.symm

noncomputable def RS.OddLine.twistMixIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj (L.mix p q) ≅ L.mix q p

Twisting a mixed sum by the line: tensoring with the odd line turns p units and q lines into q units and p lines.

Equations

• L.twistMixIso p q = CategoryTheory.leftDistributor L.obj (L.mixFun p q) ≪≫ CategoryTheory.Limits.biproduct.whiskerEquiv (Equiv.sumComm (Fin p) (Fin q)) (L.twistSummandIso p q)