colimit_exists_rep — Mathlib

English

Equality of two images under colimit injections is equivalent to the existence of a joint representation through some common index.

Русский

Равенство двух изображений под инъекциями колимита эквивалентно существованию совместного представления через общий индекс.

LaTeX

$$$D.\\iota_i x = D.\\iota_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_rep [HasColimit F] (x : ToType (colimit F)) :
    ∃ (j : J) (y : ToType (F.obj j)), colimit.ι F j y = x :=
  Concrete.isColimit_exists_rep F (colimit.isColimit _) x

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