epi_iff_epi_left — Mathlib

English

For morphisms in Over X with pushouts, h is epi if and only if its left component h.left is epi.

Русский

Для морфизмов в Over X с пушаутами, h эпиморфизм тогда и только тогда, когда его левая часть h.left эпиморфизм.

LaTeX

$$$ \\text{Epi}(h) \\;\\Leftrightarrow\\; \\text{Epi}(h.left). $$$

Lean4

theorem epi_iff_epi_left [HasPushouts C] {f g : Over X} (h : f ⟶ g) : Epi h ↔ Epi h.left :=
  CostructuredArrow.epi_iff_epi_left _

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