descColimitType_surjective_iff — Mathlib

English

For objects j,j' in J and elements x,y in F.obj j and F.obj j', equality of injections corresponds to the generated equivalence relation in ColimitType.

Русский

Для объектов j,j' в J и элементов x,y в F.obj j и F.obj j' равенство инъекции соответствует образующемуся отношению эквивалентности в F.ColimitType.

LaTeX

$$$F.ιColimitType j x = F.ιColimitType j' y \iff \mathrm{Relation.EqvGen} F.ColimitTypeRel \langle j,x\rangle \langle j',y\rangle$$$

Lean4

theorem descColimitType_surjective_iff :
    Function.Surjective (F.descColimitType c) ↔ ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z :=
  by
  constructor
  · intro h z
    obtain ⟨⟨i, x⟩, rfl⟩ := h z
    exact ⟨i, x, rfl⟩
  · intro h z
    obtain ⟨i, x, rfl⟩ := h z
    exact ⟨F.ιColimitType i x, rfl⟩

Похожие утверждения