colimit_eq_iff — Mathlib

English

If HasColimit F, then the standard colimit criterion holds: equality of injections t.ι.app i xi = t.ι.app j xj is equivalent to the existence of a common apex with maps f,g such that F.map f xi = F.map g xj.

Русский

Если имеется колимит F, то равенство инъекций колимитного кокона эквивалентно существованию общего апекса с картами f,g такие, что F.map f xi = F.map g xj.

LaTeX

$$$[HasColimit F]\\;\\Rightarrow\\; t := colimit F:\\; t.ι F i xi = t.ι F j xj \\iff ∃ k \\; f:i\\to k, g:j\\to k,\\ F.map f xi = F.map g xj$$$

Lean4

theorem colimit_eq_iff [HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} :
    colimit.ι F i xi = colimit.ι F j xj ↔ ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
  isColimit_eq_iff _ (colimit.isColimit F)

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