Commit 2023-02-23 12:36 ac350e3f

View on Github →

feat: port CategoryTheory.Functor.EpiMono (#2331)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Functor/EpiMono.lean

added theorem CategoryTheory.Adjunction.strongEpi_map_of_strongEpi

added theorem CategoryTheory.Functor.epi_map_iff_epi

added theorem CategoryTheory.Functor.epi_of_epi_map

added theorem CategoryTheory.Functor.isSplitEpi_iff

added theorem CategoryTheory.Functor.isSplitMono_iff

added theorem CategoryTheory.Functor.mono_map_iff_mono

added theorem CategoryTheory.Functor.mono_of_mono_map

added theorem CategoryTheory.Functor.preservesEpimorphisms.iso_iff

added theorem CategoryTheory.Functor.preservesEpimorphisms.of_iso

added theorem CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects

added theorem CategoryTheory.Functor.preservesEpimorphsisms_of_adjunction

added theorem CategoryTheory.Functor.preservesMonomorphisms.iso_iff

added theorem CategoryTheory.Functor.preservesMonomorphisms.of_iso

added theorem CategoryTheory.Functor.preservesMonomorphisms_of_adjunction

added theorem CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects

added theorem CategoryTheory.Functor.reflectsEpimorphisms.iso_iff

added theorem CategoryTheory.Functor.reflectsEpimorphisms.of_iso

added theorem CategoryTheory.Functor.reflectsEpimorphisms_of_preserves_of_reflects

added theorem CategoryTheory.Functor.reflectsMonomorphisms.iso_iff

added theorem CategoryTheory.Functor.reflectsMonomorphisms.of_iso

added theorem CategoryTheory.Functor.reflectsMonomorphisms_of_preserves_of_reflects

added def CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence

added def CategoryTheory.Functor.splitEpiEquiv

added def CategoryTheory.Functor.splitMonoEquiv

added theorem CategoryTheory.Functor.strongEpi_map_iff_strongEpi_of_isEquivalence