epi_left_of_epi — Mathlib

English

If a morphism h in the category of objects over X is an epimorphism (and pushouts exist), then its left component h.left is epi.

Русский

Если морфизм h в категории объектов над X является эпиморфизмом (и существуют пушауты), то его левая часть h.left также является эпиморфизмом.

LaTeX

$$$ \\text{If } h \\text{ is epi, then } h.left \\text{ is epi.}$$$

Lean4

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

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