Theorems · Definition · category theory

ModuleCat.FilteredColimits.M

{R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J (ModuleCat R) → AddCommGrpCat

The colimit of F ⋙ forget₂ (ModuleCat R) AddCommGrpCat in the category AddCommGrpCat. In the following, we will show that this has the structure of an R-module.

Defined in

Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Cited by

8 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingCategoryTheory.SmallCategoryCategoryTheory.IsFiltered