mathlib documentation

algebra.category.Module.colimits

The category of R-modules has all colimits. #

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 v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) :
Type v

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

inductive Module.colimits.relation {R : Type v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) :

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]

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

Equations
def Module.colimits.colimit_type {R : Type v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) :
Type v

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

Equations
@[instance]
Equations
@[simp]
theorem Module.colimits.quot_zero {R : Type v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) :
@[simp]
theorem Module.colimits.quot_neg {R : Type v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) (x : Module.colimits.prequotient F) :
quot.mk setoid.r x.neg = -quot.mk setoid.r x
@[simp]
theorem Module.colimits.quot_add {R : Type v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) (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 v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) (s : R) (x : Module.colimits.prequotient F) :
def Module.colimits.colimit {R : Type v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) :

The bundled module giving the colimit of a diagram.

Equations
def Module.colimits.cocone_fun {R : Type v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) (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 v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) (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 v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) {j j' : J} (f : j j') :
@[simp]
theorem Module.colimits.cocone_naturality_components {R : Type v} [ring R] {J : Type v} [category_theory.small_category J] (F : J Module R) (j j' : J) (f : j j') (x : (F.obj j)) :

The cocone over the proposed colimit module.

Equations

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

Equations

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

Equations