The category of (commutative) (additive) monoids has all limits

Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

@[implicit_reducible]

instance MonCat.monoidObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) (j : J) : Monoid ((F.comp (CategoryTheory.forget MonCat)).obj j)

@[implicit_reducible]

instance AddMonCat.addMonoidObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) (j : J) : AddMonoid ((F.comp (CategoryTheory.forget AddMonCat)).obj j)

def MonCat.sectionsSubmonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) : Submonoid ((j : J) → ↑(F.obj j))

The flat sections of a functor into MonCat form a submonoid of all sections.

def AddMonCat.sectionsAddSubmonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) : AddSubmonoid ((j : J) → ↑(F.obj j))

The flat sections of a functor into AddMonCat form an additive submonoid of all sections.

@[implicit_reducible]

instance MonCat.sectionsMonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) : Monoid ↑(F.comp (CategoryTheory.forget MonCat)).sections

@[implicit_reducible]

instance AddMonCat.sectionsAddMonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) : AddMonoid ↑(F.comp (CategoryTheory.forget AddMonCat)).sections

@[implicit_reducible]

noncomputable instance MonCat.limitMonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] : Monoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt

@[implicit_reducible]

noncomputable instance AddMonCat.limitAddMonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] : AddMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt

noncomputable def MonCat.limitπMonoidHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt →* (F.comp (CategoryTheory.forget MonCat)).obj j

limit.π (F ⋙ forget MonCat) j as a MonoidHom.

noncomputable def AddMonCat.limitπAddMonoidHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt →+ (F.comp (CategoryTheory.forget AddMonCat)).obj j

limit.π (F ⋙ forget AddMonCat) j as an AddMonoidHom.

noncomputable def MonCat.HasLimits.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] : CategoryTheory.Limits.Cone F

Construction of a limit cone in MonCat. (Internal use only; use the limits API.)

noncomputable def AddMonCat.HasLimits.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] : CategoryTheory.Limits.Cone F

(Internal use only; use the limits API.)

noncomputable def MonCat.HasLimits.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] : CategoryTheory.Limits.IsLimit (limitCone F)

Witness that the limit cone in MonCat is a limit cone. (Internal use only; use the limits API.)

noncomputable def AddMonCat.HasLimits.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] : CategoryTheory.Limits.IsLimit (limitCone F)

(Internal use only; use the limits API.)

instance MonCat.HasLimits.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget MonCat).sections is u-small, F has a limit.

instance AddMonCat.HasLimits.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget AddMonCat).sections is u-small, F has a limit.

instance MonCat.HasLimits.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J MonCat

If J is u-small, MonCat.{u} has limits of shape J.

instance AddMonCat.HasLimits.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J AddMonCat

If J is u-small, AddMonCat.{u} has limits of shape J.

instance MonCat.hasLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} MonCat

The category of monoids has all limits.

instance AddMonCat.hasLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddMonCat

The category of additive monoids has all limits.

instance MonCat.hasLimits : CategoryTheory.Limits.HasLimits MonCat

instance AddMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddMonCat

instance MonCat.forget_preservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget MonCat)

If J is u-small, the forgetful functor from MonCat.{u} preserves limits of shape J.

instance AddMonCat.forget_preservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddMonCat)

If J is u-small, the forgetful functor from AddMonCat.{u} preserves limits of shape J.

instance MonCat.forget_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget MonCat)

The forgetful functor from monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

instance AddMonCat.forget_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddMonCat)

The forgetful functor from additive monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

instance MonCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget MonCat)

instance AddMonCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddMonCat)

@[implicit_reducible]

noncomputable instance MonCat.forget_createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) : CategoryTheory.CreatesLimit F (CategoryTheory.forget MonCat)

@[implicit_reducible]

noncomputable instance AddMonCat.forget_createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) : CategoryTheory.CreatesLimit F (CategoryTheory.forget AddMonCat)

@[implicit_reducible]

noncomputable instance MonCat.forget_createsLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget MonCat)

@[implicit_reducible]

noncomputable instance AddMonCat.forget_createsLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddMonCat)

@[implicit_reducible]

noncomputable instance MonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget MonCat)

The forgetful functor from monoids to types preserves all limits.

@[implicit_reducible]

noncomputable instance AddMonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddMonCat)

The forgetful functor from additive monoids to types preserves all limits.

@[implicit_reducible]

noncomputable instance MonCat.forget_createsLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget MonCat)

@[implicit_reducible]

noncomputable instance AddMonCat.forget_createsLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget AddMonCat)

@[implicit_reducible]

instance CommMonCat.commMonoidObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) (j : J) : CommMonoid ((F.comp (CategoryTheory.forget CommMonCat)).obj j)

@[implicit_reducible]

instance AddCommMonCat.addCommMonoidObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) (j : J) : AddCommMonoid ((F.comp (CategoryTheory.forget AddCommMonCat)).obj j)

@[implicit_reducible]

noncomputable instance CommMonCat.limitCommMonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommMonCat))).pt

@[implicit_reducible]

noncomputable instance AddCommMonCat.limitAddCommMonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : AddCommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddCommMonCat))).pt

instance CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ CommMonCat MonCat)).comp (CategoryTheory.forget MonCat)).sections

instance AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)).comp (CategoryTheory.forget AddMonCat)).sections

@[implicit_reducible]

noncomputable instance CommMonCat.forget₂CreatesLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommMonCat MonCat)

We show that the forgetful functor CommMonCat ⥤ MonCat creates limits.

All we need to do is notice that the limit point has a CommMonoid instance available, and then reuse the existing limit.

@[implicit_reducible]

noncomputable instance AddCommMonCat.forget₂CreatesLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)

We show that the forgetful functor AddCommMonCat ⥤ AddMonCat creates limits.

All we need to do is notice that the limit point has an AddCommMonoid instance available, and then reuse the existing limit.

noncomputable def CommMonCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor into CommMonCat. (Generally, you'll just want to use limit F.)

noncomputable def AddCommMonCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor into AddCommMonCat. (Generally, you'll just want to use limit F.)

noncomputable def CommMonCat.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.Limits.IsLimit (limitCone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

noncomputable def AddCommMonCat.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.Limits.IsLimit (limitCone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

instance CommMonCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget CommMonCat).sections is u-small, F has a limit.

instance AddCommMonCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget AddCommMonCat).sections is u-small, F has a limit.

instance CommMonCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J CommMonCat

If J is u-small, CommMonCat.{u} has limits of shape J.

instance AddCommMonCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J AddCommMonCat

If J is u-small, AddCommMonCat.{u} has limits of shape J.

instance CommMonCat.hasLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommMonCat

The category of commutative monoids has all limits.

instance AddCommMonCat.hasLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddCommMonCat

The category of additive commutative monoids has all limits.

instance CommMonCat.hasLimits : CategoryTheory.Limits.HasLimits CommMonCat

instance AddCommMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommMonCat

instance CommMonCat.forget₂Mon_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommMonCat MonCat)

The forgetful functor from commutative monoids to monoids preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of monoids.

instance AddCommMonCat.forget₂AddMonPreservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddCommMonCat AddMonCat)

The forgetful functor from additive commutative monoids to additive monoids preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of additive monoids.

instance CommMonCat.forget₂Mon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommMonCat MonCat)

instance AddCommMonCat.forget₂Mon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddCommMonCat AddMonCat)

instance CommMonCat.forget_preservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget CommMonCat)

If J is u-small, the forgetful functor from CommMonCat.{u} preserves limits of shape J.

instance AddCommMonCat.forget_preservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddCommMonCat)

If J is u-small, the forgetful functor from AddCommMonCat.{u} preserves limits of shape J.

instance CommMonCat.forget_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommMonCat)

The forgetful functor from commutative monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

instance AddCommMonCat.forget_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddCommMonCat)

The forgetful functor from additive commutative monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

instance AddCommMonCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddCommMonCat)

instance CommMonCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommMonCat)

@[implicit_reducible]

noncomputable instance CommMonCat.forget_createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget CommMonCat)

@[implicit_reducible]

noncomputable instance AddCommMonCat.forget_createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget AddCommMonCat)

@[implicit_reducible]

noncomputable instance CommMonCat.forget_createsLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget MonCat)

@[implicit_reducible]

noncomputable instance AddCommMonCat.forget_createsLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddMonCat)

@[implicit_reducible]

noncomputable instance CommMonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget MonCat)

The forgetful functor from commutative monoids to types preserves all limits.

@[implicit_reducible]

noncomputable instance AddCommMonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddMonCat)

The forgetful functor from commutative additive monoids to types preserves all limits.

@[implicit_reducible]

noncomputable instance CommMonCat.forget_createsLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget MonCat)

@[implicit_reducible]

noncomputable instance AddCommMonCat.forget_createsLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget AddMonCat)