The category of additive commutative groups has all colimits.
This file uses a "pre-automated" approach, just as for Mon/colimits.lean.
It is a very uniform approach, that conceivably could be synthesised directly
by a tactic that analyses the shape of add_comm_group and monoid_hom.
TODO:
In fact, in AddCommGroup 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 AddCommGroup 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
AddCommGroup.colimits.prequotient
{J : Type v}
[category_theory.small_category J] :
J ⥤ AddCommGroup → Type v
- of : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (j : J), ↥(F.obj j) → AddCommGroup.colimits.prequotient F
- zero : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup), AddCommGroup.colimits.prequotient F
- neg : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup), AddCommGroup.colimits.prequotient F → AddCommGroup.colimits.prequotient F
- add : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup), AddCommGroup.colimits.prequotient F → AddCommGroup.colimits.prequotient F → AddCommGroup.colimits.prequotient F
An inductive type representing all group expressions (without relations)
on a collection of types indexed by the objects of J.
@[instance]
def
AddCommGroup.colimits.inhabited
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup) :
Equations
inductive
AddCommGroup.colimits.relation
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup) :
- refl : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F x x
- symm : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x y : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F x y → AddCommGroup.colimits.relation F y x
- trans : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x y z : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F x y → AddCommGroup.colimits.relation F y z → AddCommGroup.colimits.relation F x z
- map : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (j j' : J) (f : j ⟶ j') (x : ↥(F.obj j)), AddCommGroup.colimits.relation F (AddCommGroup.colimits.prequotient.of j' (⇑(F.map f) x)) (AddCommGroup.colimits.prequotient.of j x)
- zero : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (j : J), AddCommGroup.colimits.relation F (AddCommGroup.colimits.prequotient.of j 0) AddCommGroup.colimits.prequotient.zero
- neg : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (j : J) (x : ↥(F.obj j)), AddCommGroup.colimits.relation F (AddCommGroup.colimits.prequotient.of j (-x)) (AddCommGroup.colimits.prequotient.of j x).neg
- add : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (j : J) (x y : ↥(F.obj j)), AddCommGroup.colimits.relation F (AddCommGroup.colimits.prequotient.of j (x + y)) ((AddCommGroup.colimits.prequotient.of j x).add (AddCommGroup.colimits.prequotient.of j y))
- neg_1 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x x' : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F x x' → AddCommGroup.colimits.relation F x.neg x'.neg
- add_1 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x x' y : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F x x' → AddCommGroup.colimits.relation F (x.add y) (x'.add y)
- add_2 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x y y' : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F y y' → AddCommGroup.colimits.relation F (x.add y) (x.add y')
- zero_add : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F (AddCommGroup.colimits.prequotient.zero.add x) x
- add_zero : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F (x.add AddCommGroup.colimits.prequotient.zero) x
- add_left_neg : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F (x.neg.add x) AddCommGroup.colimits.prequotient.zero
- add_comm : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x y : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F (x.add y) (y.add x)
- add_assoc : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ AddCommGroup) (x y z : AddCommGroup.colimits.prequotient F), AddCommGroup.colimits.relation F ((x.add y).add z) (x.add (y.add z))
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.
@[instance]
def
AddCommGroup.colimits.colimit_setoid
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup) :
The setoid corresponding to group expressions modulo abelian group relations and identifications.
Equations
@[instance]
def
AddCommGroup.colimits.colimit_type.inhabited
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup) :
def
AddCommGroup.colimits.colimit_type
{J : Type v}
[category_theory.small_category J] :
J ⥤ AddCommGroup → Type v
The underlying type of the colimit of a diagram in AddCommGroup.
@[instance]
def
AddCommGroup.colimits.add_comm_group
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup) :
Equations
- AddCommGroup.colimits.add_comm_group F = {add := quot.lift (λ (x : AddCommGroup.colimits.prequotient F), quot.lift (λ (y : AddCommGroup.colimits.prequotient F), quot.mk setoid.r (x.add y)) _) _, add_assoc := _, zero := quot.mk setoid.r AddCommGroup.colimits.prequotient.zero, zero_add := _, add_zero := _, neg := quot.lift (λ (x : AddCommGroup.colimits.prequotient F), quot.mk setoid.r x.neg) _, add_left_neg := _, add_comm := _}
@[simp]
theorem
AddCommGroup.colimits.quot_zero
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup) :
quot.mk setoid.r AddCommGroup.colimits.prequotient.zero = 0
@[simp]
theorem
AddCommGroup.colimits.quot_neg
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup)
(x : AddCommGroup.colimits.prequotient F) :
@[simp]
theorem
AddCommGroup.colimits.quot_add
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup)
(x y : AddCommGroup.colimits.prequotient F) :
The bundled abelian group giving the colimit of a diagram.
def
AddCommGroup.colimits.cocone_fun
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup)
(j : J) :
↥(F.obj j) → AddCommGroup.colimits.colimit_type F
The function from a given abelian group in the diagram to the colimit abelian group.
Equations
- AddCommGroup.colimits.cocone_fun F j x = quot.mk setoid.r (AddCommGroup.colimits.prequotient.of j x)
def
AddCommGroup.colimits.cocone_morphism
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup)
(j : J) :
The group homomorphism from a given abelian group in the diagram to the colimit abelian group.
Equations
- AddCommGroup.colimits.cocone_morphism F j = {to_fun := AddCommGroup.colimits.cocone_fun F j, map_zero' := _, map_add' := _}
@[simp]
theorem
AddCommGroup.colimits.cocone_naturality
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup)
{j j' : J}
(f : j ⟶ j') :
@[simp]
theorem
AddCommGroup.colimits.cocone_naturality_components
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup)
(j j' : J)
(f : j ⟶ j')
(x : ↥(F.obj j)) :
⇑(AddCommGroup.colimits.cocone_morphism F j') (⇑(F.map f) x) = ⇑(AddCommGroup.colimits.cocone_morphism F j) x
def
AddCommGroup.colimits.colimit_cocone
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup) :
The cocone over the proposed colimit abelian group.
Equations
- AddCommGroup.colimits.colimit_cocone F = {X := AddCommGroup.colimits.colimit F, ι := {app := AddCommGroup.colimits.cocone_morphism F, naturality' := _}}
@[simp]
def
AddCommGroup.colimits.desc_fun_lift
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup)
(s : category_theory.limits.cocone F) :
AddCommGroup.colimits.prequotient F → ↥(s.X)
The function from the free abelian group on the diagram to the cone point of any other cocone.
Equations
- AddCommGroup.colimits.desc_fun_lift F s (x.add y) = AddCommGroup.colimits.desc_fun_lift F s x + AddCommGroup.colimits.desc_fun_lift F s y
- AddCommGroup.colimits.desc_fun_lift F s x.neg = -AddCommGroup.colimits.desc_fun_lift F s x
- AddCommGroup.colimits.desc_fun_lift F s AddCommGroup.colimits.prequotient.zero = 0
- AddCommGroup.colimits.desc_fun_lift F s (AddCommGroup.colimits.prequotient.of j x) = ⇑(s.ι.app j) x
def
AddCommGroup.colimits.desc_fun
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup)
(s : category_theory.limits.cocone F) :
AddCommGroup.colimits.colimit_type F → ↥(s.X)
The function from the colimit abelian group to the cone point of any other cocone.
Equations
- AddCommGroup.colimits.desc_fun F s = quot.lift (AddCommGroup.colimits.desc_fun_lift F s) _
def
AddCommGroup.colimits.desc_morphism
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup)
(s : category_theory.limits.cocone F) :
The group homomorphism from the colimit abelian group to the cone point of any other cocone.
Equations
- AddCommGroup.colimits.desc_morphism F s = {to_fun := AddCommGroup.colimits.desc_fun F s, map_zero' := _, map_add' := _}
def
AddCommGroup.colimits.colimit_is_colimit
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ AddCommGroup) :
Evidence that the proposed colimit is the colimit.
Equations
- AddCommGroup.colimits.colimit_is_colimit F = {desc := λ (s : category_theory.limits.cocone F), AddCommGroup.colimits.desc_morphism F s, fac' := _, uniq' := _}
@[instance]
Equations
- AddCommGroup.colimits.has_colimits_AddCommGroup = {has_colimits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_colimit := λ (F : J ⥤ AddCommGroup), {cocone := AddCommGroup.colimits.colimit_cocone F, is_colimit := AddCommGroup.colimits.colimit_is_colimit F}}}
The categorical cokernel of a morphism in AddCommGroup
agrees with the usual group-theoretical quotient.