Documentation

Mathlib.CategoryTheory.Monoidal.Internal.Limits

Limits of monoid objects. #

If C has limits (of a given shape), 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.

Equations
Instances For

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

    Equations
    • One or more equations did not get rendered due to their size.
    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.

      Equations
      Instances For

        Implementation of Mon_.hasLimits: the proposed cone over a functor F : J ⥤ Mon_ C is a limit cone.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For