Commit 2025-11-21 13:53 4a2711ac

View on Github →

feat(CategoryTheory): effective epi implies strong epi (#31860) Also:

Import EffectiveEpi.Basic in the file defining RegularEpi, and prove the relationship there.
Fix some names and golf some proofs in EffectiveEpi.Basic

Estimated changes

Modified Mathlib/CategoryTheory/EffectiveEpi/Basic.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/RegularEpi.lean

deleted theorem CategoryTheory.effectiveEpiOfKernelPair

deleted def CategoryTheory.effectiveEpiStructOfRegularEpi

Modified Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

added def CategoryTheory.effectiveEpiStructOfRegularEpi

added theorem CategoryTheory.effectiveEpi_of_kernelPair