# Documentation

Mathlib.Algebra.Category.GroupCat.FilteredColimits

# 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 ⥤ GroupCat. We show that the colimit of F ⋙ forget₂ GroupCat MonCat (in MonCat) carries the structure of a group, thereby showing that the forgetful functor forget₂ GroupCat MonCat preserves filtered colimits. In particular, this implies that forget GroupCat preserves filtered colimits. Similarly for AddGroupCat, CommGroupCat and AddCommGroupCat.

noncomputable abbrev AddGroupCat.FilteredColimits.G {J : Type v} :

The colimit of F ⋙ forget₂ AddGroupCat AddMonCat in the category AddMonCat. In the following, we will show that this has the structure of an additive group.

Instances For
@[inline, reducible]
noncomputable abbrev GroupCat.FilteredColimits.G {J : Type v} (F : ) :

The colimit of F ⋙ forget₂ GroupCat MonCat in the category MonCat. In the following, we will show that this has the structure of a group.

Instances For
abbrev AddGroupCat.FilteredColimits.G.mk {J : Type v} :
(j : J) × ↑(F.obj j)

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

Instances For
@[inline, reducible]
abbrev GroupCat.FilteredColimits.G.mk {J : Type v} (F : ) :
(j : J) × ↑(F.obj j)

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

Instances For
theorem AddGroupCat.FilteredColimits.G.mk_eq {J : Type v} (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (h : k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd) :
theorem GroupCat.FilteredColimits.G.mk_eq {J : Type v} (F : ) (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (h : k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd) :
def AddGroupCat.FilteredColimits.colimitNegAux {J : Type v} (x : (j : J) × ↑(F.obj j)) :

The "unlifted" version of negation in the colimit.

Instances For
def GroupCat.FilteredColimits.colimitInvAux {J : Type v} (F : ) (x : (j : J) × ↑(F.obj j)) :

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

Instances For
theorem AddGroupCat.FilteredColimits.colimitNegAux_eq_of_rel {J : Type v} (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) :
theorem GroupCat.FilteredColimits.colimitInvAux_eq_of_rel {J : Type v} (F : ) (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) :

Negation in the colimit. See also colimitNegAux.

theorem AddGroupCat.FilteredColimits.colimitNeg.proof_1 {J : Type u_1} (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) :
instance GroupCat.FilteredColimits.colimitInv {J : Type v} (F : ) :

Taking inverses in the colimit. See also colimitInvAux.

@[simp]
theorem AddGroupCat.FilteredColimits.colimit_neg_mk_eq {J : Type v} (x : (j : J) × ↑(F.obj j)) :
= AddGroupCat.FilteredColimits.G.mk F { fst := x.fst, snd := -x.snd }
@[simp]
theorem GroupCat.FilteredColimits.colimit_inv_mk_eq {J : Type v} (F : ) (x : (j : J) × ↑(F.obj j)) :
= GroupCat.FilteredColimits.G.mk F { fst := x.fst, snd := x.snd⁻¹ }
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x
∀ (a : ), zsmulRec 0 a = zsmulRec 0 a
∀ (a b : ), a - b = a - b
∀ (n : ) (a : ), zsmulRec () a = zsmulRec () a
∀ (n : ) (a : ), zsmulRec () a = zsmulRec () a
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
noncomputable instance GroupCat.FilteredColimits.colimitGroup {J : Type v} (F : ) :

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

Instances For
noncomputable def GroupCat.FilteredColimits.colimit {J : Type v} (F : ) :

The bundled group giving the filtered colimit of a diagram.

Instances For

The cocone over the proposed colimit additive group.

Instances For
theorem AddGroupCat.FilteredColimits.colimitCocone.proof_1 {J : Type u_1} ⦃X : J ⦃Y : J (f : X Y) :
CategoryTheory.CategoryStruct.comp () (.app Y) = CategoryTheory.CategoryStruct.comp (.app X) ((().obj ().pt).map f)
noncomputable def GroupCat.FilteredColimits.colimitCocone {J : Type v} (F : ) :

The cocone over the proposed colimit group.

Instances For
theorem AddGroupCat.FilteredColimits.colimitCoconeIsColimit.proof_2 {J : Type u_1} (t : ) :
∀ (x : t.pt), (∀ (j : J), = t.app j) → x = (fun t => AddMonCat.FilteredColimits.colimitDesc () (().mapCocone t)) t

The proposed colimit cocone is a colimit in AddGroup.

Instances For

The proposed colimit cocone is a colimit in GroupCat.

Instances For

The colimit of F ⋙ forget₂ AddCommGroupCat AddGroupCat in the category AddGroupCat. In the following, we will show that this has the structure of a commutative additive group.

Instances For
@[inline, reducible]
noncomputable abbrev CommGroupCat.FilteredColimits.G {J : Type v} :

The colimit of F ⋙ forget₂ CommGroupCat GroupCat in the category GroupCat. In the following, we will show that this has the structure of a commutative group.

Instances For

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

Instances For

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

Instances For

The cocone over the proposed colimit additive commutative group.

Instances For
theorem AddCommGroupCat.FilteredColimits.colimitCocone.proof_1 {J : Type u_1} ⦃X : J ⦃Y : J (f : X Y) :

The cocone over the proposed colimit commutative group.

Instances For
theorem AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit.proof_2 {J : Type u_1} (t : ) :
∀ (x : ), (∀ (j : J), = t.app j) → x = (fun t => CategoryTheory.Limits.IsColimit.desc () (().mapCocone t)) t

The proposed colimit cocone is a colimit in AddCommGroup.

Instances For

The proposed colimit cocone is a colimit in CommGroupCat.

Instances For