Commit 2023-02-15 14:53 238118c2

View on Github →

feat: port CategoryTheory.EpiMono (#2292)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/EpiMono.lean

added theorem CategoryTheory.IsIso.of_epi_section'

added theorem CategoryTheory.IsIso.of_epi_section

added theorem CategoryTheory.IsIso.of_mono_retraction'

added theorem CategoryTheory.IsIso.of_mono_retraction

added theorem CategoryTheory.IsSplitEpi.id

added theorem CategoryTheory.IsSplitEpi.mk'

added theorem CategoryTheory.IsSplitMono.id

added theorem CategoryTheory.IsSplitMono.mk'

added theorem CategoryTheory.SplitEpi.epi

added def CategoryTheory.SplitEpi.map

added def CategoryTheory.SplitEpi.splitMono

added structure CategoryTheory.SplitEpi

added def CategoryTheory.SplitMono.map

added theorem CategoryTheory.SplitMono.mono

added def CategoryTheory.SplitMono.splitEpi

added structure CategoryTheory.SplitMono

added theorem CategoryTheory.isIso_of_epi_of_isSplitMono

added theorem CategoryTheory.isIso_of_mono_of_isSplitEpi

added theorem CategoryTheory.isSplitEpi_of_epi

added theorem CategoryTheory.isSplitMono_of_mono