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.

source

@[instance_reducible]

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

Monoid ↑(F.obj j)

Equations

MonCat.monoidObj F j = (F.obj j).str

source

@[instance_reducible]

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

AddMonoid ↑(F.obj j)

Equations

AddMonCat.addMonoidObj F j = (F.obj j).str

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

@[instance_reducible]

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

Monoid ↑(F.comp (CategoryTheory.forget MonCat)).sections

Equations

MonCat.sectionsMonoid F = (MonCat.sectionsSubmonoid F).toMonoid

source

@[instance_reducible]

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

AddMonoid ↑(F.comp (CategoryTheory.forget AddMonCat)).sections

Equations

AddMonCat.sectionsAddMonoid F = (AddMonCat.sectionsAddSubmonoid F).toAddMonoid

source

@[instance_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

Equations

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

source

@[instance_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

Equations

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

source

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

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

Equations

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

Instances For

source

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

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

Equations

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

Instances For

source

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

Equations

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

Instances For

source

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

Equations

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

Instances For

source

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

Equations

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

Instances For

source

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

Equations

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

Instances For

source

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.

source

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.

source

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.

source

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.

source

instance MonCat.hasLimitsOfSize [UnivLE.{v, u}] :

CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} MonCat

The category of monoids has all limits.

source

instance AddMonCat.hasLimitsOfSize [UnivLE.{v, u}] :

CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddMonCat

The category of additive monoids has all limits.

source

instance MonCat.hasLimits :

CategoryTheory.Limits.HasLimits MonCat

source

instance AddMonCat.hasLimits :

CategoryTheory.Limits.HasLimits AddMonCat

source

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.

source

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.

source

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.

source

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.

source

instance MonCat.forget_preservesLimits :

CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget MonCat)

source

instance AddMonCat.forget_preservesLimits :

CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddMonCat)

source

@[instance_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)

Equations

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

source

@[instance_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)

Equations

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

source

@[instance_reducible]

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

CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget MonCat)

Equations

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

source

@[instance_reducible]

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

CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddMonCat)

Equations

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

source

@[instance_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.

Equations

MonCat.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.3} [CategoryTheory.Category.{?u.1, ?u.3} J] => inferInstance }

source

@[instance_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.

Equations

AddMonCat.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.3} [CategoryTheory.Category.{?u.1, ?u.3} J] => inferInstance }

source

@[instance_reducible]

noncomputable instance MonCat.forget_createsLimits :

CategoryTheory.CreatesLimits (CategoryTheory.forget MonCat)

Equations

MonCat.forget_createsLimits = MonCat.forget_createsLimitsOfSize

source

@[instance_reducible]

noncomputable instance AddMonCat.forget_createsLimits :

CategoryTheory.CreatesLimits (CategoryTheory.forget AddMonCat)

Equations

AddMonCat.forget_createsLimits = AddMonCat.forget_createsLimitsOfSize

source

@[instance_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)

Equations

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

source

@[instance_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)

Equations

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

source

@[instance_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

Equations

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

source

@[instance_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

Equations

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

source

@[instance_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.

Equations

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

source

@[instance_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.

Equations

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

source

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

Equations

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

Instances For

source

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

Equations

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

Instances For

source

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

Equations

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

Instances For

source

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

Equations

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

Instances For

source

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.

source

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.

source

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.

source

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.

source

instance CommMonCat.hasLimitsOfSize [UnivLE.{v, u}] :

CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommMonCat

The category of commutative monoids has all limits.

source

instance AddCommMonCat.hasLimitsOfSize [UnivLE.{v, u}] :

CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddCommMonCat

The category of additive commutative monoids has all limits.

source

instance CommMonCat.hasLimits :

CategoryTheory.Limits.HasLimits CommMonCat

source

instance AddCommMonCat.hasLimits :

CategoryTheory.Limits.HasLimits AddCommMonCat

source

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.

source

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.

source

instance CommMonCat.forget₂Mon_preservesLimits :

CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommMonCat MonCat)

source

instance AddCommMonCat.forget₂Mon_preservesLimits :

CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddCommMonCat AddMonCat)

source

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.

source

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.

source

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.

source

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.

source

instance AddCommMonCat.forget_preservesLimits :

CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddCommMonCat)

source

instance CommMonCat.forget_preservesLimits :

CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommMonCat)

source

@[instance_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)

Equations

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

source

@[instance_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)

Equations

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

source

@[instance_reducible]

noncomputable instance CommMonCat.forget_createsLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] :

CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget MonCat)

Equations

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

source

@[instance_reducible]

noncomputable instance AddCommMonCat.forget_createsLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] :

CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddMonCat)

Equations

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

source

@[instance_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.

Equations

CommMonCat.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.3} [CategoryTheory.Category.{?u.1, ?u.3} J] => inferInstance }

source

@[instance_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.

Equations

AddCommMonCat.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.3} [CategoryTheory.Category.{?u.1, ?u.3} J] => inferInstance }

source

@[instance_reducible]

noncomputable instance CommMonCat.forget_createsLimits :

CategoryTheory.CreatesLimits (CategoryTheory.forget MonCat)

Equations

CommMonCat.forget_createsLimits = CommMonCat.forget_createsLimitsOfSize

source

@[instance_reducible]

noncomputable instance AddCommMonCat.forget_createsLimits :

CategoryTheory.CreatesLimits (CategoryTheory.forget AddMonCat)

Equations

AddCommMonCat.forget_createsLimits = AddCommMonCat.forget_createsLimitsOfSize

Documentation

Mathlib.Algebra.Category.MonCat.Limits

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