English
For a cocone c over F, the map descColimitType c: F.ColimitType → ? is injective if and only if the following holds: for all j, j' in J and x ∈ F(j), x' ∈ F(j'), whenever c.ι j x = c.ι j' x', there exists k ∈ J and morphisms f: j → k, f': j' → k with F.map f x = F.map f' x'.
Русский
Для кокона c над F отображение descColimitType c: F.ColimitType → ? инъективно тогда и только тогда, когда для любых j, j' ∈ J и x ∈ F(j), x' ∈ F(j'), если c.ι j x = c.ι j' x', то существует k ∈ J и морфизмы f: j → k, f': j' → k такие, что F.map f x = F.map f' x'.
LaTeX
$$$$ \text{Injective}(F.descColimitType\, c) \iff \forall j\, j'\, x:\, F(j)\, , x':\, F(j')\, , c.ι j x = c.ι j' x' \to \exists k:\, J, \exists f: j \to k, \exists f': j' \to k, F.map f\, x = F.map f'\, x'. $$$$
Lean4
theorem descColimitType_injective_iff_of_isFiltered :
Function.Injective (F.descColimitType c) ↔
∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
c.ι j x = c.ι j' x' → ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k), F.map f x = F.map f' x' :=
by
constructor
· intro h j j' x x' eq
have : F.ιColimitType j x = F.ιColimitType j' x' := h eq
rwa [ιColimitType_eq_iff_of_isFiltered] at this
· intro h x x' eq
obtain ⟨i, x, rfl⟩ := F.ιColimitType_jointly_surjective x
obtain ⟨i', x', rfl⟩ := F.ιColimitType_jointly_surjective x'
simp only [descColimitType_ιColimitType_apply] at eq
obtain ⟨k, f, f', eq⟩ := h _ _ _ _ eq
rw [← F.ιColimitType_map f x, eq, F.ιColimitType_map]
