English
Let J be a filtered category and F: J → Type a diagram. For any object j in J and elements x, y ∈ F(j), equality of their images in the colimit type, F.ιColimitType j x = F.ιColimitType j y, holds if and only if there exists an object k ∈ J and a morphism f: j → k such that F.map f (x) = F.map f (y).
Русский
Пусть J — фильтрованная категория и F: J → Type — диаграмма. Пусть j ∈ J и x, y ∈ F(j). Равенство образов x и y в типе-ко-лимите, F.ιColimitType j x = F.ιColimitType j y, эквивалентно существованию объекта k ∈ J и morphism f: j → k such that F.map f x = F.map f y.
LaTeX
$$$$ F.\iotaColimitType\, j\, x = F.\iotaColimitType\, j\, y \iff \exists k: J, \exists f: j \to k, F.map f\, x = F.map f\, y. $$$$
Lean4
/-- More precise variant of the lemma `ιColimitType_eq_iff_of_isFiltered`
in the case both `x` and `y` and in the same type `F.obj j`. -/
theorem ιColimitType_eq_iff_of_isFiltered' {j : J} (x y : F.obj j) :
F.ιColimitType j x = F.ιColimitType j y ↔ ∃ (k : J) (f : j ⟶ k), F.map f x = F.map f y :=
by
rw [ιColimitType_eq_iff_of_isFiltered]
constructor
· rintro ⟨k, f, f', h⟩
refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩
nth_rw 2 [coeq_condition]
simp [h]
· rintro ⟨k, f, h⟩
exact ⟨k, f, f, h⟩
