The category of R-modules has all colimits. #
From the existence of colimits in AddCommGroupCat
, we deduce the existence of colimits
in ModuleCat R
. This way, we get for free that the functor
forget₂ (ModuleCat R) AddCommGroupCat
commutes with colimits.
Note that finite colimits can already be obtained from the instance Abelian (Module R)
.
TODO:
In fact, in ModuleCat R
there is a much nicer model of colimits as quotients
of finitely supported functions, and we really should implement this as well.
The induced scalar multiplication on
colimit (F ⋙ forget₂ _ AddCommGroupCat)
.
Instances For
The cocone for F
constructed from the colimit of
(F ⋙ forget₂ (ModuleCat R) AddCommGroupCat)
.
Instances For
The cocone for F
constructed from the colimit of
(F ⋙ forget₂ (ModuleCat R) AddCommGroupCat)
is a colimit cocone.