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

@[reducible, inline]

noncomputable abbrev GrpCat.FilteredColimits.G {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) : MonCat

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

Equations

• GrpCat.FilteredColimits.G F = MonCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ GrpCat MonCat))

@[reducible, inline]

noncomputable abbrev AddGrpCat.FilteredColimits.G {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) : AddMonCat

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

Equations

• AddGrpCat.FilteredColimits.G F = AddMonCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat))

@[reducible, inline]

abbrev GrpCat.FilteredColimits.G.mk {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) : (j : J) × ↑(F.obj j) → ↑(G F)

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

Equations

• GrpCat.FilteredColimits.G.mk F x = (F.comp (CategoryTheory.forget GrpCat)).ιColimitType x.fst x.snd

@[reducible, inline]

abbrev AddGrpCat.FilteredColimits.G.mk {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) : (j : J) × ↑(F.obj j) → ↑(G F)

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

Equations

• AddGrpCat.FilteredColimits.G.mk F x = (F.comp (CategoryTheory.forget AddGrpCat)).ιColimitType x.fst x.snd

theorem GrpCat.FilteredColimits.G.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) (x y : (j : J) × ↑(F.obj j)) (h : ∃ (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k), (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd) : mk F x = mk F y

theorem AddGrpCat.FilteredColimits.G.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) (x y : (j : J) × ↑(F.obj j)) (h : ∃ (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k), (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd) : mk F x = mk F y

theorem GrpCat.FilteredColimits.colimit_one_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) (j : J) : 1 = G.mk F ⟨j, 1⟩

theorem AddGrpCat.FilteredColimits.colimit_zero_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) (j : J) : 0 = G.mk F ⟨j, 0⟩

theorem GrpCat.FilteredColimits.colimit_mul_mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) (x y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k) : G.mk F x * G.mk F y = G.mk F ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd * (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩

theorem AddGrpCat.FilteredColimits.colimit_add_mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) (x y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k) : G.mk F x + G.mk F y = G.mk F ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd + (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩

theorem GrpCat.FilteredColimits.colimit_mul_mk_eq' {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) {j : J} (x y : ↑(F.obj j)) : G.mk F ⟨j, x⟩ * G.mk F ⟨j, y⟩ = G.mk F ⟨j, x * y⟩

theorem AddGrpCat.FilteredColimits.colimit_add_mk_eq' {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) {j : J} (x y : ↑(F.obj j)) : G.mk F ⟨j, x⟩ + G.mk F ⟨j, y⟩ = G.mk F ⟨j, x + y⟩

def GrpCat.FilteredColimits.colimitInvAux {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) (x : (j : J) × ↑(F.obj j)) : ↑(G F)

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

Equations

• GrpCat.FilteredColimits.colimitInvAux F x = GrpCat.FilteredColimits.G.mk F ⟨x.fst, x.snd⁻¹⟩

def AddGrpCat.FilteredColimits.colimitNegAux {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) (x : (j : J) × ↑(F.obj j)) : ↑(G F)

The "unlifted" version of negation in the colimit.

Equations

• AddGrpCat.FilteredColimits.colimitNegAux F x = AddGrpCat.FilteredColimits.G.mk F ⟨x.fst, -x.snd⟩

theorem GrpCat.FilteredColimits.colimitInvAux_eq_of_rel {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) (x y : (j : J) × ↑(F.obj j)) (h : CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget GrpCat)) x y) : colimitInvAux F x = colimitInvAux F y

theorem AddGrpCat.FilteredColimits.colimitNegAux_eq_of_rel {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) (x y : (j : J) × ↑(F.obj j)) (h : CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget AddGrpCat)) x y) : colimitNegAux F x = colimitNegAux F y

@[implicit_reducible]

instance GrpCat.FilteredColimits.colimitInv {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) : Inv ↑(G F)

Taking inverses in the colimit. See also colimitInvAux.

Equations

• GrpCat.FilteredColimits.colimitInv F = { inv := fun (x : ↑(GrpCat.FilteredColimits.G F)) => Quot.lift (GrpCat.FilteredColimits.colimitInvAux F) ⋯ x }

@[implicit_reducible]

instance AddGrpCat.FilteredColimits.colimitNeg {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) : Neg ↑(G F)

Negation in the colimit. See also colimitNegAux.

Equations

• AddGrpCat.FilteredColimits.colimitNeg F = { neg := fun (x : ↑(AddGrpCat.FilteredColimits.G F)) => Quot.lift (AddGrpCat.FilteredColimits.colimitNegAux F) ⋯ x }

@[simp]

theorem GrpCat.FilteredColimits.colimit_inv_mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) (x : (j : J) × ↑(F.obj j)) : (G.mk F x)⁻¹ = G.mk F ⟨x.fst, x.snd⁻¹⟩

@[simp]

theorem AddGrpCat.FilteredColimits.colimit_neg_mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) (x : (j : J) × ↑(F.obj j)) : -G.mk F x = G.mk F ⟨x.fst, -x.snd⟩

@[implicit_reducible]

noncomputable instance GrpCat.FilteredColimits.colimitGroup {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) : Group ↑(G F)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance AddGrpCat.FilteredColimits.colimitAddGroup {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) : AddGroup ↑(G F)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GrpCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) : GrpCat

The bundled group giving the filtered colimit of a diagram.

Equations

• GrpCat.FilteredColimits.colimit F = GrpCat.of ↑(GrpCat.FilteredColimits.G F)

noncomputable def AddGrpCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) : AddGrpCat

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

Equations

• AddGrpCat.FilteredColimits.colimit F = AddGrpCat.of ↑(AddGrpCat.FilteredColimits.G F)

noncomputable def GrpCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddGrpCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit additive group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GrpCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GrpCat) : CategoryTheory.Limits.IsColimit (colimitCocone F)

The proposed colimit cocone is a colimit in GrpCat.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddGrpCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrpCat) : CategoryTheory.Limits.IsColimit (colimitCocone F)

The proposed colimit cocone is a colimit in AddGroup.

Equations

• One or more equations did not get rendered due to their size.

instance GrpCat.FilteredColimits.forget₂Mon_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ GrpCat MonCat)

instance AddGrpCat.FilteredColimits.forget₂AddMon_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ AddGrpCat AddMonCat)

instance GrpCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget GrpCat)

instance AddGrpCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddGrpCat)

@[reducible, inline]

noncomputable abbrev CommGrpCat.FilteredColimits.G {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommGrpCat) : GrpCat

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

Equations

• CommGrpCat.FilteredColimits.G F = GrpCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))

@[reducible, inline]

noncomputable abbrev AddCommGrpCat.FilteredColimits.G {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGrpCat) : AddGrpCat

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

Equations

• AddCommGrpCat.FilteredColimits.G F = AddGrpCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))

@[implicit_reducible]

noncomputable instance CommGrpCat.FilteredColimits.colimitCommGroup {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommGrpCat) : CommGroup ↑(G F)

Equations

• CommGrpCat.FilteredColimits.colimitCommGroup F = { toGroup := (CommGrpCat.FilteredColimits.G F).str, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance AddCommGrpCat.FilteredColimits.colimitAddCommGroup {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGrpCat) : AddCommGroup ↑(G F)

Equations

• AddCommGrpCat.FilteredColimits.colimitAddCommGroup F = { toAddGroup := (AddCommGrpCat.FilteredColimits.G F).str, add_comm := ⋯ }

noncomputable def CommGrpCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommGrpCat) : CommGrpCat

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

Equations

• CommGrpCat.FilteredColimits.colimit F = CommGrpCat.of ↑(CommGrpCat.FilteredColimits.G F)

noncomputable def AddCommGrpCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGrpCat) : AddCommGrpCat

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

Equations

• AddCommGrpCat.FilteredColimits.colimit F = AddCommGrpCat.of ↑(AddCommGrpCat.FilteredColimits.G F)

noncomputable def CommGrpCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommGrpCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit commutative group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommGrpCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGrpCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit additive commutative group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommGrpCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommGrpCat) : CategoryTheory.Limits.IsColimit (colimitCocone F)

The proposed colimit cocone is a colimit in CommGrpCat.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGrpCat) : CategoryTheory.Limits.IsColimit (colimitCocone F)

The proposed colimit cocone is a colimit in AddCommGroup.

Equations

• One or more equations did not get rendered due to their size.

instance CommGrpCat.FilteredColimits.forget₂Group_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommGrpCat GrpCat)

instance AddCommGrpCat.FilteredColimits.forget₂AddGroup_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)

instance CommGrpCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget CommGrpCat)

instance AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddCommGrpCat)