epi_left_of_epi — Mathlib

English

If f is an epi in CostructuredArrow G X, then its left component f.left is an epi.

Русский

Если f — эпиморфизм в CostructuredArrow G X, то его левый компонент f.left является эпиморфизмом.

LaTeX

$$$[\\text{Epi } f] \\Rightarrow [\\text{Epi } f.left]$$$

Lean4

instance epi_left_of_epi [HasPushouts A] [PreservesColimitsOfShape WalkingSpan G] {Y Z : CostructuredArrow G X}
    (f : Y ⟶ Z) [Epi f] : Epi f.left :=
  show Epi ((proj G X).map f) from inferInstance

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