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.

@[protected, instance]
Equations
@[protected, instance]
def Mon.monoid_obj {J : Type v} [category_theory.small_category J] (F : J Mon) (j : J) :
Equations
def AddMon.sections_add_submonoid {J : Type v} [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.

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

The category of monoids has all limits.

@[protected, instance]

The category of additive monoids has all limits.

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

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
@[protected, instance]

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

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

Equations
@[protected, instance]

The category of commutative monoids has all limits.

@[protected, instance]

The category of commutative monoids has all limits.

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

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