The category of R-modules has all colimits.

From the existence of colimits in AddCommGrpCat, we deduce the existence of colimits in ModuleCat R. This way, we get for free that the functor forget₂ (ModuleCat R) AddCommGrpCat 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.

noncomputable def ModuleCat.HasColimit.coconePointSMul {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : R →+* CategoryTheory.End (CategoryTheory.Limits.colimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)))

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

@[simp]

theorem ModuleCat.HasColimit.coconePointSMul_apply {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] (r : R) : (coconePointSMul F) r = CategoryTheory.Limits.colimMap { app := fun (j : J) => (F.obj j).smul r, naturality := ⋯ }

noncomputable def ModuleCat.HasColimit.colimitCocone {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : CategoryTheory.Limits.Cocone F

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

@[simp]

theorem ModuleCat.HasColimit.colimitCocone_pt_isModule {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : (colimitCocone F).pt.isModule = instModuleCarrierMkOfSMul' (coconePointSMul F)

@[simp]

theorem ModuleCat.HasColimit.colimitCocone_pt_carrier {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : ↑(colimitCocone F).pt = ↑(mkOfSMul' (coconePointSMul F))

@[simp]

theorem ModuleCat.HasColimit.colimitCocone_ι_app {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] (j : J) : (colimitCocone F).ι.app j = homMk (CategoryTheory.Limits.colimit.ι (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)) j) ⋯

@[simp]

theorem ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : (colimitCocone F).pt.isAddCommGroup = instAddCommGroupCarrierMkOfSMul' (coconePointSMul F)

noncomputable def ModuleCat.HasColimit.isColimitColimitCocone {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : CategoryTheory.Limits.IsColimit (colimitCocone F)

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

instance ModuleCat.HasColimit.instHasColimit {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : CategoryTheory.Limits.HasColimit F

instance ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)

instance ModuleCat.HasColimit.reflectsColimit {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : CategoryTheory.Limits.ReflectsColimit F (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)

instance ModuleCat.hasColimitsOfShape (R : Type w) [Ring R] (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat] : CategoryTheory.Limits.HasColimitsOfShape J (ModuleCat R)

instance ModuleCat.reflectsColimitsOfShape (R : Type w) [Ring R] (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat] : CategoryTheory.Limits.ReflectsColimitsOfShape J (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)

instance ModuleCat.hasColimitsOfSize (R : Type w) [Ring R] [CategoryTheory.Limits.HasColimitsOfSize.{v, u, w', w' + 1} AddCommGrpCat] : CategoryTheory.Limits.HasColimitsOfSize.{v, u, w', max (w' + 1) w} (ModuleCat R)

instance ModuleCat.forget₂PreservesColimitsOfShape (R : Type w) [Ring R] (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat] : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)

instance ModuleCat.forget₂PreservesColimitsOfSize (R : Type w) [Ring R] [CategoryTheory.Limits.HasColimitsOfSize.{u, v, w', w' + 1} AddCommGrpCat] : CategoryTheory.Limits.PreservesColimitsOfSize.{u, v, w', w', max w (w' + 1), w' + 1} (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)

instance ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax (R : Type w) [Ring R] [CategoryTheory.Limits.HasColimitsOfSize.{u, v, max w w', max (w + 1) (w' + 1)} AddCommGrpMax] : CategoryTheory.Limits.PreservesColimitsOfSize.{u, v, max w w', max w w', max (w + 1) (w' + 1), max (w + 1) (w' + 1)} (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)

instance ModuleCat.instHasFiniteColimits (R : Type w) [Ring R] : CategoryTheory.Limits.HasFiniteColimits (ModuleCat R)

instance ModuleCat.instHasCoequalizers (R : Type w) [Ring R] : CategoryTheory.Limits.HasCoequalizers (ModuleCat R)

noncomputable def ModuleCat.finsuppCocone (R : Type w) [CommRing R] (M ι : Type u) [AddCommGroup M] [Module R M] : CategoryTheory.Limits.Cofan fun (x : ι) => of R M

The coproduct cone induced by the concrete coproduct.

noncomputable def ModuleCat.finsuppCoconeIsColimit (R : Type w) [CommRing R] (M ι : Type u) [AddCommGroup M] [Module R M] : CategoryTheory.Limits.IsColimit (finsuppCocone R M ι)

The concrete cocoproduct cone is colimiting.