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
- 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
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.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.limit (F ⋙ category_theory.forget Group)) (Group.limit_group F), π := {app := Mon.limit_π_monoid_hom (F ⋙ category_theory.forget₂ Group Mon), naturality' := _}}, valid_lift := (category_theory.limits.limit.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) (category_theory.limits.limit.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' := _}) _})
The category of groups has all limits.
Equations
- Group.has_limits = {has_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ Group), category_theory.has_limit_of_created F (category_theory.forget₂ Group Mon)}}
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.small_category J), {preserves_limit := λ (F : J ⥤ Group), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ Group Mon)}}
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.small_category J), {preserves_limit := λ (F : J ⥤ Group), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget Group))}}
Equations
- CommGroup.comm_group_obj F j = id (F.obj j).comm_group_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
- CommGroup.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.limit (F ⋙ category_theory.forget CommGroup)) (CommGroup.limit_comm_group F), π := {app := Mon.limit_π_monoid_hom (F ⋙ category_theory.forget₂ CommGroup Group ⋙ category_theory.forget₂ Group Mon), naturality' := _}}, valid_lift := (category_theory.limits.limit.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) (category_theory.limits.limit.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' := _}) _})
The category of commutative groups has all limits.
Equations
- CommGroup.has_limits = {has_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ CommGroup), category_theory.has_limit_of_created F (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
- CommGroup.forget₂_Group_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_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.
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.small_category J), {preserves_limit := λ (F : J ⥤ CommGroup), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.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.small_category J), {preserves_limit := λ (F : J ⥤ CommGroup), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget CommGroup))}}
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.
Equations
- AddCommGroup.kernel_iso_ker_over f = {hom := category_theory.over.hom_mk (AddCommGroup.kernel_iso_ker f).hom _, inv := category_theory.over.hom_mk (AddCommGroup.kernel_iso_ker f).inv _, hom_inv_id' := _, inv_hom_id' := _}