Restriction of Deligne packages

A Deligne fibre-functor package restricts along any braided monoidal, additive, ℂ-linear functor: compose the fibre functor with the embedding.

noncomputable def RS.DelignePackage.restrict {A : Type u_1} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] {B : Type u_2} [CategoryTheory.Category.{u_4, u_2} B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.SymmetricCategory B] [CategoryTheory.Preadditive B] [CategoryTheory.Linear ℂ B] (F : CategoryTheory.Functor B A) [F.Braided] [F.Additive] [CategoryTheory.Functor.Linear ℂ F] (P : DelignePackage A) : DelignePackage B

Restrict a Deligne package along a braided linear functor.

Equations

• RS.DelignePackage.restrict F P = { ω := F.comp P.ω, braided := inferInstance, additive := ⋯, linear := ⋯ }