# mathlibdocumentation

algebra.category.Mon.limits

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

@[instance]
@[instance]
def Mon.monoid_obj {J : Type u} (F : J Mon) (j : J) :
Equations
add_submonoid (Π (j : J), (F.obj j))

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

def Mon.sections_submonoid {J : Type u} (F : J Mon) :
submonoid (Π (j : J), (F.obj j))

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

Equations
@[instance]
@[instance]
def Mon.limit_monoid {J : Type u} (F : J Mon) :
Equations

limit.π (F ⋙ forget AddMon) j as an add_monoid_hom.

def Mon.limit_π_monoid_hom {J : Type u} (F : J Mon) (j : J) :

limit.π (F ⋙ forget Mon) j as a monoid_hom.

Equations
def Mon.has_limits.limit_cone {J : Type u} (F : J Mon) :

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

Equations

(Internal use only; use the limits API.)

def Mon.has_limits.limit_cone_is_limit {J : Type u} (F : J Mon) :

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

Equations

(Internal use only; use the limits API.)

@[instance]

The category of monoids has all limits.

@[instance]
@[instance]

The forgetful functor from monoids to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations
@[instance]
def CommMon.comm_monoid_obj {J : Type u} (F : J CommMon) (j : J) :
Equations
@[instance]
@[instance]
@[instance]
def CommMon.limit_comm_monoid {J : Type u} (F : J CommMon) :
Equations
@[instance]

We show that the forgetful functor CommMon ⥤ Mon creates limits.

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

Equations
@[instance]
def CommMon.limit_cone {J : Type u} (F : J CommMon) :

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

Equations

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

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

def CommMon.limit_cone_is_limit {J : Type u} (F : J CommMon) :

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

Equations
@[instance]

The category of commutative monoids has all limits.

@[instance]
@[instance]

The forgetful functor from commutative monoids to monoids preserves all limits. (That is, the underlying monoid could have been computed instead as limits in the category of monoids.)

Equations
@[instance]

The forgetful functor from commutative monoids to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations