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 AlgCat R.)

source

def Mon_.limit {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (Mon_ C)) :

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

Instances For

source

@[simp]

theorem Mon_.limit_mon_one {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (Mon_ C)) :

Mon_Class.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim) (CategoryTheory.Limits.limMap Mon_Class.one)

source

@[simp]

theorem Mon_.limit_mon_mul {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (Mon_ C)) :

Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim (F.comp (forget C)) (F.comp (forget C))) (CategoryTheory.Limits.limMap Mon_Class.mul)

source

@[simp]

theorem Mon_.limit_X {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (Mon_ C)) :

(limit F).X = CategoryTheory.Limits.limit (F.comp (forget C))

source

def Mon_.limitCone {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (Mon_ C)) :

CategoryTheory.Limits.Cone F

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

Equations

Instances For

source

@[simp]

theorem Mon_.limitCone_pt {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (Mon_ C)) :

(limitCone F).pt = limit F

source

@[simp]

theorem Mon_.limitCone_π_app_hom {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (Mon_ C)) (j : J) :

((limitCone F).π.app j).hom = CategoryTheory.Limits.limit.π (F.comp (forget C)) j

source

def Mon_.forgetMapConeLimitConeIso {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (Mon_ C)) :

(forget C).mapCone (limitCone F) ≅ CategoryTheory.Limits.limit.cone (F.comp (forget 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

Instances For

source