Theorems · Theorem · category theory

AddMonCat.FilteredColimits.colimit_zero_eq

∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (j : J), 0 = AddMonCat.FilteredColimits.M.mk F ⟨j, 0⟩

The definition of the "zero" in the colimit is independent of the chosen object of J. In particular, this lemma allows us to "unfold" the definition of colimit_zero at a custom chosen object j.

Defined in

Mathlib.Algebra.Category.MonCat.FilteredColimits

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered