Commit 2020-08-02 11:46 52c0b421
View on Github →feat(category_theory): Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D (#3576)
When D
is a monoidal category,
monoid objects in C ⥤ D
are the same thing as functors from C
into the monoid objects of D
.
This is formalised as:
Mon_functor_category_equivalence : Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D
The intended application is that asRing ≌ Mon_ Ab
(not yet constructed!), we havepresheaf Ring X ≌ presheaf (Mon_ Ab) X ≌ Mon_ (presheaf Ab X)
, and we can model a module over a presheaf of rings as a module object inpresheaf Ab X
.