Transporting an odd line along a monoidal functor

A strong braided monoidal additive functor carries an odd line to an odd line: the square of the image is the image of the square, and the self-braiding of the image is the image of the self-braiding, which is minus an identity.

noncomputable def RS.OddLine.map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.SymmetricCategory B] [CategoryTheory.Preadditive B] (F : CategoryTheory.Functor A B) [F.Braided] [F.Additive] (L : OddLine A) : OddLine B

The image of an odd line under a strong braided monoidal additive functor is an odd line.

Equations

• One or more equations did not get rendered due to their size.