mathlib3 documentation

algebra.category.Group.limits

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

The flat sections of a functor into Group form a subgroup of all sections.

Equations

The flat sections of a functor into AddGroup form an additive subgroup of all sections.

Equations
@[protected, instance]

We show that the forgetful functor AddGroupAddMon creates limits.

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

Equations

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

Equations

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

Equations
@[protected, instance]

The category of additive groups has all limits.

@[protected, instance]

The category of groups has all limits.

@[protected, instance]

The forgetful functor from groups to monoids preserves all limits.

This means the underlying monoid of a limit can be computed as a limit in the category of monoids.

Equations
@[protected, instance]

The forgetful functor from additive groups to additive monoids preserves all limits.

This means the underlying additive monoid of a limit can be computed as a limit in the category of additive monoids.

Equations
@[protected, instance]

The forgetful functor from additive groups 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 groups 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]

We show that the forgetful functor CommGroupGroup creates limits.

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

Equations
@[protected, instance]

We show that the forgetful functor AddCommGroupAddGroup creates limits.

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

Equations

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

Equations

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

Equations
@[protected, instance]

The category of additive commutative groups has all limits.

@[protected, instance]

The category of commutative groups has all limits.

@[protected, instance]

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

Equations
@[protected, instance]

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

Equations
@[protected, instance]

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

Equations
@[protected, instance]

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

Equations
@[protected, instance]

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

Equations
@[protected, instance]

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

Equations

The categorical kernel of a morphism in AddCommGroup agrees with the usual group-theoretical kernel.

Equations

The categorical kernel inclusion for f : G ⟶ H, as an object over G, agrees with the subtype map.

Equations