surjective_eq_epimorphisms — Mathlib

English

Let forget C be a forgetful functor that preserves epimorphisms. Then a morphism f in C is surjective on the underlying sets if and only if f is an epimorphism in C.

Русский

Пусть забывающий функтор forget C сохраняет эпиморфизмы. Тогда морфизм f в C сюръективен по основанию множеств тогда и только тогда, когда он является эпиморфизмом в C.

LaTeX

$$$\\operatorname{MorphismProperty.surjective}(C) = \\operatorname{epimorphisms}(C).$$$

Lean4

theorem surjective_eq_epimorphisms [(forget C).PreservesEpimorphisms] :
    MorphismProperty.surjective C = epimorphisms C :=
  by
  rw [surjective_eq_epimorphisms_iff]
  infer_instance

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