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 ⥤ ModuleCat R. We show that the colimit of
F ⋙ forget₂ (ModuleCat R) AddCommGroupCat
AddCommGroupCat) carries the structure of an
R-module, thereby showing that the forgetful
forget₂ (ModuleCat R) AddCommGroupCat preserves filtered colimits. In particular, this
forget (ModuleCat R) preserves filtered colimits.
The canonical projection into the colimit, as a quotient type.
The "unlifted" version of scalar multiplication in the colimit.
Scalar multiplication in the colimit. See also
The linear map from a given
R-module in the diagram to the colimit module.
Given a cocone
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.
The proposed colimit cocone is a colimit in