isColimit_exists_of_rep_eq — Mathlib

English

Equality of two colimit injections implies the existence of a common representation through some index.

Русский

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

LaTeX

$$$D.\\iota_i x = D.\\iota_j y \\Rightarrow \\exists k,f,g:\\, i\\to k, j\\to k, F.map f x = F.map g y$$$

Lean4

theorem isColimit_exists_of_rep_eq {D : Cocone F} {i j : J} (hD : IsColimit D) (x : ToType (F.obj i))
    (y : ToType (F.obj j)) (h : D.ι.app _ x = D.ι.app _ y) : ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y :=
  by
  let E := (forget C).mapCocone D
  let hE : IsColimit E := isColimitOfPreserves _ hD
  exact (Types.FilteredColimit.isColimit_eq_iff (F ⋙ forget C) hE).mp h

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