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.

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]

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))

abbrev AddGrp.FilteredColimits.G.mk {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrp) : (j : J) × ↑(F.obj j) → ↑(AddGrp.FilteredColimits.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)))

@[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) → ↑(Grp.FilteredColimits.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)))

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

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

def AddGrp.FilteredColimits.colimitNegAux {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrp) (x : (j : J) × ↑(F.obj j)) : ↑(AddGrp.FilteredColimits.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⟩

def Grp.FilteredColimits.colimitInvAux {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J Grp) (x : (j : J) × ↑(F.obj j)) : ↑(Grp.FilteredColimits.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⁻¹⟩

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

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

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

instance AddGrp.FilteredColimits.colimitNeg {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGrp) : Neg ↑(AddGrp.FilteredColimits.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 }

instance Grp.FilteredColimits.colimitInv {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J Grp) : Inv ↑(Grp.FilteredColimits.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 }

@[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)) : -AddGrp.FilteredColimits.G.mk F x = AddGrp.FilteredColimits.G.mk F ⟨x.fst, -x.snd⟩

@[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)) : (Grp.FilteredColimits.G.mk F x)⁻¹ = Grp.FilteredColimits.G.mk F ⟨x.fst, x.snd⁻¹⟩

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

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

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

Equations

• AddGrp.FilteredColimits.colimitAddGroup F = let __src := AddGrp.FilteredColimits.colimitNeg F; let __src_1 := (AddGrp.FilteredColimits.G F).str; AddGroup.mk ⋯

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

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

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

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

Equations

• Grp.FilteredColimits.colimitGroup F = let __src := Grp.FilteredColimits.colimitInv F; let __src_1 := (Grp.FilteredColimits.G F).str; Group.mk ⋯

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.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)

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

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.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.

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

The proposed colimit cocone is a colimit in AddGroup.

Equations

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

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

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

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

Equations

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

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

Equations

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

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

Equations

• AddGrp.FilteredColimits.forgetPreservesFilteredColimits = CategoryTheory.Limits.compPreservesFilteredColimits (CategoryTheory.forget₂ AddGrp AddMonCat) (CategoryTheory.forget AddMonCat)

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

Equations

• Grp.FilteredColimits.forgetPreservesFilteredColimits = CategoryTheory.Limits.compPreservesFilteredColimits (CategoryTheory.forget₂ Grp MonCat) (CategoryTheory.forget MonCat)

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))

@[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))

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

Equations

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

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

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

Equations

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

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.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.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.

theorem AddCommGrp.FilteredColimits.colimitCocone.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommGrp) ⦃X : J⦄ ⦃Y : J⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp)).map f) ((AddGrp.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp))).ι.app Y) = CategoryTheory.CategoryStruct.comp ((AddGrp.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp))).ι.app X) (((CategoryTheory.Functor.const J).obj (AddGrp.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp))).pt).map 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.

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

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

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

The proposed colimit cocone is a colimit in AddCommGroup.

Equations

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

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

Equations

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

noncomputable instance CommGrp.FilteredColimits.forget₂GroupPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommGrp Grp)

Equations

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

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

Equations

• AddCommGrp.FilteredColimits.forgetPreservesFilteredColimits = CategoryTheory.Limits.compPreservesFilteredColimits (CategoryTheory.forget₂ AddCommGrp AddGrp) (CategoryTheory.forget AddGrp)

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

Equations

• CommGrp.FilteredColimits.forgetPreservesFilteredColimits = CategoryTheory.Limits.compPreservesFilteredColimits (CategoryTheory.forget₂ CommGrp Grp) (CategoryTheory.forget Grp)