The category of additive commutative groups has all colimits.

This file constructs colimits in the category of additive commutative groups, as quotients of finitely supported functions.

We build the colimit of a diagram in AddCommGrp by constructing the free group on the disjoint union of all the abelian groups in the diagram, then taking the quotient by the abelian group laws within each abelian group, and the identifications given by the morphisms in the diagram.

@[reducible, inline]

abbrev AddCommGrp.Colimits.Relations {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] : AddSubgroup (Π₀ (j : J), ↑(F.obj j))

The relations between elements of the direct sum of the F.obj j given by the morphisms in the diagram J.

Equations

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

def AddCommGrp.Colimits.Quot {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] : Type (max u w)

The candidate for the colimit of F, defined as the quotient of the direct sum of the commutative groups F.obj j by the relations given by the morphisms in the diagram.

Equations

• AddCommGrp.Colimits.Quot F = ((Π₀ (j : J), ↑(F.obj j)) ⧸ AddCommGrp.Colimits.Relations F)

instance AddCommGrp.Colimits.instAddCommGroupQuot {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] : AddCommGroup (Quot F)

Equations

• AddCommGrp.Colimits.instAddCommGroupQuot F = QuotientAddGroup.Quotient.addCommGroup (AddCommGrp.Colimits.Relations F)

def AddCommGrp.Colimits.Quot.ι {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] (j : J) : ↑(F.obj j) →+ Quot F

Inclusion of F.obj j into the candidate colimit.

Equations

• AddCommGrp.Colimits.Quot.ι F j = (QuotientAddGroup.mk' (AddCommGrp.Colimits.Relations F)).comp (DFinsupp.singleAddHom (fun (j : J) => ↑(F.obj j)) j)

theorem AddCommGrp.Colimits.Quot.addMonoidHom_ext {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] {α : Type u_1} [AddMonoid α] {f g : Quot F →+ α} (h : ∀ (j : J) (x : ↑(F.obj j)), f ((ι F j) x) = g ((ι F j) x)) : f = g

def AddCommGrp.Colimits.Quot.desc {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) (c : CategoryTheory.Limits.Cocone F) [DecidableEq J] : Quot F →+ ↑c.pt

(implementation detail) Part of the universal property of the colimit cocone, but without assuming that Quot F lives in the correct universe.

Equations

• AddCommGrp.Colimits.Quot.desc F c = QuotientAddGroup.lift (AddCommGrp.Colimits.Relations F) (DFinsupp.sumAddHom c.ι.app) ⋯

@[simp]

theorem AddCommGrp.Colimits.Quot.ι_desc {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) (c : CategoryTheory.Limits.Cocone F) [DecidableEq J] (j : J) (x : ↑(F.obj j)) : (desc F c) ((ι F j) x) = (c.ι.app j) x

@[simp]

theorem AddCommGrp.Colimits.Quot.map_ι {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] {j j' : J} {f : j ⟶ j'} (x : ↑(F.obj j)) : (ι F j') ((F.map f) x) = (ι F j) x

def AddCommGrp.Colimits.toCocone {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A) : CategoryTheory.Limits.Cocone F

(implementation detail) A morphism of commutative additive groups Quot F →+ A induces a cocone on F as long as the universes work out.

Equations

• AddCommGrp.Colimits.toCocone F f = { pt := AddCommGrp.of A, ι := { app := fun (j : J) => f.comp (AddCommGrp.Colimits.Quot.ι F j), naturality := ⋯ } }

@[simp]

theorem AddCommGrp.Colimits.toCocone_ι_app {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A) (j : J) : (toCocone F f).ι.app j = f.comp (Quot.ι F j)

@[simp]

theorem AddCommGrp.Colimits.toCocone_pt {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A) : (toCocone F f).pt = of A

theorem AddCommGrp.Colimits.Quot.desc_toCocone_desc {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) (c : CategoryTheory.Limits.Cocone F) [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A) (hc : CategoryTheory.Limits.IsColimit c) : AddMonoidHom.comp (hc.desc (toCocone F f)) (desc F c) = f

theorem AddCommGrp.Colimits.Quot.desc_toCocone_desc_app {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) (c : CategoryTheory.Limits.Cocone F) [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A) (hc : CategoryTheory.Limits.IsColimit c) (x : Quot F) : (hc.desc (toCocone F f)) ((desc F c) x) = f x

noncomputable def AddCommGrp.Colimits.isColimit_of_bijective_desc {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) (c : CategoryTheory.Limits.Cocone F) [DecidableEq J] (h : Function.Bijective ⇑(Quot.desc F c)) : CategoryTheory.Limits.IsColimit c

If c is a cocone of F such that Quot.desc F c is bijective, then c is a colimit cocone of F.

Equations

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

noncomputable def AddCommGrp.Colimits.colimitCocone {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] [Small.{w, max w u} (Quot F)] : CategoryTheory.Limits.Cocone F

(internal implementation) The colimit cocone of a functor F, implemented as a quotient of DFinsupp (fun j ↦ F.obj j), under the assumption that said quotient is small.

Equations

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

@[simp]

theorem AddCommGrp.Colimits.colimitCocone_pt {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] [Small.{w, max w u} (Quot F)] : (colimitCocone F).pt = of (Shrink.{w, max u w} (Quot F))

@[simp]

theorem AddCommGrp.Colimits.colimitCocone_ι_app {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] [Small.{w, max w u} (Quot F)] (j : J) : (colimitCocone F).ι.app j = ofHom (Shrink.addEquiv.symm.toAddMonoidHom.comp (Quot.ι F j))

@[simp]

theorem AddCommGrp.Colimits.Quot.desc_colimitCocone {J : Type u} [CategoryTheory.Category.{v, u} J] [DecidableEq J] (F : CategoryTheory.Functor J AddCommGrp) [Small.{w, max u w} (Quot F)] : desc F (colimitCocone F) = Shrink.addEquiv.symm.toAddMonoidHom

noncomputable def AddCommGrp.Colimits.colimitCoconeIsColimit {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] [Small.{w, max u w} (Quot F)] : CategoryTheory.Limits.IsColimit (colimitCocone F)

(internal implementation) The fact that the candidate colimit cocone constructed in colimitCocone is the colimit.

Equations

• AddCommGrp.Colimits.colimitCoconeIsColimit F = AddCommGrp.Colimits.isColimit_of_bijective_desc F (AddCommGrp.Colimits.colimitCocone F) ⋯

theorem AddCommGrp.hasColimit_of_small_quot {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] (h : Small.{w, max u w} (Colimits.Quot F)) : CategoryTheory.Limits.HasColimit F

instance AddCommGrp.instSmallQuot {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] [Small.{w, u} J] : Small.{w, max u w} (Colimits.Quot F)

instance AddCommGrp.hasColimit {J : Type u} [CategoryTheory.Category.{v, u} J] [Small.{w, u} J] (F : CategoryTheory.Functor J AddCommGrp) : CategoryTheory.Limits.HasColimit F

instance AddCommGrp.hasColimitsOfShape {J : Type u} [CategoryTheory.Category.{v, u} J] [Small.{w, u} J] : CategoryTheory.Limits.HasColimitsOfShape J AddCommGrp

If J is w-small, then any functor J ⥤ AddCommGrp.{w} has a colimit.

@[instance 1300]

instance AddCommGrp.hasColimitsOfSize [UnivLE.{u, w}] : CategoryTheory.Limits.HasColimitsOfSize.{v, u, w, w + 1} AddCommGrp

The category of additive commutative groups has all small colimits.

noncomputable def AddCommGrp.cokernelIsoQuotient {G H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.Limits.cokernel f ≅ of (↑H ⧸ AddMonoidHom.range f)

The categorical cokernel of a morphism in AddCommGrp agrees with the usual group-theoretical quotient.

Equations

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