# The category of additive commutative groups has all colimits. #

This file uses a "pre-automated" approach, just as for Algebra.Category.MonCat.Colimits. It is a very uniform approach, that conceivably could be synthesised directly by a tactic that analyses the shape of AddCommGroup and MonoidHom.

TODO: In fact, in AddCommGroupCat there is a much nicer model of colimits as quotients of finitely supported functions, and we really should implement this as well (or instead).

We build the colimit of a diagram in AddCommGroupCat 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.

inductive AddCommGroupCat.Colimits.Prequotient {J : Type u} :
Type (max (max u v) w)

An inductive type representing all group expressions (without relations) on a collection of types indexed by the objects of J.

• of: {J : Type u} → [inst : ] → {F : } → (j : J) → (F.obj j)
• zero: {J : Type u} → [inst : ] →
• neg: {J : Type u} → [inst : ] →
• add: {J : Type u} → [inst : ] →
Instances For
Equations
• = { default := AddCommGroupCat.Colimits.Prequotient.zero }

The relation on Prequotient saying when two expressions are equal because of the abelian group laws, or because one element is mapped to another by a morphism in the diagram.

Instances For

The setoid corresponding to group expressions modulo abelian group relations and identifications.

Equations
• = { r := , iseqv := }

The underlying type of the colimit of a diagram in AddCommGroupCat.

Equations
Instances For
Equations
• = { zero := AddCommGroupCat.Colimits.Prequotient.zero }
Equations
• = { neg := Quotient.map AddCommGroupCat.Colimits.Prequotient.neg }
Equations
Equations
• = { default := 0 }
@[simp]
theorem AddCommGroupCat.Colimits.quot_zero {J : Type u} :
@[simp]
theorem AddCommGroupCat.Colimits.quot_neg {J : Type u} :
Quot.mk Setoid.r x.neg = -Quot.mk Setoid.r x
@[simp]
Quot.mk Setoid.r (x.add y) = Quot.mk Setoid.r x + Quot.mk Setoid.r y

The bundled abelian group giving the colimit of a diagram.

Equations
Instances For
def AddCommGroupCat.Colimits.coconeFun {J : Type u} (j : J) (x : (F.obj j)) :

The function from a given abelian group in the diagram to the colimit abelian group.

Equations
Instances For
def AddCommGroupCat.Colimits.coconeMorphism {J : Type u} (j : J) :
F.obj j

The group homomorphism from a given abelian group in the diagram to the colimit abelian group.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem AddCommGroupCat.Colimits.cocone_naturality {J : Type u} {j : J} {j' : J} (f : j j') :
@[simp]
theorem AddCommGroupCat.Colimits.cocone_naturality_components {J : Type u} (j : J) (j' : J) (f : j j') (x : (F.obj j)) :
((F.map f) x) =

The cocone over the proposed colimit abelian group.

Equations
• = { pt := , ι := { app := , naturality := } }
Instances For

The function from the free abelian group on the diagram to the cone point of any other cocone.

Equations
Instances For

The function from the colimit abelian group to the cone point of any other cocone.

Equations
Instances For

The group homomorphism from the colimit abelian group to the cone point of any other cocone.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For

Evidence that the proposed colimit is the colimit.

Equations
• = { desc := fun (s : ) => , fac := , uniq := }
Instances For

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

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