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 AddCommGrpCat 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 AddCommGrpCat.Colimits.Relations {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [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.

def AddCommGrpCat.Colimits.Quot {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [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.

@[implicit_reducible]

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

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

Inclusion of F.obj j into the candidate colimit.

theorem AddCommGrpCat.Colimits.Quot.addMonoidHom_ext {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [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 AddCommGrpCat.Colimits.Quot.desc {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) (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.

@[simp]

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

@[simp]

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

def AddCommGrpCat.Colimits.quotToQuotUlift {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [DecidableEq J] : Quot F →+ Quot (F.comp uliftFunctor)

The obvious additive map from Quot F to Quot (F ⋙ uliftFunctor.{u'}).

theorem AddCommGrpCat.Colimits.quotToQuotUlift_ι {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [DecidableEq J] (j : J) (x : ↑(F.obj j)) : (quotToQuotUlift F) ((Quot.ι F j) x) = (Quot.ι (F.comp uliftFunctor) j) { down := x }

def AddCommGrpCat.Colimits.quotUliftToQuot {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [DecidableEq J] : Quot (F.comp uliftFunctor) →+ Quot F

The obvious additive map from Quot (F ⋙ uliftFunctor.{u'}) to Quot F.

theorem AddCommGrpCat.Colimits.quotUliftToQuot_ι {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [DecidableEq J] (j : J) (x : ↑((F.comp uliftFunctor).obj j)) : (quotUliftToQuot F) ((Quot.ι (F.comp uliftFunctor) j) x) = (Quot.ι F j) x.down

def AddCommGrpCat.Colimits.quotQuotUliftAddEquiv {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [DecidableEq J] : Quot F ≃+ Quot (F.comp uliftFunctor)

The additive equivalence between Quot F and Quot (F ⋙ uliftFunctor.{u'}).

theorem AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [DecidableEq J] (c : CategoryTheory.Limits.Cocone F) : (desc (F.comp uliftFunctor) (uliftFunctor.mapCocone c)).comp (quotQuotUliftAddEquiv F).toAddMonoidHom = AddEquiv.ulift.symm.toAddMonoidHom.comp (desc F c)

def AddCommGrpCat.Colimits.toCocone {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [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.

@[simp]

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

@[simp]

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

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

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

noncomputable def AddCommGrpCat.Colimits.isColimit_of_bijective_desc {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) (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.

noncomputable def AddCommGrpCat.Colimits.colimitCocone {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [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.

@[simp]

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

@[simp]

theorem AddCommGrpCat.Colimits.colimitCocone_ι_app {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [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 AddCommGrpCat.Colimits.Quot.desc_colimitCocone {J : Type u} [CategoryTheory.Category.{v, u} J] [DecidableEq J] (F : CategoryTheory.Functor J AddCommGrpCat) [Small.{w, max u w} (Quot F)] : desc F (colimitCocone F) = Shrink.addEquiv.symm.toAddMonoidHom

noncomputable def AddCommGrpCat.Colimits.colimitCoconeIsColimit {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [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.

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

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

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

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

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

@[instance 1300]

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

The category of additive commutative groups has all small colimits.

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

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