Theorems · Theorem · category theory

MonCat.FilteredColimits.colimit_one_eq

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

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

Defined in

Mathlib.Algebra.Category.MonCat.FilteredColimits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered