epi_iff_surjective — Mathlib

English

In TopCat, an arrow is epic if and only if it is surjective on the underlying function.

Русский

В TopCat эпиморфизм эквивалентен сюръективности соответствующей функции.

LaTeX

$$$\\text{Epi}(f) \\iff \\text{Function.Surjective}(f)$$$

Lean4

theorem epi_iff_surjective {X Y : TopCat.{u}} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f :=
  by
  suffices Epi f ↔ Epi ((forget TopCat).map f)
    by
    rw [this, CategoryTheory.epi_iff_surjective]
    rfl
  constructor
  · intro
    infer_instance
  · apply Functor.epi_of_epi_map

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