mathlib3 documentation

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.

source
inductive Module.colimits.prequotient {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
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
source
@[protected, instance]
def Module.colimits.prequotient.inhabited {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
inhabited (Module.colimits.prequotient F)
Equations
source
inductive Module.colimits.relation {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
Module.colimits.prequotient F → Module.colimits.prequotient F → Prop

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.

source
@[instance]
def Module.colimits.colimit_setoid {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
setoid (Module.colimits.prequotient F)

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

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

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

Equations
Instances for Module.colimits.colimit_type
source
@[protected, instance]
def Module.colimits.colimit_type.add_comm_group {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
add_comm_group (Module.colimits.colimit_type F)
Equations
source
@[protected, instance]
def Module.colimits.colimit_type.module {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
module R (Module.colimits.colimit_type F)
Equations
source
@[simp]
theorem Module.colimits.quot_zero {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
quot.mk setoid.r Module.colimits.prequotient.zero = 0
source
@[simp]
theorem Module.colimits.quot_neg {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) (x : Module.colimits.prequotient F) :
quot.mk setoid.r x.neg = -quot.mk setoid.r x
source
@[simp]
theorem Module.colimits.quot_add {R : Type u} [ring R] {J : Type w} [category_theory.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
source
@[simp]
theorem Module.colimits.quot_smul {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) (s : R) (x : Module.colimits.prequotient F) :
quot.mk setoid.r (Module.colimits.prequotient.smul s x) = s • quot.mk setoid.r x
source
def Module.colimits.colimit {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
Module R

The bundled module giving the colimit of a diagram.

Equations
source
def Module.colimits.cocone_fun {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) (j : J) (x : ↥(F.obj j)) :
Module.colimits.colimit_type F

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

Equations
source
def Module.colimits.cocone_morphism {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) (j : J) :
F.obj j ⟶ Module.colimits.colimit F

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

Equations
source
@[simp]
theorem Module.colimits.cocone_naturality {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) {j j' : J} (f : j ⟶ j') :
F.map f ≫ Module.colimits.cocone_morphism F j' = Module.colimits.cocone_morphism F j
source
@[simp]
theorem Module.colimits.cocone_naturality_components {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) (j j' : J) (f : j ⟶ j') (x : ↥(F.obj j)) :
⇑(Module.colimits.cocone_morphism F j') (⇑(F.map f) x) = ⇑(Module.colimits.cocone_morphism F j) x
source
def Module.colimits.colimit_cocone {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
category_theory.limits.cocone F

The cocone over the proposed colimit module.

Equations
source
@[simp]
def Module.colimits.desc_fun_lift {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) (s : category_theory.limits.cocone F) :
Module.colimits.prequotient F → ↥(s.X)

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

Equations
source
def Module.colimits.desc_fun {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) (s : category_theory.limits.cocone F) :
Module.colimits.colimit_type F → ↥(s.X)

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

Equations
source
def Module.colimits.desc_morphism {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) (s : category_theory.limits.cocone F) :
Module.colimits.colimit F ⟶ s.X

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

Equations
source
def Module.colimits.colimit_cocone_is_colimit {R : Type u} [ring R] {J : Type w} [category_theory.category J] (F : J ⥤ Module R) :
category_theory.limits.is_colimit (Module.colimits.colimit_cocone F)

Evidence that the proposed colimit is the colimit.

Equations
source
@[protected, instance]
def Module.colimits.has_colimits_Module {R : Type u} [ring R] :
category_theory.limits.has_colimits (Module R)
source
@[protected, instance]
def Module.colimits.has_colimits_of_size_Module {R : Type u} [ring R] :
category_theory.limits.has_colimits_of_size (Module R)
source
@[protected, instance]
def Module.colimits.has_colimits_of_size_zero_Module {R : Type u} [ring R] :
category_theory.limits.has_colimits_of_size (Module R)
source
@[protected, instance]
def Module.colimits.has_colimits_Module' (R : Type u) [ring R] :
category_theory.limits.has_colimits (Module R)
source
@[protected, instance]
def Module.colimits.has_colimits_Module'' (R : Type u) [ring R] :
category_theory.limits.has_colimits (Module R)