colimit_exists_of_rep_eq — Mathlib

English

Equivalence between equality of limit injections and existence of index-based equalizers in the limit diagram.

Русский

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

LaTeX

$$$\\forall i,j:\\, J,\\; (\\mathrm{limit}.\\pi F i x = \\mathrm{limit}.\\pi F j y) \\iff \\exists k,f,g:\\, i\\to k, j\\to k, F.map f x = F.map g y$$$

Lean4

theorem colimit_exists_of_rep_eq [HasColimit F] {i j : J} (x : ToType (F.obj i)) (y : ToType (F.obj j))
    (h : colimit.ι F _ x = colimit.ι F _ y) : ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y :=
  Concrete.isColimit_exists_of_rep_eq.{s} F (colimit.isColimit _) x y h

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