mathlib documentation


Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D

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