The fibre functor is additive

Base change followed by realization is a functor from the ambient category to the super modules over the Γ-algebra, and it is additive: whiskering by the algebra is additive, and realization is composition. Additivity is what makes the fibre functor preserve finite biproducts, and hence what turns a mixed sum into a free super module of the corresponding rank.

The functor is built directly rather than as a composite through the module objects, because the category of module objects carries no additive structure in this development.

noncomputable def RS.fibreFun {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] : CategoryTheory.Functor D (gammaAlgebra D L R).Mod

The fibre functor over an algebra: base change, then realize.

Equations

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

@[simp]

theorem RS.fibreFun_obj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V : D) : (fibreFun L R).obj V = gammaModule D L R (freeMod R V).X

@[simp]

theorem RS.fibreFun_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {V W : D} (f : V ⟶ W) : (fibreFun L R).map f = (gammaModuleFunctor L R).map (freeModMap R f)

instance RS.fibreFun_additive {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] : (fibreFun L R).Additive

The fibre functor is additive.

noncomputable def RS.fibreFunBiproduct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] [CategoryTheory.Limits.HasFiniteBiproducts D] {ι : Type} [Fintype ι] (f : ι → D) : (fibreFun L R).obj (⨁ f) ≅ ⨁ fun (i : ι) => (fibreFun L R).obj (f i)

The fibre functor takes a finite biproduct to a finite biproduct.

Equations

• RS.fibreFunBiproduct L R f = (RS.fibreFun L R).mapBiproduct f