Commit 2025-12-01 06:24 6a263ebf

View on Github →

refactor(Category Theory): change RegularMono/Epi from class to structure (#32154) Refactors RegularEpi to be a structure. See zulip.

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean

modified def CategoryTheory.LiftLeftAdjoint.counitCoequalises

Modified Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean

modified def CategoryTheory.LiftRightAdjoint.unitEqualises

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

modified def CategoryTheory.IsKernelPair.toCoequalizer

Modified Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean

added def CategoryTheory.NormalEpi.regularEpi

added def CategoryTheory.NormalMono.regularMono

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

modified def CategoryTheory.RegularEpi.desc'

added theorem CategoryTheory.RegularEpi.effectiveEpi

added theorem CategoryTheory.RegularEpi.epi

added def CategoryTheory.RegularEpi.ofSplitEpi

added structure CategoryTheory.RegularEpi

added def CategoryTheory.RegularMono.equalizer

modified def CategoryTheory.RegularMono.lift'

added theorem CategoryTheory.RegularMono.mono

added def CategoryTheory.RegularMono.ofIsSplitMono

added theorem CategoryTheory.RegularMono.strongMono

added structure CategoryTheory.RegularMono

added def CategoryTheory.coequalizerRegular

modified def CategoryTheory.effectiveEpiStructOfRegularEpi

modified theorem CategoryTheory.isIso_of_regularEpi_of_mono

modified theorem CategoryTheory.isIso_of_regularMono_of_epi

added theorem CategoryTheory.isRegularEpi_of_regularEpi

added theorem CategoryTheory.isRegularMono_of_regularMono

added theorem CategoryTheory.strongEpi_of_regularEpi

Modified Mathlib/CategoryTheory/Topos/Classifier.lean

Modified Mathlib/Topology/Category/TopCat/EffectiveEpi.lean