CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutSign UpSign In

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

| Download

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Project: Xena
Views: 18536
License: APACHE
Tweet
Share
Share
/-
Copyright (c) 2019 Reid Barton. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Reid Barton
-/
import topology.category.Top.adjunctions
import category_theory.epi_mono

universe u

open category_theory
open Top

namespace Top

lemma epi_iff_surjective {X Y : Top.{u}} (f : X ⟶ Y) : epi f ↔ function.surjective f :=
begin
  suffices : epi f ↔ epi ((forget Top).map f),
  { rw [this, category_theory.epi_iff_surjective], refl },
  split,
  { apply left_adjoint_preserves_epi adj₂ },
  { apply faithful_reflects_epi }
end

lemma mono_iff_injective {X Y : Top.{u}} (f : X ⟶ Y) : mono f ↔ function.injective f :=
begin
  suffices : mono f ↔ mono ((forget Top).map f),
  { rw [this, category_theory.mono_iff_injective], refl },
  split,
  { apply right_adjoint_preserves_mono adj₁ },
  { apply faithful_reflects_mono }
end

end Top