# The category of R-modules has all colimits. #

From the existence of colimits in AddCommGrp, we deduce the existence of colimits in ModuleCat R. This way, we get for free that the functor forget₂ (ModuleCat R) AddCommGrp 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]
theorem ModuleCat.HasColimit.coconePointSMul_apply {R : Type w} [Ring R] {J : Type u} (F : ) [] (r : R) :
= CategoryTheory.Limits.colimMap { app := fun (j : J) => (F.obj j).smul r, naturality := }
noncomputable def ModuleCat.HasColimit.coconePointSMul {R : Type w} [Ring R] {J : Type u} (F : ) [] :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ModuleCat.HasColimit.colimitCocone_ι_app {R : Type w} [Ring R] {J : Type u} (F : ) [] (j : J) :
@[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) AddCommGrp).

Equations
• One or more equations did not get rendered due to their size.
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) AddCommGrp) is a colimit cocone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance ModuleCat.HasColimit.instHasColimit {R : Type w} [Ring R] {J : Type u} (F : ) [] :
Equations
• =
noncomputable instance ModuleCat.HasColimit.instPreservesColimitAddCommGrpForget₂ {R : Type w} [Ring R] {J : Type u} (F : ) [] :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance ModuleCat.HasColimit.reflectsColimit {R : Type w} [Ring R] {J : Type u} (F : ) [] :
Equations
instance ModuleCat.hasColimitsOfShape (R : Type w) [Ring R] (J : Type u) :
Equations
• =
noncomputable instance ModuleCat.reflectsColimitsOfShape (R : Type w) [Ring R] (J : Type u) :
Equations
• = { reflectsColimit := fun {K : } => inferInstance }
instance ModuleCat.hasColimitsOfSize (R : Type w) [Ring R] [] :
Equations
• =
noncomputable instance ModuleCat.forget₂PreservesColimitsOfShape (R : Type w) [Ring R] (J : Type u) :
Equations
• = { preservesColimit := fun {K : } => inferInstance }
noncomputable instance ModuleCat.forget₂PreservesColimitsOfSize (R : Type w) [Ring R] [] :
Equations
• = { preservesColimitsOfShape := fun {J : Type ?u.29} [] => inferInstance }
Equations
• One or more equations did not get rendered due to their size.
Equations
• =
instance ModuleCat.instHasCoequalizers (R : Type w) [Ring R] :
Equations
• =