Theorems · Theorem · category theory

AddMonCat.FilteredColimits.colimit_add_mk_eq

∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (x y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k),
  AddMonCat.FilteredColimits.M.mk F x + AddMonCat.FilteredColimits.M.mk F y =
    AddMonCat.FilteredColimits.M.mk F
      ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd + (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩

Addition in the colimit is independent of the chosen "maximum" in the filtered category. In particular, this lemma allows us to "unfold" the definition of the addition of x and y, using a custom object k and morphisms f : x.1 ⟶ k and g : y.1 ⟶ k.

Defined in

Mathlib.Algebra.Category.MonCat.FilteredColimits

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered