# 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.)

@[simp]
theorem Mon_.limit_one {J : Type v} {C : Type u} (F : ) :
().one = CategoryTheory.Limits.limit.lift (F.comp ()) ( { pt := 𝟙_ C, π := { app := fun (j : J) => , naturality := } })
@[simp]
theorem Mon_.limit_mul {J : Type v} {C : Type u} (F : ) :
@[simp]
theorem Mon_.limit_X {J : Type v} {C : Type u} (F : ) :
def Mon_.limit {J : Type v} {C : Type u} (F : ) :

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
• = CategoryTheory.Limits.limLax.mapMon.obj (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.obj F)
Instances For
@[simp]
theorem Mon_.limitCone_pt {J : Type v} {C : Type u} (F : ) :
().pt =
@[simp]
theorem Mon_.limitCone_π_app_hom {J : Type v} {C : Type u} (F : ) (j : J) :
(().app j).hom = CategoryTheory.Limits.limit.π (F.comp ()) j
def Mon_.limitCone {J : Type v} {C : Type u} (F : ) :

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
def Mon_.forgetMapConeLimitConeIso {J : Type v} {C : Type u} (F : ) :
().mapCone () CategoryTheory.Limits.limit.cone (F.comp ())

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
@[simp]
theorem Mon_.limitConeIsLimit_lift_hom {J : Type v} {C : Type u} (F : ) (s : ) :
(.lift s).hom = CategoryTheory.Limits.limit.lift (F.comp ()) (().mapCone s)
def Mon_.limitConeIsLimit {J : Type v} {C : Type u} (F : ) :

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
instance Mon_.hasLimits {C : Type u} :
Equations
• =
Equations
• One or more equations did not get rendered due to their size.