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 MonCat
, SemiRingCat
, RingCat
, and AlgebraCat 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.
Instances For
Implementation of Mon_.hasLimits
: a limiting cone over a functor F : J ⥤ Mon_ C
.
Instances For
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
.
Instances For
Implementation of Mon_.hasLimits
:
the proposed cone over a functor F : J ⥤ Mon_ C
is a limit cone.