epi_of_isColimitMkIdId — Mathlib

English

If f: X → Y and t is the colimit of the cocone mk(id_Y, id_Y) for the diagram (f,f), then f is epi.

Русский

Если для диаграммы (f,f) колимит-коно t строится из mk(id_Y, id_Y), то f является эпиморфизмом.

LaTeX

$$$\\text{If } t = \\mathrm{PushoutCocone.mk}(\\mathrm{id}_Y,\\mathrm{id}_Y) \\; \\text{for } f,\\; \\; t\\text{ isColimit } \\Rightarrow \\Epi f$$$

Lean4

/-- `f` is an epi if the pushout cocone `(𝟙 X, 𝟙 X)` is a colimit for the pair `(f, f)`.
The converse is given in `PushoutCocone.isColimitMkIdId`.
-/
theorem epi_of_isColimitMkIdId (f : X ⟶ Y) (t : IsColimit (mk (𝟙 Y) (𝟙 Y) rfl : PushoutCocone f f)) : Epi f :=
  ⟨fun {Z} g h eq => by
    rcases PushoutCocone.IsColimit.desc' t _ _ eq with ⟨_, rfl, rfl⟩
    rfl⟩

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