Regular categories

A regular category is category with finite limits such that each kernel pair has a coequalizer and such that regular epimorphisms are stable under pullback.

These categories provide a good ground to develop the calculus of relations, as well as being the semantics for regular logic.

Main results

• We show that every regular category has strong epi-mono factorisations, following Theorem 1.11 in [Gra21].

Future work

• Show Frobenius reciprocity
• Show that every topos is regular
• Show that regular logic has an interpretation in regular categories

References

• Marino Gran, An Introduction to Regular Categories
• https://ncatlab.org/nlab/show/regular+category

class CategoryTheory.Regular (C : Type u) [Category.{v, u} C] extends CategoryTheory.Limits.HasFiniteLimits C : Prop

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.

• out (J : Type) [𝒥 : SmallCategory J] [FinCategory J] : HasLimitsOfShape J C
• hasCoequalizer_of_isKernelPair {X Y Z : C} {f : X ⟶ Y} {g₁ g₂ : Z ⟶ X} : IsKernelPair f g₁ g₂ → Limits.HasCoequalizer g₁ g₂
• regularEpiIsStableUnderBaseChange : (MorphismProperty.regularEpi C).IsStableUnderBaseChange

instance CategoryTheory.instIsRegularEpiSnd {C : Type u} [Category.{v, u} C] [Regular C] {X Y B : C} (f : X ⟶ B) (g : Y ⟶ B) [Limits.HasPullback f g] [IsRegularEpi f] : IsRegularEpi (Limits.pullback.snd f g)

instance CategoryTheory.instIsRegularEpiFst {C : Type u} [Category.{v, u} C] [Regular C] {X Y B : C} (f : X ⟶ B) (g : Y ⟶ B) [Limits.HasPullback f g] [IsRegularEpi g] : IsRegularEpi (Limits.pullback.fst f g)

instance CategoryTheory.instPreregular {C : Type u} [Category.{v, u} C] [Regular C] : Preregular C

theorem CategoryTheory.Regular.instHasCoequalizerFstSnd {C : Type u} [Category.{v, u} C] [Regular C] {X Y : C} (f : X ⟶ Y) : Limits.HasCoequalizer (Limits.pullback.fst f f) (Limits.pullback.snd f f)

instance CategoryTheory.Regular.instMonoDesc {C : Type u} [Category.{v, u} C] [Regular C] {X Y : C} (f : X ⟶ Y) : Mono (Limits.coequalizer.desc f ⋯)

noncomputable def CategoryTheory.Regular.strongEpiMonoFactorisation {C : Type u} [Category.{v, u} C] [Regular C] {X Y : C} (f : X ⟶ Y) : Limits.StrongEpiMonoFactorisation f

In a regular category, every morphism f : X ⟶ Y factors as e ≫ m, where e is the projection map to the coequalizer of the kernel pair of f, and m is the canonical map from that coequalizer to Y. In particular, f factors as a strong epimorphism followed by a monomorphism.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Regular.instIsRegularEpiEStrongEpiMonoFactorisation {C : Type u} [Category.{v, u} C] [Regular C] {X Y : C} (f : X ⟶ Y) : IsRegularEpi (strongEpiMonoFactorisation f).e

instance CategoryTheory.Regular.hasStrongEpiMonoFactorisations {C : Type u} [Category.{v, u} C] [Regular C] : Limits.HasStrongEpiMonoFactorisations C

In a regular category, every morphism f factors as e ≫ m, with e a strong epimorphism and m a monomorphism.

noncomputable def CategoryTheory.Regular.regularEpiOfExtremalEpi {C : Type u} [Category.{v, u} C] [Regular C] {X Y : C} (f : X ⟶ Y) [h : ExtremalEpi f] : RegularEpi f

In a regular category, every extremal epimorphism is a regular epimorphism.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Regular.isRegularEpi_of_extremalEpi {C : Type u} [Category.{v, u} C] [Regular C] {X Y : C} (f : X ⟶ Y) [ExtremalEpi f] : IsRegularEpi f