Commit 2020-08-02 11:46 52c0b421

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 as Ring ≌ Mon_ Ab (not yet constructed!), we have presheaf 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 in presheaf Ab X.