English
If t is a colimit cocone for F, then for any i and x,y in F(i), t.ι.app i x = t.ι.app i y iff there exists j and f:i→j with F.map f x = F.map f y.
Русский
Если t — колимитный кокон для F, то для любого i и элементов x,y ∈ F(i) равенство t.ι.app i x = t.ι.app i y эквивалентно существованию j и морфизма f:i→j с F.map f x = F.map f y.
LaTeX
$$$\\forall i\\,\\forall x,y\\in F(i),\\ t.ι.app i x = t.ι.app i y \\iff \\exists j\\,\\exists f:i\\to j,\\ F.map f x = F.map f y$$$
Lean4
theorem isColimit_eq_iff {t : Cocone F} (ht : IsColimit t) {i j : J} {xi : F.obj i} {xj : F.obj j} :
t.ι.app i xi = t.ι.app j xj ↔ ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
by
have : HasColimit F := ⟨_, ht⟩
refine Iff.trans ?_ (colimit_eq_iff_aux F)
rw [← (IsColimit.coconePointUniqueUpToIso ht (colimitCoconeIsColimit F)).toEquiv.injective.eq_iff]
convert Iff.rfl
· exact (congrFun (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xi).symm
· exact (congrFun (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xj).symm
