mathlib documentation

algebra.category.Group.filtered_colimits

The forgetful functor from (commutative) (additive) groups preserves filtered colimits. #

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.

theorem AddGroup.filtered_colimits.G.mk_eq {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J AddGroup) (x y : Σ (j : J), (F.obj j)) (h : ∃ (k : J) (f : x.fst k) (g : y.fst k), (F.map f) x.snd = (F.map g) y.snd) :
theorem Group.filtered_colimits.G.mk_eq {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J Group) (x y : Σ (j : J), (F.obj j)) (h : ∃ (k : J) (f : x.fst k) (g : y.fst k), (F.map f) x.snd = (F.map g) y.snd) :

The "unlifted" version of taking inverses in the colimit.

Equations
@[instance]

Taking inverses in the colimit. See also colimit_inv_aux.

Equations

The bundled group giving the filtered colimit of a diagram.

Equations

The bundled additive group giving the filtered colimit of a diagram.

Equations

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.

The bundled commutative group giving the filtered colimit of a diagram.

Equations

The bundled additive commutative group giving the filtered colimit of a diagram.

Equations