Theorems · Definition · category theory

ModuleCat.FilteredColimits.M.mk

{R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) → (j : J) × ↑(F.obj j) → ↑(ModuleCat.FilteredColimits.M F)

The canonical projection into the colimit, as a quotient type.

Defined in

Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Cited by

7 results in Mathlib

Foundations

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

Assumes

RingCategoryTheory.SmallCategoryCategoryTheory.IsFiltered