# mathlibdocumentation

category_theory.monoidal.internal.limits

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

def Mon_.limit {J : Type v} {C : Type u} (F : J Mon_ C) :

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
@[simp]
theorem Mon_.limit_one {J : Type v} {C : Type u} (F : J Mon_ C) :

@[simp]
theorem Mon_.limit_X {J : Type v} {C : Type u} (F : J Mon_ C) :

@[simp]

@[simp]
theorem Mon_.limit_cone_X {J : Type v} {C : Type u} (F : J Mon_ C) :
.X =

def Mon_.limit_cone {J : Type v} {C : Type u} (F : J Mon_ C) :

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

Equations
@[simp]
theorem Mon_.limit_cone_π_app_hom {J : Type v} {C : Type u} (F : J Mon_ C) (j : J) :

def Mon_.forget_map_cone_limit_cone_iso {J : Type v} {C : Type u} (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.

Equations
def Mon_.limit_cone_is_limit {J : Type v} {C : Type u} (F : J Mon_ C) :

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

Equations
@[simp]
theorem Mon_.limit_cone_is_limit_lift_hom {J : Type v} {C : Type u} (F : J Mon_ C)  :

@[instance]

@[instance]

Equations