mathlibdocumentation

algebra.category.Module.filtered_colimits

The forgetful functor from R-modules preserves filtered colimits. #

Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend to preserve filtered colimits.

In this file, we start with a ring R, a small filtered category J and a functor F : J ⥤ Module R. We show that the colimit of F ⋙ forget₂ (Module R) AddCommGroup (in AddCommGroup) carries the structure of an R-module, thereby showing that the forgetful functor forget₂ (Module R) AddCommGroup preserves filtered colimits. In particular, this implies that forget (Module R) preserves filtered colimits.

noncomputable def Module.filtered_colimits.M {R : Type u} [ring R] {J : Type v} (F : J ) :

The colimit of F ⋙ forget₂ (Module R) AddCommGroup in the category AddCommGroup. In the following, we will show that this has the structure of an R-module.

def Module.filtered_colimits.M.mk {R : Type u} [ring R] {J : Type v} (F : J ) :
(Σ (j : J), (F.obj j))

The canonical projection into the colimit, as a quotient type.

theorem Module.filtered_colimits.M.mk_eq {R : Type u} [ring R] {J : Type v} (F : J ) (x y : Σ (j : J), (F.obj j)) (h : ∃ (k : J) (f : x.fst k) (g : y.fst k), (F.map f) x.snd = (F.map g) y.snd) :
def Module.filtered_colimits.colimit_smul_aux {R : Type u} [ring R] {J : Type v} (F : J ) (r : R) (x : Σ (j : J), (F.obj j)) :

The "unlifted" version of scalar multiplication in the colimit.

Equations
theorem Module.filtered_colimits.colimit_smul_aux_eq_of_rel {R : Type u} [ring R] {J : Type v} (F : J ) (r : R) (x y : Σ (j : J), (F.obj j))  :
@[protected, instance]
def Module.filtered_colimits.colimit_has_scalar {R : Type u} [ring R] {J : Type v} (F : J ) :

Equations
• = {smul := λ (r : R) (x : , quot.lift _ x}
@[simp]
theorem Module.filtered_colimits.colimit_smul_mk_eq {R : Type u} [ring R] {J : Type v} (F : J ) (r : R) (x : Σ (j : J), (F.obj j)) :
= x.fst, r x.snd
@[protected, instance]
noncomputable def Module.filtered_colimits.colimit_module {R : Type u} [ring R] {J : Type v} (F : J ) :
Equations
noncomputable def Module.filtered_colimits.colimit {R : Type u} [ring R] {J : Type v} (F : J ) :

The bundled R-module giving the filtered colimit of a diagram.

Equations
noncomputable def Module.filtered_colimits.cocone_morphism {R : Type u} [ring R] {J : Type v} (F : J ) (j : J) :

The linear map from a given R-module in the diagram to the colimit module.

Equations
noncomputable def Module.filtered_colimits.colimit_cocone {R : Type u} [ring R] {J : Type v} (F : J ) :

The cocone over the proposed colimit module.

Equations
noncomputable def Module.filtered_colimits.colimit_desc {R : Type u} [ring R] {J : Type v} (F : J )  :

Given a cocone t of F, the induced monoid linear map from the colimit to the cocone point. We already know that this is a morphism between additive groups. The only thing left to see is that it is a linear map, i.e. preserves scalar multiplication.

Equations
noncomputable def Module.filtered_colimits.colimit_cocone_is_colimit {R : Type u} [ring R] {J : Type v} (F : J ) :

The proposed colimit cocone is a colimit in Module R.

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