Commit 2025-12-02 07:28 90f5d6d9

View on Github →

refactor(CategoryTheory): promote IsRegularMono/Epi from abbrev to class and add some API (#32192)

Estimated changes

Modified Mathlib/CategoryTheory/Adhesive.lean

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

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

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

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

added def CategoryTheory.IsRegularEpi.W

added def CategoryTheory.IsRegularEpi.desc

added theorem CategoryTheory.IsRegularEpi.fac

added def CategoryTheory.IsRegularEpi.getStruct

added def CategoryTheory.IsRegularEpi.isColimit

added def CategoryTheory.IsRegularEpi.left

added def CategoryTheory.IsRegularEpi.right

added theorem CategoryTheory.IsRegularEpi.uniq

added theorem CategoryTheory.IsRegularEpi.w

added def CategoryTheory.IsRegularMono.Z

added theorem CategoryTheory.IsRegularMono.fac

added def CategoryTheory.IsRegularMono.getStruct

added def CategoryTheory.IsRegularMono.isLimit

added def CategoryTheory.IsRegularMono.left

added def CategoryTheory.IsRegularMono.lift

added def CategoryTheory.IsRegularMono.right

added theorem CategoryTheory.IsRegularMono.uniq

added theorem CategoryTheory.IsRegularMono.w

modified theorem CategoryTheory.isRegularEpi_of_regularEpi

modified theorem CategoryTheory.isRegularMono_of_regularMono

added def CategoryTheory.regularEpiOfEffectiveEpi

deleted def CategoryTheory.regularEpiOfIsRegularEpi

added def CategoryTheory.regularEpiOfKernelPair

deleted def CategoryTheory.regularMonoOfIsRegularMono

Modified Mathlib/CategoryTheory/Topos/Classifier.lean

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