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
(in AddCommGroupCat
) carries the structure of an R
-module, thereby showing that the forgetful
functor forget₂ (ModuleCat R) AddCommGroupCat
preserves filtered colimits. In particular, this
implies that forget (ModuleCat R)
preserves filtered colimits.
The colimit of F ⋙ forget₂ (ModuleCat R) AddCommGroupCat
in the category AddCommGroupCat
.
In the following, we will show that this has the structure of an R
-module.
Instances For
The canonical projection into the colimit, as a quotient type.
Instances For
The "unlifted" version of scalar multiplication in the colimit.
Instances For
Scalar multiplication in the colimit. See also colimitSMulAux
.
The bundled R
-module giving the filtered colimit of a diagram.
Instances For
The linear map from a given R
-module in the diagram to the colimit module.
Instances For
The cocone over the proposed colimit module.
Instances For
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.
Instances For
The proposed colimit cocone is a colimit in ModuleCat R
.