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

noncomputable 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) :
(Mon_.limit F).one = {X := 𝟙_ C _inst_4, π := {app := λ (j : J), 𝟙 (𝟙_ C), naturality' := _}})
@[simp]
theorem Mon_.limit_X {J : Type v} {C : Type u} (F : J Mon_ C) :
@[simp]
theorem Mon_.limit_mul {J : Type v} {C : Type u} (F : J Mon_ C) :
(Mon_.limit F).mul = {X := , π := {app := λ (j : J), , naturality' := _}})
@[simp]
theorem Mon_.limit_cone_X {J : Type v} {C : Type u} (F : J Mon_ C) :
.X =
noncomputable 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) :
noncomputable 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
noncomputable 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)  :
@[protected, instance]
@[protected, instance]
noncomputable def Mon_.forget_preserves_limits {C : Type u}  :
Equations