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

@[protected, instance]
Equations
@[protected, instance]
def Mon.monoid_obj {J : Type v} (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.

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

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

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

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

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

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

Equations
def Mon.has_limits.limit_cone {J : Type v} (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.)

Equations
def Mon.has_limits.limit_cone_is_limit {J : Type v} (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.)

Equations
@[protected, instance]

The category of monoids has all limits.

@[protected, instance]

The category of additive monoids has all limits.

@[protected, instance]
@[protected, instance]
@[protected, instance]

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.

Equations
@[protected, instance]

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.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def CommMon.comm_monoid_obj {J : Type v} (F : J CommMon) (j : J) :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def CommMon.limit_comm_monoid {J : Type v} (F : J CommMon) :
Equations
@[protected, 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
@[protected, instance]

We show that the forgetful functor AddCommMon ⥤ AddMon creates limits.

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

Equations
noncomputable def CommMon.limit_cone {J : Type v} (F : J CommMon) :

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

Equations
noncomputable def AddCommMon.limit_cone {J : Type v} (F : J AddCommMon) :

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

Equations
noncomputable def AddCommMon.limit_cone_is_limit {J : Type v} (F : J AddCommMon) :

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

Equations
noncomputable def CommMon.limit_cone_is_limit {J : Type v} (F : J CommMon) :

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

Equations
@[protected, instance]

The category of commutative monoids has all limits.

@[protected, instance]

The category of commutative monoids has all limits.

@[protected, instance]
@[protected, instance]
@[protected, instance]

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.

Equations
@[protected, instance]

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.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]

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.

Equations
@[protected, instance]

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.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations