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.
Equations
- AddGroup.add_group_obj F j = id (F.obj j).add_group
Equations
- Group.group_obj F j = id (F.obj j).group
The flat sections of a functor into Group
form a subgroup of all sections.
The flat sections of a functor into AddGroup
form an additive subgroup of all sections.
Equations
Equations
Equations
- AddGroup.category_theory.forget₂.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (F ⋙ category_theory.forget₂ AddGroup AddMon)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := AddGroup.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddGroup)).X (AddGroup.limit_add_group F), π := {app := AddMon.limit_π_add_monoid_hom (F ⋙ category_theory.forget₂ AddGroup AddMon), naturality' := _}}, valid_lift := (AddMon.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ AddGroup AddMon)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ AddGroup AddMon) (AddMon.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ AddGroup AddMon)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget AddMon).map_cone ((category_theory.forget₂ AddGroup AddMon).map_cone s)).X), ⟨λ (j : J), ((category_theory.forget AddMon).map_cone ((category_theory.forget₂ AddGroup AddMon).map_cone s)).π.app j v, _⟩, map_zero' := _, map_add' := _}) _})
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
- Group.category_theory.forget₂.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (F ⋙ category_theory.forget₂ Group Mon)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := Group.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Group)).X (Group.limit_group F), π := {app := Mon.limit_π_monoid_hom (F ⋙ category_theory.forget₂ Group Mon), naturality' := _}}, valid_lift := (Mon.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ Group Mon)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ Group Mon) (Mon.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ Group Mon)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget Mon).map_cone ((category_theory.forget₂ Group Mon).map_cone s)).X), ⟨λ (j : J), ((category_theory.forget Mon).map_cone ((category_theory.forget₂ Group Mon).map_cone s)).π.app j v, _⟩, map_one' := _, map_mul' := _}) _})
A choice of limit cone for a functor into Group
.
(Generally, you'll just want to use limit F
.)
A choice of limit cone for a functor into Group
.
(Generally, you'll just want to use limit F
.)
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
The category of groups has all limits.
Equations
- AddGroup.forget₂_AddMon_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ AddGroup), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ AddGroup AddMon)}}
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
- Group.forget₂_Mon_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Group), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ Group Mon)}}
Equations
- AddGroup.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ AddGroup), category_theory.limits.comp_preserves_limit (category_theory.forget₂ AddGroup AddMon) (category_theory.forget AddMon)}}
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
- Group.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Group), category_theory.limits.comp_preserves_limit (category_theory.forget₂ Group Mon) (category_theory.forget Mon)}}
Equations
Equations
- CommGroup.comm_group_obj F j = id (F.obj j).comm_group_instance
Equations
- AddCommGroup.category_theory.forget₂.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (F ⋙ category_theory.forget₂ AddCommGroup AddGroup)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := AddCommGroup.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddCommGroup)).X (AddCommGroup.limit_add_comm_group F), π := {app := AddMon.limit_π_add_monoid_hom (F ⋙ category_theory.forget₂ AddCommGroup AddGroup ⋙ category_theory.forget₂ AddGroup AddMon), naturality' := _}}, valid_lift := (AddGroup.limit_cone_is_limit (F ⋙ category_theory.forget₂ AddCommGroup AddGroup)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ AddCommGroup AddGroup ⋙ category_theory.forget₂ AddGroup AddMon) (AddMon.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ AddCommGroup AddGroup ⋙ category_theory.forget₂ AddGroup AddMon)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget AddMon).map_cone ((category_theory.forget₂ AddCommGroup AddGroup ⋙ category_theory.forget₂ AddGroup AddMon).map_cone s)).X), ⟨λ (j : J), ((category_theory.forget AddMon).map_cone ((category_theory.forget₂ AddCommGroup AddGroup ⋙ category_theory.forget₂ AddGroup AddMon).map_cone s)).π.app j v, _⟩, map_zero' := _, map_add' := _}) _})
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
- CommGroup.category_theory.forget₂.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (F ⋙ category_theory.forget₂ CommGroup Group)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := CommGroup.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommGroup)).X (CommGroup.limit_comm_group F), π := {app := Mon.limit_π_monoid_hom (F ⋙ category_theory.forget₂ CommGroup Group ⋙ category_theory.forget₂ Group Mon), naturality' := _}}, valid_lift := (Group.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommGroup Group)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ CommGroup Group ⋙ category_theory.forget₂ Group Mon) (Mon.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommGroup Group ⋙ category_theory.forget₂ Group Mon)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget Mon).map_cone ((category_theory.forget₂ CommGroup Group ⋙ category_theory.forget₂ Group Mon).map_cone s)).X), ⟨λ (j : J), ((category_theory.forget Mon).map_cone ((category_theory.forget₂ CommGroup Group ⋙ category_theory.forget₂ Group Mon).map_cone s)).π.app j v, _⟩, map_one' := _, map_mul' := _}) _})
A choice of limit cone for a functor into CommGroup
.
(Generally, you'll just want to use limit F
.)
A choice of limit cone for a functor into CommGroup
.
(Generally, you'll just want to use limit F
.)
The chosen cone is a limit cone.
(Generally, you'll just wantto use limit.cone F
.)
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
The category of commutative groups has all limits.
Equations
- AddCommGroup.forget₂_AddGroup_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ AddCommGroup), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ AddCommGroup AddGroup)}}
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
- CommGroup.forget₂_Group_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommGroup), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ CommGroup Group)}}
An auxiliary declaration to speed up typechecking.
An auxiliary declaration to speed up typechecking.
Equations
- AddCommGroup.forget₂_AddCommMon_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ AddCommGroup), category_theory.limits.preserves_limit_of_preserves_limit_cone (AddCommGroup.limit_cone_is_limit F) (AddCommGroup.forget₂_AddCommMon_preserves_limits_aux F)}}
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
- CommGroup.forget₂_CommMon_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommGroup), category_theory.limits.preserves_limit_of_preserves_limit_cone (CommGroup.limit_cone_is_limit F) (CommGroup.forget₂_CommMon_preserves_limits_aux F)}}
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
- CommGroup.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommGroup), category_theory.limits.comp_preserves_limit (category_theory.forget₂ CommGroup Group) (category_theory.forget Group)}}
Equations
- AddCommGroup.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ AddCommGroup), category_theory.limits.comp_preserves_limit (category_theory.forget₂ AddCommGroup AddGroup) (category_theory.forget AddGroup)}}
The categorical kernel of a morphism in AddCommGroup
agrees with the usual group-theoretical kernel.
Equations
- AddCommGroup.kernel_iso_ker f = {hom := {to_fun := λ (g : ↥(category_theory.limits.kernel f)), ⟨⇑(category_theory.limits.kernel.ι f) g, _⟩, map_zero' := _, map_add' := _}, inv := category_theory.limits.kernel.lift f (add_monoid_hom.ker f).subtype _, hom_inv_id' := _, inv_hom_id' := _}
The categorical kernel inclusion for f : G ⟶ H
, as an object over G
,
agrees with the subtype
map.