Theorems · Theorem · category theory

ModuleCat.FilteredColimits.M.mk_eq

∀ {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)) (x y : (j : J) × ↑(F.obj j)),
  (∃ k f g,
      (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd) →
    ModuleCat.FilteredColimits.M.mk F x = ModuleCat.FilteredColimits.M.mk F y

Defined in

Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingCategoryTheory.SmallCategoryCategoryTheory.IsFiltered