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.

source
@[protected, instance]
def AddGroup.add_group_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ AddGroup) (j : J) :
add_group ((F ⋙ category_theory.forget AddGroup).obj j)
Equations
source
@[protected, instance]
def Group.group_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ Group) (j : J) :
group ((F ⋙ category_theory.forget Group).obj j)
Equations
source
def Group.sections_subgroup {J : Type v} [category_theory.small_category J] (F : J ⥤ Group) :
subgroup (Π (j : J), ↥(F.obj j))

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

Equations
source
def AddGroup.sections_add_subgroup {J : Type v} [category_theory.small_category J] (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.

Equations
source
@[protected, instance]
def AddGroup.limit_add_group {J : Type v} [category_theory.small_category J] (F : J ⥤ AddGroup) :
add_group (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddGroup)).X
Equations
source
@[protected, instance]
def Group.limit_group {J : Type v} [category_theory.small_category J] (F : J ⥤ Group) :
group (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Group)).X
Equations
source
@[protected, instance]
noncomputable def AddGroup.forget₂.creates_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ AddGroup) :
category_theory.creates_limit F (category_theory.forget₂ AddGroup AddMon)

We show that the forgetful functor AddGroup ⥤ AddMon 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
source
@[protected, instance]
noncomputable def Group.forget₂.creates_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ Group) :
category_theory.creates_limit F (category_theory.forget₂ Group Mon)

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
source
noncomputable def AddGroup.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ AddGroup) :
category_theory.limits.cone F

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

Equations
source
noncomputable def Group.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ Group) :
category_theory.limits.cone F

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

Equations
source
noncomputable def Group.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ Group) :
category_theory.limits.is_limit (Group.limit_cone F)

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

Equations
source
noncomputable def AddGroup.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ AddGroup) :
category_theory.limits.is_limit (AddGroup.limit_cone F)

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

Equations
source
@[protected, instance]
def AddGroup.has_limits_of_size  :
category_theory.limits.has_limits_of_size AddGroup

The category of additive groups has all limits.

source
@[protected, instance]
def Group.has_limits_of_size  :
category_theory.limits.has_limits_of_size Group

The category of groups has all limits.

source
@[protected, instance]
def AddGroup.has_limits  :
category_theory.limits.has_limits AddGroup
source
@[protected, instance]
def Group.has_limits  :
category_theory.limits.has_limits Group
source
@[protected, instance]
noncomputable def Group.forget₂_Mon_preserves_limits_of_size  :
category_theory.limits.preserves_limits_of_size (category_theory.forget₂ Group Mon)

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
source
@[protected, instance]
noncomputable def AddGroup.forget₂_AddMon_preserves_limits  :
category_theory.limits.preserves_limits_of_size (category_theory.forget₂ AddGroup AddMon)

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
source
@[protected, instance]
noncomputable def AddGroup.forget₂_Mon_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ AddGroup AddMon)
Equations
source
@[protected, instance]
noncomputable def Group.forget₂_Mon_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ Group Mon)
Equations
source
@[protected, instance]
noncomputable def AddGroup.forget_preserves_limits_of_size  :
category_theory.limits.preserves_limits_of_size (category_theory.forget AddGroup)

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
source
@[protected, instance]
noncomputable def Group.forget_preserves_limits_of_size  :
category_theory.limits.preserves_limits_of_size (category_theory.forget Group)

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
source
@[protected, instance]
noncomputable def AddGroup.forget_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget AddGroup)
Equations
source
@[protected, instance]
noncomputable def Group.forget_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget Group)
Equations
source
@[protected, instance]
def AddCommGroup.add_comm_group_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ AddCommGroup) (j : J) :
add_comm_group ((F ⋙ category_theory.forget AddCommGroup).obj j)
Equations
source
@[protected, instance]
def CommGroup.comm_group_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ CommGroup) (j : J) :
comm_group ((F ⋙ category_theory.forget CommGroup).obj j)
Equations
source
@[protected, instance]
def AddCommGroup.limit_add_comm_group {J : Type v} [category_theory.small_category J] (F : J ⥤ AddCommGroup) :
add_comm_group (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddCommGroup)).X
Equations
source
@[protected, instance]
def CommGroup.limit_comm_group {J : Type v} [category_theory.small_category J] (F : J ⥤ CommGroup) :
comm_group (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommGroup)).X
Equations
source
@[protected, instance]
noncomputable def CommGroup.forget₂.creates_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ CommGroup) :
category_theory.creates_limit F (category_theory.forget₂ CommGroup Group)

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
source
@[protected, instance]
noncomputable def AddCommGroup.forget₂.creates_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ AddCommGroup) :
category_theory.creates_limit F (category_theory.forget₂ AddCommGroup AddGroup)

We show that the forgetful functor AddCommGroup ⥤ AddGroup 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
source
noncomputable def CommGroup.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ CommGroup) :
category_theory.limits.cone F

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

Equations
source
noncomputable def AddCommGroup.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ AddCommGroup) :
category_theory.limits.cone F

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

Equations
source
noncomputable def AddCommGroup.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ AddCommGroup) :
category_theory.limits.is_limit (AddCommGroup.limit_cone F)

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

Equations
source
noncomputable def CommGroup.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ CommGroup) :
category_theory.limits.is_limit (CommGroup.limit_cone F)

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

Equations
source
@[protected, instance]
def AddCommGroup.has_limits_of_size  :
category_theory.limits.has_limits_of_size AddCommGroup

The category of additive commutative groups has all limits.

source
@[protected, instance]
def CommGroup.has_limits_of_size  :
category_theory.limits.has_limits_of_size CommGroup

The category of commutative groups has all limits.

source
@[protected, instance]
def CommGroup.has_limits  :
category_theory.limits.has_limits CommGroup
source
@[protected, instance]
def AddCommGroup.has_limits  :
category_theory.limits.has_limits AddCommGroup
source
@[protected, instance]
noncomputable def AddCommGroup.forget₂_AddGroup_preserves_limits  :
category_theory.limits.preserves_limits_of_size (category_theory.forget₂ AddCommGroup AddGroup)

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
source
@[protected, instance]
noncomputable def CommGroup.forget₂_Group_preserves_limits_of_size  :
category_theory.limits.preserves_limits_of_size (category_theory.forget₂ CommGroup Group)

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
source
@[protected, instance]
noncomputable def AddCommGroup.forget₂_Group_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ AddCommGroup AddGroup)
Equations
source
@[protected, instance]
noncomputable def CommGroup.forget₂_Group_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ CommGroup Group)
Equations
source
noncomputable def AddCommGroup.forget₂_AddCommMon_preserves_limits_aux {J : Type v} [category_theory.small_category J] (F : J ⥤ AddCommGroup) :
category_theory.limits.is_limit ((category_theory.forget₂ AddCommGroup AddCommMon).map_cone (AddCommGroup.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations
source
noncomputable def CommGroup.forget₂_CommMon_preserves_limits_aux {J : Type v} [category_theory.small_category J] (F : J ⥤ CommGroup) :
category_theory.limits.is_limit ((category_theory.forget₂ CommGroup CommMon).map_cone (CommGroup.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations
source
@[protected, instance]
noncomputable def CommGroup.forget₂_CommMon_preserves_limits_of_size  :
category_theory.limits.preserves_limits_of_size (category_theory.forget₂ CommGroup CommMon)

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
source
@[protected, instance]
noncomputable def AddCommGroup.forget₂_AddCommMon_preserves_limits  :
category_theory.limits.preserves_limits_of_size (category_theory.forget₂ AddCommGroup AddCommMon)

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
source
@[protected, instance]
noncomputable def AddCommGroup.forget_preserves_limits  :
category_theory.limits.preserves_limits_of_size (category_theory.forget AddCommGroup)

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
source
@[protected, instance]
noncomputable def CommGroup.forget_preserves_limits_of_size  :
category_theory.limits.preserves_limits_of_size (category_theory.forget CommGroup)

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
source
noncomputable def AddCommGroup.kernel_iso_ker {G H : AddCommGroup} (f : G ⟶ H) :
category_theory.limits.kernel f ≅ AddCommGroup.of ↥(add_monoid_hom.ker f)

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

Equations
source
@[simp]
theorem AddCommGroup.kernel_iso_ker_hom_comp_subtype {G H : AddCommGroup} (f : G ⟶ H) :
(AddCommGroup.kernel_iso_ker f).hom ≫ (add_monoid_hom.ker f).subtype = category_theory.limits.kernel.ι f
source
@[simp]
theorem AddCommGroup.kernel_iso_ker_inv_comp_ι {G H : AddCommGroup} (f : G ⟶ H) :
(AddCommGroup.kernel_iso_ker f).inv ≫ category_theory.limits.kernel.ι f = (add_monoid_hom.ker f).subtype
source
noncomputable def AddCommGroup.kernel_iso_ker_over {G H : AddCommGroup} (f : G ⟶ H) :
category_theory.over.mk (category_theory.limits.kernel.ι f) ≅ category_theory.over.mk (add_monoid_hom.ker f).subtype

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

Equations
source
@[simp]
theorem AddCommGroup.kernel_iso_ker_over_inv_left_apply {G H : AddCommGroup} (f : G ⟶ H) (ᾰ : ↥((category_theory.limits.kernel_fork.of_ι (add_monoid_hom.ker f).subtype _).X)) :
⇑((AddCommGroup.kernel_iso_ker_over f).inv.left) ᾰ = ⇑(category_theory.limits.limit.lift (category_theory.limits.parallel_pair f 0) (category_theory.limits.kernel_fork.of_ι (add_monoid_hom.ker f).subtype _)) ᾰ
source
@[simp]
theorem AddCommGroup.kernel_iso_ker_over_hom_right_down_down {G H : AddCommGroup} (f : G ⟶ H) :
_ = _
source
@[simp]
theorem AddCommGroup.kernel_iso_ker_over_inv_right_down_down {G H : AddCommGroup} (f : G ⟶ H) :
_ = _
source
@[simp]
theorem AddCommGroup.kernel_iso_ker_over_hom_left_apply_coe {G H : AddCommGroup} (f : G ⟶ H) (g : ↥(category_theory.limits.kernel f)) :
↑(⇑((AddCommGroup.kernel_iso_ker_over f).hom.left) g) = ⇑(category_theory.limits.kernel.ι f) g