# mathlib3documentation

algebra.category.Module.colimits

# The category of R-modules has all colimits. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file uses a "pre-automated" approach, just as for Mon/colimits.lean.

Note that finite colimits can already be obtained from the instance abelian (Module R).

TODO: In fact, in Module R 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 Module 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 Module.colimits.prequotient {R : Type u} [ring R] {J : Type w} (F : J ) :
Type (max u v w)

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

Instances for Module.colimits.prequotient
@[protected, instance]
def Module.colimits.prequotient.inhabited {R : Type u} [ring R] {J : Type w} (F : J ) :
Equations
inductive Module.colimits.relation {R : Type u} [ring R] {J : Type w} (F : J ) :

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

@[instance]
def Module.colimits.colimit_setoid {R : Type u} [ring R] {J : Type w} (F : J ) :

The setoid corresponding to module expressions modulo module relations and identifications.

Equations
@[protected, instance]
def Module.colimits.colimit_type.inhabited {R : Type u} [ring R] {J : Type w} (F : J ) :
def Module.colimits.colimit_type {R : Type u} [ring R] {J : Type w} (F : J ) :
Type (max u v w)

The underlying type of the colimit of a diagram in Module R.

Equations
Instances for Module.colimits.colimit_type
@[protected, instance]
def Module.colimits.colimit_type.add_comm_group {R : Type u} [ring R] {J : Type w} (F : J ) :
Equations
@[protected, instance]
def Module.colimits.colimit_type.module {R : Type u} [ring R] {J : Type w} (F : J ) :
Equations
@[simp]
theorem Module.colimits.quot_zero {R : Type u} [ring R] {J : Type w} (F : J ) :
@[simp]
theorem Module.colimits.quot_neg {R : Type u} [ring R] {J : Type w} (F : J )  :
quot.mk setoid.r x.neg = -quot.mk setoid.r x
@[simp]
theorem Module.colimits.quot_add {R : Type u} [ring R] {J : Type w} (F : J ) (x y : Module.colimits.prequotient F) :
quot.mk setoid.r (x.add y) = quot.mk setoid.r x + quot.mk setoid.r y
@[simp]
theorem Module.colimits.quot_smul {R : Type u} [ring R] {J : Type w} (F : J ) (s : R)  :
quot.mk setoid.r = s quot.mk setoid.r x
def Module.colimits.colimit {R : Type u} [ring R] {J : Type w} (F : J ) :

The bundled module giving the colimit of a diagram.

Equations
def Module.colimits.cocone_fun {R : Type u} [ring R] {J : Type w} (F : J ) (j : J) (x : (F.obj j)) :

The function from a given module in the diagram to the colimit module.

Equations
def Module.colimits.cocone_morphism {R : Type u} [ring R] {J : Type w} (F : J ) (j : J) :

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

Equations
@[simp]
theorem Module.colimits.cocone_naturality {R : Type u} [ring R] {J : Type w} (F : J ) {j j' : J} (f : j j') :
@[simp]
theorem Module.colimits.cocone_naturality_components {R : Type u} [ring R] {J : Type w} (F : J ) (j j' : J) (f : j j') (x : (F.obj j)) :
((F.map f) x) =
def Module.colimits.colimit_cocone {R : Type u} [ring R] {J : Type w} (F : J ) :

The cocone over the proposed colimit module.

Equations
@[simp]
def Module.colimits.desc_fun_lift {R : Type u} [ring R] {J : Type w} (F : J )  :

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

Equations
def Module.colimits.desc_fun {R : Type u} [ring R] {J : Type w} (F : J )  :

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

Equations
• = quot.lift _
def Module.colimits.desc_morphism {R : Type u} [ring R] {J : Type w} (F : J )  :

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

Equations
def Module.colimits.colimit_cocone_is_colimit {R : Type u} [ring R] {J : Type w} (F : J ) :

Evidence that the proposed colimit is the colimit.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]