mathlib3 documentation

topology.category.Top.epi_mono

Epi- and monomorphisms in Top #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file shows that a continuous function is an epimorphism in the category of topological spaces if and only if it is surjective, and that a continuous function is a monomorphism in the category of topological spaces if and only if it is injective.

source
theorem Top.epi_iff_surjective {X Y : Top} (f : X ⟶ Y) :
category_theory.epi f ↔ function.surjective ⇑f
source
theorem Top.mono_iff_injective {X Y : Top} (f : X ⟶ Y) :
category_theory.mono f ↔ function.injective ⇑f