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.
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.
The canonical projection into the colimit, as a quotient type.
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⟩
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}
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 := _}
The bundled R
-module giving the filtered colimit of a diagram.
Equations
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' := _}
The cocone over the proposed colimit module.
Equations
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' := _}
The proposed colimit cocone is a colimit in Module R
.
Equations
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))}}