epi_of_epi_left — Mathlib

English

In Over X, if k.left is an epimorphism, then k is an epimorphism (the forgetful functor reflects epis).

Русский

В Over X, если k.left является эпиморфизмом, то и k является эпиморфизмом (forgetful-функтор отражает эпиморфизмы).

LaTeX

$$$ Epi(k) \quad \text{ given } Epi(k.left) $$$

Lean4

/-- If `k.left` is an epimorphism, then `k` is an epimorphism. In other words, `Over.forget X` reflects
epimorphisms.
The converse does not hold without additional assumptions on the underlying category, see
`CategoryTheory.Over.epi_left_of_epi`.
-/
theorem epi_of_epi_left {f g : Over X} (k : f ⟶ g) [hk : Epi k.left] : Epi k :=
  (forget X).epi_of_epi_map hk

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