The fibre functor over an algebra

Deligne's ω of 2.11: base change to the algebra, then take the morphisms out of the two generators. Both steps are functorial, so ω is a functor from the category to the super modules over the Γ-algebra of the base.

@[reducible, inline]

noncomputable abbrev RS.fibreObj {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (X : CategoryTheory.Ind C) : CategoryTheory.Ind C

The base change of an object, as a module object.

Equations

• RS.fibreObj A X = (RS.freeMod A X).X

noncomputable def RS.fibreFunctor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] : CategoryTheory.Functor (CategoryTheory.Ind C) (gammaAlgebra (CategoryTheory.Ind C) L A).Mod

The fibre functor over an algebra (Deligne 2.11): base change and realize.

Equations

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