mathlibdocumentation

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.

def Group.filtered_colimits.G {J : Type v} (F : J 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.

def Group.filtered_colimits.G.mk {J : Type v} (F : J Group) :
(Σ (j : J), (F.obj j))

The canonical projection into the colimit, as a quotient type.

(Σ (j : J), (F.obj j))

The canonical projection into the colimit, as a quotient type.

theorem AddGroup.filtered_colimits.G.mk_eq {J : Type v} (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} (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) :
def Group.filtered_colimits.colimit_inv_aux {J : Type v} (F : J Group) (x : Σ (j : J), (F.obj j)) :

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

Equations
def AddGroup.filtered_colimits.colimit_neg_aux {J : Type v} (F : J AddGroup) (x : Σ (j : J), (F.obj j)) :

The "unlifted" version of negation in the colimit.

Equations
theorem AddGroup.filtered_colimits.colimit_neg_aux_eq_of_rel {J : Type v} (F : J AddGroup) (x y : Σ (j : J), (F.obj j))  :
theorem Group.filtered_colimits.colimit_inv_aux_eq_of_rel {J : Type v} (F : J Group) (x y : Σ (j : J), (F.obj j))  :
@[instance]

Negation in the colimit. See also colimit_neg_aux.

Equations
• = {neg := λ (x : , quot.lift _ x}
@[instance]
def Group.filtered_colimits.colimit_has_inv {J : Type v} (F : J Group) :

Taking inverses in the colimit. See also colimit_inv_aux.

Equations
• = {inv := λ (x : , quot.lift _ x}
@[simp]
theorem AddGroup.filtered_colimits.colimit_neg_mk_eq {J : Type v} (F : J AddGroup) (x : Σ (j : J), (F.obj j)) :
@[simp]
theorem Group.filtered_colimits.colimit_inv_mk_eq {J : Type v} (F : J Group) (x : Σ (j : J), (F.obj j)) :
= x.fst, (x.snd)⁻¹
@[instance]
def Group.filtered_colimits.colimit_group {J : Type v} (F : J Group) :
Equations
@[instance]
Equations
def Group.filtered_colimits.colimit {J : Type v} (F : J Group) :

The bundled group giving the filtered colimit of a diagram.

Equations

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

Equations
def Group.filtered_colimits.colimit_cocone {J : Type v} (F : J Group) :

The cocone over the proposed colimit group.

Equations

The cocone over the proposed colimit additive group.

Equations

The proposed colimit cocone is a colimit in Group.

Equations

The proposed colimit cocone is a colimit in AddGroup.

Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
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.

def CommGroup.filtered_colimits.G {J : Type v} (F : J CommGroup) :

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.

@[instance]
Equations
@[instance]
Equations

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

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

The proposed colimit cocone is a colimit in CommGroup.

Equations
@[instance]
Equations
@[instance]
Equations