mathlib documentation

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]
def Mon.monoid_obj {J : Type u} [category_theory.small_category J] (F : J Mon) (j : J) :
Equations
def AddMon.sections_add_submonoid {J : Type u} [category_theory.small_category J] (F : J AddMon) :
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} [category_theory.small_category J] (F : J Mon) :
submonoid (Π (j : J), (F.obj j))

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

Equations

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

Equations

(Internal use only; use the limits API.)

@[instance]

The category of monoids has all limits.

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

We show that the forgetful functor CommMonMon 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

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

@[instance]

The category of commutative monoids has all limits.

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