isColimit_rep_eq_iff_exists — Mathlib

English

Equivalence between equality of injections and existence of joint representations, in the Colimit setting.

Русский

Эквивалентность между равенством инъекций и существованием совместных представлений в контексте колимита.

LaTeX

$$$\\forall i,j, x,y:\\, ToType(F.obj i), ToType(F.obj j),\\; (F.obj i)\\text{ and }(F.obj j)\\text{ injections equality } \\iff \\exists k,f,g:\\, i\\to k, j\\to k, F.map f x = F.map g y$$$

Lean4

theorem isColimit_rep_eq_iff_exists {D : Cocone F} {i j : J} (hD : IsColimit D) (x : ToType (F.obj i))
    (y : ToType (F.obj j)) : D.ι.app i x = D.ι.app j y ↔ ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y :=
  ⟨Concrete.isColimit_exists_of_rep_eq.{s} _ hD _ _, Concrete.isColimit_rep_eq_of_exists _ _ _⟩

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