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.

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.

instance AddCommGrp.Colimits.instAddCommGroupQuot {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) [DecidableEq J] : AddCommGroup (Quot 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.

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.

@[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) = (CategoryTheory.ConcreteCategory.hom (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') ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = (ι F j) x

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

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

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

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

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

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

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

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

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

@[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 = ofHom (f.comp (Quot.ι F j))

@[simp]

theorem AddCommGrp.Colimits.toCocone_pt_coe {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 = 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) : (Hom.hom (hc.desc (toCocone F f))).comp (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) : (CategoryTheory.ConcreteCategory.hom (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.

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.

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

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 ⧸ (Hom.hom f).range)

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