Realization as a functor on module objects #
Taking the morphisms out of the two generators is functorial on module objects over a fixed commutative monoid object: the realization of a module map is postcomposition.
noncomputable def
RS.gammaModuleFunctor
{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 (CategoryTheory.Mod D R) (gammaAlgebra D L R).Mod
Realization, as a functor on module objects.
Equations
- One or more equations did not get rendered due to their size.