Documentation

Mathlib.Algebra.Category.ModuleCat.Colimits

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.

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    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

      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