Commit 2023-11-03 14:28 500b9f9e

View on Github →

feat: CompHaus and friends are preregular (#8126) We prove that CompHaus, Profinite and Stonean are preregular (that effective epis can be pulled back).

Estimated changes

Modified Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

added def CategoryTheory.EffectiveEpiStructId

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

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

Modified Mathlib/Topology/Category/Stonean/Basic.lean

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