colimit_rep_eq_of_exists — Mathlib

English

For a colimit F and x, there exists a representation via some j with an element y such that colimit.ι F j y = x.

Русский

Для колимита F и элемента x существует представление через некоторый j с элементом y, такое что colimit.ι F j y = x.

LaTeX

$$$\\exists j:\\, J\\;\\exists y:\\, F.obj j,\\; colimit.\\iota F j y = x$$$

Lean4

theorem colimit_rep_eq_of_exists [HasColimit 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) : colimit.ι F i x = colimit.ι F j y :=
  Concrete.isColimit_rep_eq_of_exists F x y h

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