# Documentation

Mathlib.Algebra.Category.ModuleCat.Colimits

# 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.

@[simp]
noncomputable def ModuleCat.HasColimit.coconePointSMul {R : Type w} [Ring R] {J : Type u} (F : ) :

The induced scalar multiplication on colimit (F ⋙ forget₂ _ AddCommGroupCat).

Instances For
@[simp]
theorem ModuleCat.HasColimit.colimitCocone_ι_app {R : Type w} [Ring R] {J : Type u} (F : ) (j : J) :
.app j = ModuleCat.homMk () (_ : ∀ (r : R), CategoryTheory.CategoryStruct.comp () (↑(ModuleCat.smul ((().obj ()).obj j)) r) = CategoryTheory.CategoryStruct.comp (↑(ModuleCat.smul (F.obj j)) r) ())
@[simp]
theorem ModuleCat.HasColimit.colimitCocone_pt {R : Type w} [Ring R] {J : Type u} (F : ) :
noncomputable def ModuleCat.HasColimit.colimitCocone {R : Type w} [Ring R] {J : Type u} (F : ) :

The cocone for F constructed from the colimit of (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat).

Instances For
noncomputable def ModuleCat.HasColimit.isColimitColimitCocone {R : Type w} [Ring R] {J : Type u} (F : ) :

The cocone for F constructed from the colimit of (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) is a colimit cocone.

Instances For
instance ModuleCat.hasColimitsOfShape (R : Type w) [Ring R] (J : Type u) :
noncomputable instance ModuleCat.forget₂PreservesColimitsOfShape (R : Type w) [Ring R] (J : Type u) :
noncomputable instance ModuleCat.forget₂PreservesColimitsOfSize (R : Type w) [Ring R] :