colimit_rep_eq_iff_exists — Mathlib

English

Equivalent statements: equality of colimit injections equals the existence of a common representation.

Русский

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

LaTeX

$$$(\\text{colimit ext}) \\iff (\\exists k,f,g, F.map f x = F.map g y)$$$

Lean4

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

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