The forgetful functor from (commutative) (additive) groups preserves filtered colimits. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend to preserve filtered colimits.
In this file, we start with a small filtered category J
and a functor F : J ⥤ Group
.
We show that the colimit of F ⋙ forget₂ Group Mon
(in Mon
) carries the structure of a group,
thereby showing that the forgetful functor forget₂ Group Mon
preserves filtered colimits. In
particular, this implies that forget Group
preserves filtered colimits. Similarly for AddGroup
,
CommGroup
and AddCommGroup
.
The colimit of F ⋙ forget₂ AddGroup AddMon
in the category AddMon
.
In the following, we will show that this has the structure of an additive group.
The colimit of F ⋙ forget₂ Group Mon
in the category Mon
.
In the following, we will show that this has the structure of a group.
The canonical projection into the colimit, as a quotient type.
The canonical projection into the colimit, as a quotient type.
The "unlifted" version of taking inverses in the colimit.
Equations
The "unlifted" version of negation in the colimit.
Equations
Negation in the colimit. See also colimit_neg_aux
.
Equations
- AddGroup.filtered_colimits.colimit_has_neg F = {neg := λ (x : ↥(AddGroup.filtered_colimits.G F)), quot.lift (AddGroup.filtered_colimits.colimit_neg_aux F) _ x}
Taking inverses in the colimit. See also colimit_inv_aux
.
Equations
- Group.filtered_colimits.colimit_has_inv F = {inv := λ (x : ↥(Group.filtered_colimits.G F)), quot.lift (Group.filtered_colimits.colimit_inv_aux F) _ x}
Equations
- Group.filtered_colimits.colimit_group F = {mul := monoid.mul (Group.filtered_colimits.G F).monoid, mul_assoc := _, one := monoid.one (Group.filtered_colimits.G F).monoid, one_mul := _, mul_one := _, npow := monoid.npow (Group.filtered_colimits.G F).monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv (Group.filtered_colimits.colimit_has_inv F), div := div_inv_monoid.div._default monoid.mul _ monoid.one _ _ monoid.npow _ _ has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid.mul _ monoid.one _ _ monoid.npow _ _ has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
Equations
- AddGroup.filtered_colimits.colimit_add_group F = {add := add_monoid.add (AddGroup.filtered_colimits.G F).add_monoid, add_assoc := _, zero := add_monoid.zero (AddGroup.filtered_colimits.G F).add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (AddGroup.filtered_colimits.G F).add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (AddGroup.filtered_colimits.colimit_has_neg F), sub := sub_neg_monoid.sub._default add_monoid.add _ add_monoid.zero _ _ add_monoid.nsmul _ _ has_neg.neg, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default add_monoid.add _ add_monoid.zero _ _ add_monoid.nsmul _ _ has_neg.neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
The bundled group giving the filtered colimit of a diagram.
Equations
Instances for ↥Group.filtered_colimits.colimit
The bundled additive group giving the filtered colimit of a diagram.
Equations
Instances for ↥AddGroup.filtered_colimits.colimit
The cocone over the proposed colimit group.
Equations
- Group.filtered_colimits.colimit_cocone F = {X := Group.filtered_colimits.colimit F, ι := {app := (Mon.filtered_colimits.colimit_cocone (F ⋙ category_theory.forget₂ Group Mon)).ι.app, naturality' := _}}
The cocone over the proposed colimit additive group.
Equations
The proposed colimit cocone is a colimit in Group
.
Equations
- Group.filtered_colimits.colimit_cocone_is_colimit F = {desc := λ (t : category_theory.limits.cocone F), Mon.filtered_colimits.colimit_desc (F ⋙ category_theory.forget₂ Group Mon) ((category_theory.forget₂ Group Mon).map_cocone t), fac' := _, uniq' := _}
The proposed colimit cocone is a colimit in AddGroup
.
Equations
Equations
- AddGroup.filtered_colimits.forget₂_AddMon_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ AddGroup), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (AddGroup.filtered_colimits.colimit_cocone_is_colimit F) (AddMon.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ AddGroup AddMon))}}
Equations
- Group.filtered_colimits.forget₂_Mon_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ Group), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (Group.filtered_colimits.colimit_cocone_is_colimit F) (Mon.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ Group Mon))}}
The colimit of F ⋙ forget₂ AddCommGroup AddGroup
in the category AddGroup
.
In the following, we will show that this has the structure of a commutative additive group.
The colimit of F ⋙ forget₂ CommGroup Group
in the category Group
.
In the following, we will show that this has the structure of a commutative group.
Equations
- CommGroup.filtered_colimits.colimit_comm_group F = {mul := group.mul (CommGroup.filtered_colimits.G F).group, mul_assoc := _, one := group.one (CommGroup.filtered_colimits.G F).group, one_mul := _, mul_one := _, npow := group.npow (CommGroup.filtered_colimits.G F).group, npow_zero' := _, npow_succ' := _, inv := group.inv (CommGroup.filtered_colimits.G F).group, div := group.div (CommGroup.filtered_colimits.G F).group, div_eq_mul_inv := _, zpow := group.zpow (CommGroup.filtered_colimits.G F).group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
Equations
- AddCommGroup.filtered_colimits.colimit_add_comm_group F = {add := add_group.add (AddCommGroup.filtered_colimits.G F).add_group, add_assoc := _, zero := add_group.zero (AddCommGroup.filtered_colimits.G F).add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul (AddCommGroup.filtered_colimits.G F).add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (AddCommGroup.filtered_colimits.G F).add_group, sub := add_group.sub (AddCommGroup.filtered_colimits.G F).add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul (AddCommGroup.filtered_colimits.G F).add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
The bundled commutative group giving the filtered colimit of a diagram.
The bundled additive commutative group giving the filtered colimit of a diagram.
Equations
Instances for ↥AddCommGroup.filtered_colimits.colimit
The cocone over the proposed colimit commutative group.
Equations
The cocone over the proposed colimit additive commutative group.
Equations
The proposed colimit cocone is a colimit in AddCommGroup
.
Equations
- AddCommGroup.filtered_colimits.colimit_cocone_is_colimit F = {desc := λ (t : category_theory.limits.cocone F), (AddGroup.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ AddCommGroup AddGroup)).desc ((category_theory.forget₂ AddCommGroup AddGroup).map_cocone t), fac' := _, uniq' := _}
The proposed colimit cocone is a colimit in CommGroup
.
Equations
Equations
- CommGroup.filtered_colimits.forget₂_Group_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ CommGroup), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (CommGroup.filtered_colimits.colimit_cocone_is_colimit F) (Group.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ CommGroup Group))}}
Equations
- AddCommGroup.filtered_colimits.forget₂_AddGroup_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ AddCommGroup), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (AddCommGroup.filtered_colimits.colimit_cocone_is_colimit F) (AddGroup.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ AddCommGroup AddGroup))}}