Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-15 17:08 b5aae18a

View on Github →

feat(category_theory): monos and epis in Type and Top (#1030)

feat(category_theory): monos and epis in Type and Top
imports
add file header
use notation for adjunction

Estimated changes

Created src/category_theory/epi_mono.lean

added theorem category_theory.faithful_reflects_epi

added theorem category_theory.faithful_reflects_mono

added theorem category_theory.left_adjoint_preserves_epi

added theorem category_theory.right_adjoint_preserves_mono

Modified src/category_theory/instances/Top/default.lean

Created src/category_theory/instances/Top/epi_mono.lean

added theorem category_theory.instances.Top.epi_iff_surjective

added theorem category_theory.instances.Top.mono_iff_injective

Modified src/category_theory/types.lean

added theorem category_theory.epi_iff_surjective

added def category_theory.hom_of_element

added theorem category_theory.hom_of_element_eq_iff

added theorem category_theory.mono_iff_injective