mathlib3 documentation

algebra.category.Module.filtered_colimits

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

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

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.

@[reducible]

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

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.

@[reducible]

def Module.filtered_colimits.M.mk {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J ⥤ Module R) :

(Σ (j : J), ↥(F.obj j)) → ↥(Module.filtered_colimits.M F)

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} [category_theory.small_category J] [category_theory.is_filtered J] (F : J ⥤ Module R) (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) :

Module.filtered_colimits.M.mk F x = Module.filtered_colimits.M.mk F y

def Module.filtered_colimits.colimit_smul_aux {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J ⥤ Module R) (r : R) (x : Σ (j : J), ↥(F.obj j)) :

↥(Module.filtered_colimits.M F)

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

Equations

Module.filtered_colimits.colimit_smul_aux F r x = Module.filtered_colimits.M.mk F ⟨x.fst, r • x.snd⟩

theorem Module.filtered_colimits.colimit_smul_aux_eq_of_rel {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J ⥤ Module R) (r : R) (x y : Σ (j : J), ↥(F.obj j)) (h : category_theory.limits.types.filtered_colimit.rel (F ⋙ category_theory.forget (Module R)) x y) :

Module.filtered_colimits.colimit_smul_aux F r x = Module.filtered_colimits.colimit_smul_aux F r y

@[protected, instance]

def Module.filtered_colimits.colimit_has_smul {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J ⥤ Module R) :

has_smul R ↥(Module.filtered_colimits.M F)

Scalar multiplication in the colimit. See also colimit_smul_aux.

Equations

Module.filtered_colimits.colimit_has_smul F = {smul := λ (r : R) (x : ↥(Module.filtered_colimits.M F)), quot.lift (Module.filtered_colimits.colimit_smul_aux F r) _ x}

@[simp]

theorem Module.filtered_colimits.colimit_smul_mk_eq {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J ⥤ Module R) (r : R) (x : Σ (j : J), ↥(F.obj j)) :

r • Module.filtered_colimits.M.mk F x = Module.filtered_colimits.M.mk F ⟨x.fst, r • x.snd⟩

@[protected, instance]

def Module.filtered_colimits.colimit_module {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J ⥤ Module R) :

module R ↥(Module.filtered_colimits.M F)

Equations

Module.filtered_colimits.colimit_module F = {to_distrib_mul_action := {to_mul_action := {to_has_smul := Module.filtered_colimits.colimit_has_smul F, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}

noncomputable def Module.filtered_colimits.colimit {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J ⥤ Module R) :

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

Equations

Module.filtered_colimits.colimit F = Module.of R ↥(Module.filtered_colimits.M F)

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

F.obj j ⟶ Module.filtered_colimits.colimit F

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

Equations

Module.filtered_colimits.cocone_morphism F j = {to_fun := ((AddCommGroup.filtered_colimits.colimit_cocone (F ⋙ category_theory.forget₂ (Module R) AddCommGroup)).ι.app j).to_fun, map_add' := _, map_smul' := _}

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

category_theory.limits.cocone F

The cocone over the proposed colimit module.

Equations

Module.filtered_colimits.colimit_cocone F = {X := Module.filtered_colimits.colimit F, ι := {app := Module.filtered_colimits.cocone_morphism F, naturality' := _}}

noncomputable def Module.filtered_colimits.colimit_desc {R : Type u} [ring R] {J : Type v} [category_theory.small_category J] [category_theory.is_filtered J] (F : J ⥤ Module R) (t : category_theory.limits.cocone F) :

Module.filtered_colimits.colimit F ⟶ t.X

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

Module.filtered_colimits.colimit_desc F t = {to_fun := ((AddCommGroup.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ (Module R) AddCommGroup)).desc ((category_theory.forget₂ (Module R) AddCommGroup).map_cocone t)).to_fun, map_add' := _, map_smul' := _}

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

category_theory.limits.is_colimit (Module.filtered_colimits.colimit_cocone F)

The proposed colimit cocone is a colimit in Module R.

Equations

Module.filtered_colimits.colimit_cocone_is_colimit F = {desc := Module.filtered_colimits.colimit_desc F, fac' := _, uniq' := _}

@[protected, instance]

noncomputable def Module.filtered_colimits.forget₂_AddCommGroup_preserves_filtered_colimits {R : Type u} [ring R] :

category_theory.limits.preserves_filtered_colimits (category_theory.forget₂ (Module R) AddCommGroup)

Equations

Module.filtered_colimits.forget₂_AddCommGroup_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ Module R), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (Module.filtered_colimits.colimit_cocone_is_colimit F) (AddCommGroup.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ (Module R) AddCommGroup))}}

@[protected, instance]

noncomputable def Module.filtered_colimits.forget_preserves_filtered_colimits {R : Type u} [ring R] :

category_theory.limits.preserves_filtered_colimits (category_theory.forget (Module R))

Equations

Module.filtered_colimits.forget_preserves_filtered_colimits = category_theory.limits.comp_preserves_filtered_colimits (category_theory.forget₂ (Module R) AddCommGroup) (category_theory.forget AddCommGroup)