The Deligne fibre-functor interface

What the development actually consumes from a fibre functor. Deligne's theorem is stated with his own hypotheses in DeligneTheorem.lean, and its conclusion is DeligneFibreFunctor: an exact, faithful, ℂ-linear symmetric monoidal functor to super vector spaces. Only the symmetric monoidal ℂ-linear structure is used downstream, so exactness and faithfulness are forgotten here, by DeligneFibreFunctor.toPackage. Weakening the interface weakens what is assumed.

The package is stated over an arbitrary carrier, so it can be instantiated at the constructed envelope; the hypotheses of the cited theorem are discharged for that envelope in RS/Novel/Envelope/EnvDelignePackage.lean.

structure RS.DelignePackage (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] : Type (max (max 1 u_1) u_2)

The Deligne fibre-functor input for a candidate tensor category: a ℂ-linear symmetric monoidal functor into SuperVect. This is the conclusion of Deligne's theorem for a category satisfying its hypotheses, weakened to the structure the Regts–Sevenster extraction consumes.

• ω : CategoryTheory.Functor A SuperVect

  The fibre functor.

• braided : self.ω.Braided

  The fibre functor is symmetric monoidal.

• additive : self.ω.Additive

  The fibre functor is additive.

• linear : CategoryTheory.Functor.Linear ℂ self.ω

  The fibre functor is ℂ-linear.