The odd line is self-dual

The square trivialisation of an odd line is an exact pairing of the line with itself. The two triangle identities are forced by the sign of the self-braiding: rearranging a triple of lines cyclically costs two transpositions, hence no sign at all, and the hexagon turns that cyclic rearrangement into a braiding past the trivialisation, which the unit coherences absorb.

theorem RS.neg_id_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (X Y : D) : CategoryTheory.MonoidalCategoryStruct.whiskerRight (-CategoryTheory.CategoryStruct.id X) Y = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

Whiskering a negated identity on the right negates it.

theorem RS.whiskerLeft_neg_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (X Y : D) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (-CategoryTheory.CategoryStruct.id Y) = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

Whiskering a negated identity on the left negates it.

theorem RS.OddLine.cycle_triple {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.whiskerRight (β_ L.obj L.obj).hom L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj L.obj).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj (β_ L.obj L.obj).hom)) = (CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj L.obj).hom

Cyclic rearrangement of a triple of lines is free: the two transpositions each contribute a sign, and the signs cancel.

theorem RS.OddLine.cycle_triple' {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.whiskerLeft L.obj (β_ L.obj L.obj).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj L.obj).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ L.obj L.obj).hom L.obj)) = (CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj L.obj).inv

Cyclic rearrangement of a triple of lines is free, in the mirror grouping.

theorem RS.OddLine.evaluation_coevaluation {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.whiskerRight L.sq.inv L.obj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj L.obj).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj L.sq.hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv

The first triangle identity of the odd line.

theorem RS.OddLine.coevaluation_evaluation {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.whiskerLeft L.obj L.sq.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj L.obj).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight L.sq.hom L.obj)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv

The second triangle identity of the odd line.

@[implicit_reducible]

noncomputable def RS.OddLine.exactPairing {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) : CategoryTheory.ExactPairing L.obj L.obj

The odd line is self-dual: the square trivialisation is an exact pairing of the line with itself.

Equations

• L.exactPairing = { coevaluation' := L.sq.inv, evaluation' := L.sq.hom, coevaluation_evaluation' := ⋯, evaluation_coevaluation' := ⋯ }