mathlib3 documentation


Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

The intended application is that as RingMon_ 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.

Future work #

Presumably this statement is not specific to monoids, and could be generalised to any internal algebraic objects, if the appropriate framework was available.

Functor translating a monoid object in a functor category to a functor into the category of monoid objects.


Functor translating a functor into the category of monoid objects to a monoid object in the functor category