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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

• Grp.FilteredColimits.G.mk F = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel (F.comp (CategoryTheory.forget Grp)))

@[reducible, inline]

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

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

Equations

• AddGrp.FilteredColimits.G.mk F = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel (F.comp (CategoryTheory.forget AddGrp)))

theorem Grp.FilteredColimits.G.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J Grp) (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 AddGrp.FilteredColimits.G.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrp) (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

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

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

Equations

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

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

The "unlifted" version of negation in the colimit.

Equations

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

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

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

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

Taking inverses in the colimit. See also colimitInvAux.

Equations

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

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

Negation in the colimit. See also colimitNegAux.

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

The bundled group giving the filtered colimit of a diagram.

Equations

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

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

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

Equations

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

noncomputable def Grp.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J Grp) : 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 AddGrp.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrp) : 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 Grp.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J Grp) : CategoryTheory.Limits.IsColimit (colimitCocone F)

The proposed colimit cocone is a colimit in Grp.

Equations

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

noncomputable def AddGrp.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrp) : 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 Grp.FilteredColimits.forget₂Mon_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ Grp MonCat)

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

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

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

@[reducible, inline]

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

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

Equations

• CommGrp.FilteredColimits.G F = Grp.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ CommGrp Grp))

@[reducible, inline]

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

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

Equations

• AddCommGrp.FilteredColimits.G F = AddGrp.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp))

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

noncomputable def CommGrp.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommGrp) : 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 AddCommGrp.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGrp) : 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 CommGrp.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommGrp) : CategoryTheory.Limits.IsColimit (colimitCocone F)

The proposed colimit cocone is a colimit in CommGrp.

Equations

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

noncomputable def AddCommGrp.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGrp) : 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 CommGrp.FilteredColimits.forget₂Group_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommGrp Grp)

instance AddCommGrp.FilteredColimits.forget₂AddGroup_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ AddCommGrp AddGrp)

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

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