epi_of_epi_right — Mathlib

English

If k is an epimorphism, then k.right is an epimorphism.

Русский

Если k является эпиморфизмом, то k.right тоже эпиморфизм.

LaTeX

$$k.right is Epi implies k is Epi$$

Lean4

/-- If `k.right` is an epimorphism, then `k` is an epimorphism. In other words, `Under.forget X`
reflects epimorphisms.
The converse of `CategoryTheory.Under.epi_right_of_epi`.

This lemma is not an instance, to avoid loops in type class inference.
-/
theorem epi_of_epi_right {f g : Under X} (k : f ⟶ g) [hk : Epi k.right] : Epi k :=
  (forget X).epi_of_epi_map hk

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