Mathlib.Topology.Category.TopCat.EpiMono

Module docstring

{"# Epi- and monomorphisms in Top

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. "}

TopCat.epi_iff_surjective theorem

{X Y : TopCat.{u}} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f

Full source

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

Epimorphisms in Topological Spaces are Surjective Continuous Functions

Informal description

For any continuous function $f \colon X \to Y$ between topological spaces $X$ and $Y$, $f$ is an epimorphism in the category of topological spaces if and only if $f$ is surjective.

TopCat.mono_iff_injective theorem

{X Y : TopCat.{u}} (f : X ⟶ Y) : Mono f ↔ Function.Injective f

Full source

theorem mono_iff_injective {X Y : TopCatTopCat.{u}} (f : X ⟶ Y) : MonoMono f ↔ Function.Injective f := by
  suffices MonoMono f ↔ Mono ((forget TopCat).map f) by
    rw [this, CategoryTheory.mono_iff_injective]
    rfl
  constructor
  · intro
    infer_instance
  · apply Functor.mono_of_mono_map

Monomorphisms in Topological Spaces are Injective Continuous Maps

Informal description

A continuous map $f \colon X \to Y$ between topological spaces is a monomorphism in the category of topological spaces if and only if $f$ is injective.