# Documentation

Mathlib.CategoryTheory.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 MonCat, SemiRingCat, RingCat, and AlgebraCat R.)

@[simp]
theorem Mon_.limit_one {J : Type v} {C : Type u} (F : ) :
().one = CategoryTheory.Limits.limit.lift () (().obj { pt := CategoryTheory.MonoidalCategory.tensorUnit', π := CategoryTheory.NatTrans.mk fun j => CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit' })
@[simp]
theorem Mon_.limit_mul {J : Type v} {C : Type u} (F : ) :
().mul = CategoryTheory.Limits.limit.lift () (().obj { pt := , π := CategoryTheory.NatTrans.mk fun j => })
@[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.

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

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

Instances For
def Mon_.forgetMapConeLimitConeIso {J : Type v} {C : Type u} (F : ) :
().mapCone ()

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

Instances For
instance Mon_.hasLimits {C : Type u} :