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.

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

Equations

• Eq (MonCat.monoidObj F j) (inferInstanceAs (Monoid (F.obj j).carrier))

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

Equations

• Eq (AddMonCat.addMonoidObj F j) (inferInstanceAs (AddMonoid (F.obj j).carrier))

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

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

Equations

• Eq (MonCat.sectionsSubmonoid F) { carrier := (F.comp (CategoryTheory.forget MonCat)).sections, mul_mem' := ⋯, one_mem' := ⋯ }

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

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

Equations

• Eq (AddMonCat.sectionsAddSubmonoid F) { carrier := (F.comp (CategoryTheory.forget AddMonCat)).sections, add_mem' := ⋯, zero_mem' := ⋯ }

def MonCat.sectionsMonoid {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J MonCat) : Monoid (F.comp (CategoryTheory.forget MonCat)).sections.Elem

Equations

• Eq (MonCat.sectionsMonoid F) (MonCat.sectionsSubmonoid F).toMonoid

def AddMonCat.sectionsAddMonoid {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J AddMonCat) : AddMonoid (F.comp (CategoryTheory.forget AddMonCat)).sections.Elem

Equations

• Eq (AddMonCat.sectionsAddMonoid F) (AddMonCat.sectionsAddSubmonoid F).toAddMonoid

noncomputable def MonCat.limitMonoid {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J MonCat) [Small (F.comp (CategoryTheory.forget MonCat)).sections.Elem] : Monoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt

Equations

• Eq (MonCat.limitMonoid F) (inferInstanceAs (Monoid (Shrink (F.comp (CategoryTheory.forget MonCat)).sections.Elem)))

noncomputable def AddMonCat.limitAddMonoid {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J AddMonCat) [Small (F.comp (CategoryTheory.forget AddMonCat)).sections.Elem] : AddMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt

Equations

• Eq (AddMonCat.limitAddMonoid F) (inferInstanceAs (AddMonoid (Shrink (F.comp (CategoryTheory.forget AddMonCat)).sections.Elem)))

noncomputable def MonCat.limitπMonoidHom {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J MonCat) [Small (F.comp (CategoryTheory.forget MonCat)).sections.Elem] (j : J) : MonoidHom (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.

Equations

• Eq (MonCat.limitπMonoidHom F j) { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).π.app j, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def AddMonCat.limitπAddMonoidHom {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J AddMonCat) [Small (F.comp (CategoryTheory.forget AddMonCat)).sections.Elem] (j : J) : AddMonoidHom (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.

Equations

• Eq (AddMonCat.limitπAddMonoidHom F j) { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).π.app j, map_zero' := ⋯, map_add' := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

(Internal use only; use the limits API.)

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

(Internal use only; use the limits API.)

Equations

• One or more equations did not get rendered due to their size.

theorem MonCat.HasLimits.hasLimit {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J MonCat) [Small (F.comp (CategoryTheory.forget MonCat)).sections.Elem] : CategoryTheory.Limits.HasLimit F

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

theorem AddMonCat.HasLimits.hasLimit {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J AddMonCat) [Small (F.comp (CategoryTheory.forget AddMonCat)).sections.Elem] : CategoryTheory.Limits.HasLimit F

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

theorem MonCat.HasLimits.hasLimitsOfShape {J : Type v} [CategoryTheory.Category J] [Small J] : CategoryTheory.Limits.HasLimitsOfShape J MonCat

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

theorem AddMonCat.HasLimits.hasLimitsOfShape {J : Type v} [CategoryTheory.Category J] [Small J] : CategoryTheory.Limits.HasLimitsOfShape J AddMonCat

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

theorem MonCat.hasLimitsOfSize [UnivLE] : CategoryTheory.Limits.HasLimitsOfSize MonCat

The category of monoids has all limits.

theorem AddMonCat.hasLimitsOfSize [UnivLE] : CategoryTheory.Limits.HasLimitsOfSize AddMonCat

The category of additive monoids has all limits.

theorem MonCat.hasLimits : CategoryTheory.Limits.HasLimits MonCat

theorem AddMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddMonCat

theorem MonCat.forget_preservesLimitsOfShape {J : Type v} [CategoryTheory.Category J] [Small J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget MonCat)

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

theorem AddMonCat.forget_preservesLimitsOfShape {J : Type v} [CategoryTheory.Category J] [Small J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddMonCat)

If J is u-small, the forgetful functor from AddMonCat.{u}

preserves limits of shape J.

theorem MonCat.forget_preservesLimitsOfSize [UnivLE] : CategoryTheory.Limits.PreservesLimitsOfSize (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.

theorem AddMonCat.forget_preservesLimitsOfSize [UnivLE] : CategoryTheory.Limits.PreservesLimitsOfSize (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.

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Eq MonCat.forget_createsLimitsOfShape { CreatesLimit := fun {K : CategoryTheory.Functor J MonCat} => inferInstance }

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

Equations

• Eq AddMonCat.forget_createsLimitsOfShape { CreatesLimit := fun {K : CategoryTheory.Functor J AddMonCat} => inferInstance }

noncomputable def MonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize (CategoryTheory.forget MonCat)

The forgetful functor from monoids to types preserves all limits.

Equations

• Eq MonCat.forget_createsLimitsOfSize { CreatesLimitsOfShape := fun {J : Type ?u.11} [CategoryTheory.Category J] => inferInstance }

noncomputable def AddMonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize (CategoryTheory.forget AddMonCat)

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

Equations

• Eq AddMonCat.forget_createsLimitsOfSize { CreatesLimitsOfShape := fun {J : Type ?u.11} [CategoryTheory.Category J] => inferInstance }

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

Equations

• Eq MonCat.forget_createsLimits MonCat.forget_createsLimitsOfSize

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

Equations

• Eq AddMonCat.forget_createsLimits AddMonCat.forget_createsLimitsOfSize

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

Equations

• Eq (CommMonCat.commMonoidObj F j) (inferInstanceAs (CommMonoid (F.obj j).carrier))

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

Equations

• Eq (AddCommMonCat.addCommMonoidObj F j) (inferInstanceAs (AddCommMonoid (F.obj j).carrier))

noncomputable def CommMonCat.limitCommMonoid {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J CommMonCat) [Small (F.comp (CategoryTheory.forget CommMonCat)).sections.Elem] : CommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommMonCat))).pt

Equations

• Eq (CommMonCat.limitCommMonoid F) (inferInstanceAs (CommMonoid (Shrink (F.comp (CategoryTheory.forget CommMonCat)).sections.Elem)))

noncomputable def AddCommMonCat.limitAddCommMonoid {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J AddCommMonCat) [Small (F.comp (CategoryTheory.forget AddCommMonCat)).sections.Elem] : AddCommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddCommMonCat))).pt

Equations

• Eq (AddCommMonCat.limitAddCommMonoid F) (inferInstanceAs (AddCommMonoid (Shrink (F.comp (CategoryTheory.forget AddCommMonCat)).sections.Elem)))

theorem CommMonCat.instSmallElemForallObjCompMonCatForget₂ForgetSections {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J CommMonCat) [Small (F.comp (CategoryTheory.forget CommMonCat)).sections.Elem] : Small ((F.comp (CategoryTheory.forget₂ CommMonCat MonCat)).comp (CategoryTheory.forget MonCat)).sections.Elem

theorem AddCommMonCat.instSmallElemForallObjCompMonCatForget₂ForgetSections {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J AddCommMonCat) [Small (F.comp (CategoryTheory.forget AddCommMonCat)).sections.Elem] : Small ((F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)).comp (CategoryTheory.forget AddMonCat)).sections.Elem

noncomputable def CommMonCat.forget₂CreatesLimit {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J CommMonCat) [Small (F.comp (CategoryTheory.forget CommMonCat)).sections.Elem] : 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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommMonCat.forget₂CreatesLimit {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J AddCommMonCat) [Small (F.comp (CategoryTheory.forget AddCommMonCat)).sections.Elem] : 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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Eq (CommMonCat.limitCone F) (CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))))

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

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

Equations

• Eq (AddCommMonCat.limitCone F) (CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))))

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

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

Equations

• Eq (CommMonCat.limitConeIsLimit F) (CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))))

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

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

Equations

• Eq (AddCommMonCat.limitConeIsLimit F) (CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))))

theorem CommMonCat.hasLimit {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J CommMonCat) [Small (F.comp (CategoryTheory.forget CommMonCat)).sections.Elem] : CategoryTheory.Limits.HasLimit F

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

theorem AddCommMonCat.hasLimit {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J AddCommMonCat) [Small (F.comp (CategoryTheory.forget AddCommMonCat)).sections.Elem] : CategoryTheory.Limits.HasLimit F

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

theorem CommMonCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category J] [Small J] : CategoryTheory.Limits.HasLimitsOfShape J CommMonCat

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

theorem AddCommMonCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category J] [Small J] : CategoryTheory.Limits.HasLimitsOfShape J AddCommMonCat

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

theorem CommMonCat.hasLimitsOfSize [UnivLE] : CategoryTheory.Limits.HasLimitsOfSize CommMonCat

The category of commutative monoids has all limits.

theorem AddCommMonCat.hasLimitsOfSize [UnivLE] : CategoryTheory.Limits.HasLimitsOfSize AddCommMonCat

The category of additive commutative monoids has all limits.

theorem CommMonCat.hasLimits : CategoryTheory.Limits.HasLimits CommMonCat

theorem AddCommMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommMonCat

theorem CommMonCat.forget₂Mon_preservesLimitsOfSize [UnivLE] : CategoryTheory.Limits.PreservesLimitsOfSize (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.

theorem AddCommMonCat.forget₂AddMonPreservesLimitsOfSize [UnivLE] : CategoryTheory.Limits.PreservesLimitsOfSize (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.

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

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

theorem CommMonCat.forget_preservesLimitsOfShape {J : Type v} [CategoryTheory.Category J] [Small J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget CommMonCat)

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

theorem AddCommMonCat.forget_preservesLimitsOfShape {J : Type v} [CategoryTheory.Category J] [Small J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddCommMonCat)

If J is u-small, the forgetful functor from AddCommMonCat.{u}

preserves limits of shape J.

theorem CommMonCat.forget_preservesLimitsOfSize [UnivLE] : CategoryTheory.Limits.PreservesLimitsOfSize (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.

theorem AddCommMonCat.forget_preservesLimitsOfSize [UnivLE] : CategoryTheory.Limits.PreservesLimitsOfSize (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.

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

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

noncomputable def CommMonCat.forget_createsLimit {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J CommMonCat) [Small (F.comp (CategoryTheory.forget CommMonCat)).sections.Elem] : CategoryTheory.CreatesLimit F (CategoryTheory.forget CommMonCat)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommMonCat.forget_createsLimit {J : Type v} [CategoryTheory.Category J] (F : CategoryTheory.Functor J AddCommMonCat) [Small (F.comp (CategoryTheory.forget AddCommMonCat)).sections.Elem] : CategoryTheory.CreatesLimit F (CategoryTheory.forget AddCommMonCat)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Eq CommMonCat.forget_createsLimitsOfShape { CreatesLimit := fun {K : CategoryTheory.Functor J MonCat} => inferInstance }

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

Equations

• Eq AddCommMonCat.forget_createsLimitsOfShape { CreatesLimit := fun {K : CategoryTheory.Functor J AddMonCat} => inferInstance }

noncomputable def CommMonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize (CategoryTheory.forget MonCat)

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

Equations

• Eq CommMonCat.forget_createsLimitsOfSize { CreatesLimitsOfShape := fun {J : Type ?u.11} [CategoryTheory.Category J] => inferInstance }

noncomputable def AddCommMonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize (CategoryTheory.forget AddMonCat)

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

Equations

• Eq AddCommMonCat.forget_createsLimitsOfSize { CreatesLimitsOfShape := fun {J : Type ?u.11} [CategoryTheory.Category J] => inferInstance }

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

Equations

• Eq CommMonCat.forget_createsLimits CommMonCat.forget_createsLimitsOfSize

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

Equations

• Eq AddCommMonCat.forget_createsLimits AddCommMonCat.forget_createsLimitsOfSize