isSeparator_of_isColimit_cofan — Mathlib

English

If a cofan is the colimit of a diagram, and its range is separating, then the cocone's base is a separator.

Русский

Если кофан является колимитом диаграммы и его диапазон разделяет, то база кокон-коллиматорной схемы является разделителем.

LaTeX

$$$\\mathrm{IsSeparating}(\\mathrm{range}(f)) \\Rightarrow \\mathrm{IsSeparator}(c.pt)$$$

Lean4

theorem isSeparator_of_isColimit_cofan {β : Type w} {f : β → C} (hf : IsSeparating (Set.range f)) {c : Cofan f}
    (hc : IsColimit c) : IsSeparator c.pt :=
  by
  refine (isSeparator_def _).2 fun X Y u v huv => hf _ _ fun Z hZ g => ?_
  obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ
  classical simpa using c.ι.app ⟨b⟩ ≫= huv (hc.desc (Cofan.mk _ (Pi.single b g)))

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