mathlibdocumentation

algebra.category.Group.limits

The category of (commutative) (additive) groups 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 AddGroup.add_group_obj {J : Type u} (F : J AddGroup) (j : J) :

@[instance]
def Group.group_obj {J : Type u} (F : J Group) (j : J) :

Equations
def Group.sections_subgroup {J : Type u} (F : J Group) :
subgroup (Π (j : J), (F.obj j))

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

Equations
def AddGroup.sections_add_subgroup {J : Type u} (F : J AddGroup) :
add_subgroup (Π (j : J), (F.obj j))

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

@[instance]
def AddGroup.limit_add_group {J : Type u} (F : J AddGroup) :

@[instance]
def Group.limit_group {J : Type u} (F : J Group) :

Equations
@[instance]

@[instance]

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

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

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

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

def Group.limit_cone {J : Type u} (F : J Group) :

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

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

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

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

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

@[instance]

@[instance]

The category of groups has all limits.

@[instance]

The forgetful functor from groups 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 groups 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 AddCommGroup.add_comm_group_obj {J : Type u} (F : J AddCommGroup) (j : J) :

@[instance]
def CommGroup.comm_group_obj {J : Type u} (F : J CommGroup) (j : J) :

Equations
@[instance]

@[instance]
def CommGroup.limit_comm_group {J : Type u} (F : J CommGroup) :

Equations
@[instance]

@[instance]

We show that the forgetful functor CommGroup ⥤ Group 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
def CommGroup.limit_cone {J : Type u} (F : J CommGroup) :

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

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

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

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

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

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

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

Equations
@[instance]

The category of commutative groups has all limits.

@[instance]

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

An auxiliary declaration to speed up typechecking.

An auxiliary declaration to speed up typechecking.

Equations
@[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
@[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
def AddCommGroup.kernel_iso_ker {G H : AddCommGroup} (f : G H) :

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

Equations
@[simp]

@[simp]

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

Equations