Structures · Category theory
CategoryTheory.Regular
A regular category is a category with finite limits, such that every kernel pair has a coequalizer, and such that regular epimorphisms are stable under base change.
- Shape
- One type argument · adds hasCoequalizer_of_isKernelPair, regularEpiIsStableUnderBaseChange
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by21
- CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation
- CategoryTheory.Regular.frobeniusMorphism
- CategoryTheory.Regular.instMonoDesc
- CategoryTheory.Regular.regularEpiOfExtremalEpi
- CategoryTheory.Regular.frobeniusMorphism_isPullback
- CategoryTheory.instPreregular
- CategoryTheory.Regular.toHasFiniteLimits
- CategoryTheory.Regular.instHasCoequalizerFstSnd
- CategoryTheory.instIsRegularEpiSnd
- CategoryTheory.Regular.exists_inf_pullback_eq_exists_inf
- CategoryTheory.Regular.hasCoequalizer_of_isKernelPair
- CategoryTheory.Regular.instIsRegularEpiEStrongEpiMonoFactorisation
- CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I
- CategoryTheory.Regular.hasStrongEpiMonoFactorisations
- CategoryTheory.instIsRegularEpiFst
- CategoryTheory.Regular.regularEpiIsStableUnderBaseChange
- CategoryTheory.Regular.instIsRegularEpiFrobeniusMorphism
- CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e
- CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m
- CategoryTheory.Regular.isRegularEpi_of_extremalEpi
- CategoryTheory.Regular.strongEpiMonoFactorisation