Theorems · Theorem · category theory

ModuleCat.FilteredColimits.colimit_add_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 : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k),
  ModuleCat.FilteredColimits.M.mk F x + ModuleCat.FilteredColimits.M.mk F y =
    ModuleCat.FilteredColimits.M.mk F
      ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd + (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩

Defined in

Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingCategoryTheory.SmallCategoryCategoryTheory.IsFiltered