Theorems · Theorem · category theory

AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_right

∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {x y y' : (j : J) × ↑(F.obj j)},
  CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget AddMonCat)) y y' →
    AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x y'

Addition in the colimit is well-defined in the right argument.

Defined in

Mathlib.Algebra.Category.MonCat.FilteredColimits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered