English
Equivalence between equality of injections at i and j under the colimit and the existence of a common coequalization data.
Русский
Эквивалентность между равенством инъекций на i и j в колимите и существованием общего ряда отображений.
LaTeX
$$$\\forall i,j, x,y:\\, ToType(F.obj i), ToType(F.obj j),\\; (D.ι.app i x = D.ι.app j y) \\iff \\exists k,f,g:\\, i\\to k, j\\to k, F.map f x = F.map g y$$$
Lean4
theorem isColimit_rep_eq_of_exists {D : Cocone F} {i j : J} (x : ToType (F.obj i)) (y : ToType (F.obj j))
(h : ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y) : D.ι.app i x = D.ι.app j y :=
by
let E := (forget C).mapCocone D
obtain ⟨k, f, g, (hfg : (F ⋙ forget C).map f x = F.map g y)⟩ := h
let h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f
let h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g
change E.ι.app i x = E.ι.app j y
rw [← h1, types_comp_apply, hfg]
exact congrFun h2 y
