mathlib documentation


Limits of monoid objects.

If C has limits, so does Mon_ C, and the forgetful functor preserves these limits.

(This could potentially replace many individual constructions for concrete categories, in particular Mon, SemiRing, Ring, and Algebra R.)

We construct the (candidate) limit of a functor F : J ⥤ Mon_ C by interpreting it as a functor Mon_ (J ⥤ C), and noting that taking limits is a lax monoidal functor, and hence sends monoid objects to monoid objects.


Implementation of Mon_.has_limits: a limiting cone over a functor F : J ⥤ Mon_ C.


The image of the proposed limit cone for F : J ⥤ Mon_ C under the forgetful functor forget C : Mon_ C ⥤ C is isomorphic to the limit cone of F ⋙ forget C.