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

def CategoryTheory.Mon.limit {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : Mon C

We construct the limit object of a functor F : J ⥤ Mon C given a limit cone c of F ⋙ forget C.

@[simp]

theorem CategoryTheory.Mon.limit_mon_one {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : MonObj.one = hc.lift { pt := MonoidalCategoryStruct.tensorUnit C, π := { app := fun (X : J) => MonObj.one, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Mon.limit_mon_mul {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : MonObj.mul = hc.lift { pt := MonoidalCategoryStruct.tensorObj c.1 c.1, π := { app := fun (X : J) => CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (c.π.app X) (c.π.app X)) MonObj.mul, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Mon.limit_X {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (limit F c hc).X = c.pt

def CategoryTheory.Mon.limitCone {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : Limits.Cone F

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

@[simp]

theorem CategoryTheory.Mon.limitCone_pt {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (limitCone F c hc).pt = limit F c hc

@[simp]

theorem CategoryTheory.Mon.limitCone_π_app_hom {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) (j : J) : ((limitCone F c hc).π.app j).hom = c.π.app j

def CategoryTheory.Mon.forgetMapConeLimitConeIso {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (forget C).mapCone (limitCone F c hc) ≅ 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.

@[simp]

theorem CategoryTheory.Mon.forgetMapConeLimitConeIso_inv_hom {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (forgetMapConeLimitConeIso F c hc).inv.hom = CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.Mon.forgetMapConeLimitConeIso_hom_hom {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (forgetMapConeLimitConeIso F c hc).hom.hom = CategoryStruct.id c.pt

def CategoryTheory.Mon.limitConeIsLimit {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : Limits.IsLimit (limitCone F c hc)

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

@[simp]

theorem CategoryTheory.Mon.limitConeIsLimit_lift_hom {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) (s : Limits.Cone F) : ((limitConeIsLimit F c hc).lift s).hom = hc.lift ((forget C).mapCone s)

def CategoryTheory.Mon.limitConeLiftsToLimit {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : LiftsToLimit F (forget C) c hc

A helper definition to show that the forgetful functor forget C : Mon C ⥤ C creates limits: given a limit cone c of F ⋙ forget C, we can lift it to a limit cone of F.

@[implicit_reducible]

instance CategoryTheory.Mon.instCreatesLimitForget {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) : CreatesLimit F (forget C)

@[implicit_reducible]

instance CategoryTheory.Mon.instCreatesLimitsOfShapeForget {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : CreatesLimitsOfShape J (forget C)

@[implicit_reducible]

instance CategoryTheory.Mon.instCreatesLimitsOfSizeForget {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : CreatesLimitsOfSize.{w, u_1, v, v, max u v, u} (forget C)

@[implicit_reducible]

instance CategoryTheory.Mon.instCreatesLimitsForget {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : CreatesLimits (forget C)

instance CategoryTheory.Mon.instHasLimitsOfShape {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasLimitsOfShape J C] : Limits.HasLimitsOfShape J (Mon C)

instance CategoryTheory.Mon.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasLimitsOfShape J C] : Limits.PreservesLimitsOfShape J (forget C)