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} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) : AddMonCat

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.

@[inline, reducible]

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

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.

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

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

@[inline, reducible]

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

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

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

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

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

The "unlifted" version of negation in the colimit.

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

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

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

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

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

Negation in the colimit. See also colimitNegAux.

theorem AddGroupCat.FilteredColimits.colimitNeg.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (h : CategoryTheory.Limits.Types.Quot.Rel (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)) x y) : AddGroupCat.FilteredColimits.colimitNegAux F x = AddGroupCat.FilteredColimits.colimitNegAux F y

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

Taking inverses in the colimit. See also colimitInvAux.

@[simp]

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

@[simp]

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

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_5 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (x : AddMonCat.FilteredColimits.M (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))) (y : AddMonCat.FilteredColimits.M (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))) (z : AddMonCat.FilteredColimits.M (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))) : x + y + z = x + (y + z)

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_8 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ (x : AddMonCat.FilteredColimits.M (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))), nsmulRec 0 x = nsmulRec 0 x

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_11 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ (a : ↑(AddGroupCat.FilteredColimits.G F)), zsmulRec 0 a = zsmulRec 0 a

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_2 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (a : ↑(AddGroupCat.FilteredColimits.G F)) : a + 0 = a

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_4 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (n : ℕ) (x : ↑(AddGroupCat.FilteredColimits.G F)) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_10 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ (a b : ↑(AddGroupCat.FilteredColimits.G F)), a - b = a - b

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_12 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ (n : ℕ) (a : ↑(AddGroupCat.FilteredColimits.G F)), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_6 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (a : AddMonCat.FilteredColimits.M (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))) : 0 + a = a

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_3 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (x : ↑(AddGroupCat.FilteredColimits.G F)) : AddMonoid.nsmul 0 x = 0

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_1 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (a : ↑(AddGroupCat.FilteredColimits.G F)) : 0 + a = a

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_14 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (x : ↑(AddGroupCat.FilteredColimits.G F)) : -x + x = 0

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_7 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (a : AddMonCat.FilteredColimits.M (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))) : a + 0 = a

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

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_13 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ (n : ℕ) (a : ↑(AddGroupCat.FilteredColimits.G F)), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

theorem AddGroupCat.FilteredColimits.colimitAddGroup.proof_9 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ (n : ℕ) (x : AddMonCat.FilteredColimits.M (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))), nsmulRec (n + 1) x = nsmulRec (n + 1) x

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

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

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

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

The bundled group giving the filtered colimit of a diagram.

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

The cocone over the proposed colimit additive group.

theorem AddGroupCat.FilteredColimits.colimitCocone.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) ⦃X : J⦄ ⦃Y : J⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)).map f) ((AddMonCat.FilteredColimits.colimitCocone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))).ι.app Y) = CategoryTheory.CategoryStruct.comp ((AddMonCat.FilteredColimits.colimitCocone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))).ι.app X) (((CategoryTheory.Functor.const J).obj (AddMonCat.FilteredColimits.colimitCocone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))).pt).map f)

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

The cocone over the proposed colimit group.

theorem AddGroupCat.FilteredColimits.colimitCoconeIsColimit.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (t : CategoryTheory.Limits.Cocone F) : ∀ (x : (AddGroupCat.FilteredColimits.colimitCocone F).pt ⟶ t.pt), (∀ (j : J), CategoryTheory.CategoryStruct.comp ((AddGroupCat.FilteredColimits.colimitCocone F).ι.app j) x = t.ι.app j) → x = (fun t => AddMonCat.FilteredColimits.colimitDesc (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCocone t)) t

theorem AddGroupCat.FilteredColimits.colimitCoconeIsColimit.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (t : CategoryTheory.Limits.Cocone F) (j : J) : CategoryTheory.CategoryStruct.comp ((AddGroupCat.FilteredColimits.colimitCocone F).ι.app j) ((fun t => AddMonCat.FilteredColimits.colimitDesc (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCocone t)) t) = t.ι.app j

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

The proposed colimit cocone is a colimit in AddGroup.

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

The proposed colimit cocone is a colimit in GroupCat.

noncomputable instance AddGroupCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ AddGroupCat AddMonCat)

noncomputable instance GroupCat.FilteredColimits.forget₂MonPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ GroupCat MonCat)

noncomputable instance AddGroupCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddGroupCat)

noncomputable instance GroupCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget GroupCat)

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

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.

@[inline, reducible]

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

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.

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

theorem AddCommGroupCat.FilteredColimits.colimitAddCommGroup.proof_2 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGroupCat) (a : ↑(AddCommMonCat.FilteredColimits.M (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddCommMonCat)))) (b : ↑(AddCommMonCat.FilteredColimits.M (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddCommMonCat)))) : a + b = b + a

theorem AddCommGroupCat.FilteredColimits.colimitAddCommGroup.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGroupCat) (a : ↑(AddCommGroupCat.FilteredColimits.G F)) : -a + a = 0

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

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

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

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

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

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

The cocone over the proposed colimit additive commutative group.

theorem AddCommGroupCat.FilteredColimits.colimitCocone.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGroupCat) ⦃X : J⦄ ⦃Y : J⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat)).map f) ((AddGroupCat.FilteredColimits.colimitCocone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat))).ι.app Y) = CategoryTheory.CategoryStruct.comp ((AddGroupCat.FilteredColimits.colimitCocone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat))).ι.app X) (((CategoryTheory.Functor.const J).obj (AddGroupCat.FilteredColimits.colimitCocone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat))).pt).map f)

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

The cocone over the proposed colimit commutative group.

theorem AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGroupCat) (t : CategoryTheory.Limits.Cocone F) : ∀ (x : (AddCommGroupCat.FilteredColimits.colimitCocone F).pt ⟶ t.pt), (∀ (j : J), CategoryTheory.CategoryStruct.comp ((AddCommGroupCat.FilteredColimits.colimitCocone F).ι.app j) x = t.ι.app j) → x = (fun t => CategoryTheory.Limits.IsColimit.desc (AddGroupCat.FilteredColimits.colimitCoconeIsColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat))) ((CategoryTheory.forget₂ AddCommGroupCat AddGroupCat).mapCocone t)) t

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

The proposed colimit cocone is a colimit in AddCommGroup.

theorem AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGroupCat) (t : CategoryTheory.Limits.Cocone F) (j : J) : CategoryTheory.CategoryStruct.comp ((AddCommGroupCat.FilteredColimits.colimitCocone F).ι.app j) ((fun t => CategoryTheory.Limits.IsColimit.desc (AddGroupCat.FilteredColimits.colimitCoconeIsColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat))) ((CategoryTheory.forget₂ AddCommGroupCat AddGroupCat).mapCocone t)) t) = t.ι.app j

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

The proposed colimit cocone is a colimit in CommGroupCat.

noncomputable instance AddCommGroupCat.FilteredColimits.forget₂AddGroupPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat)

noncomputable instance CommGroupCat.FilteredColimits.forget₂GroupPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommGroupCat GroupCat)

noncomputable instance AddCommGroupCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddCommGroupCat)

noncomputable instance CommGroupCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget CommGroupCat)