The odd line of the doubling #
The ℤ/2-graded doubling of a tensor category always contains an
odd line: the monoidal unit placed in odd degree squares to the
unit and self-braids by −1. This is Deligne's device for the
general case of 2.11, where the category itself need not contain
such an object.
noncomputable def
RS.doubledOddLine
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.MonoidalCategory A]
[CategoryTheory.SymmetricCategory A]
[CategoryTheory.Preadditive A]
[CategoryTheory.MonoidalPreadditive A]
[CategoryTheory.Limits.HasBinaryBiproducts A]
[CategoryTheory.Limits.HasZeroObject A]
:
The odd line of the doubling: the unit in odd degree.
Equations
- RS.doubledOddLine = { obj := RS.Doubled.oddUnit, sq := RS.Doubled.oddUnitSq, braid_neg := ⋯ }