Regular categories

A regular category is a 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 [Gran2021].
• We show that every regular category satisfies Frobenius reciprocity. That is, that in their internal language, we have ∃ x, (P(x) ⊓ Q) iff (∃ x, P(x)) ⊓ Q, for a proposition Q not depending on x.

Future work

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

References

• [Marino Gran, An Introduction to Regular Categories][Gran2021]
• 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.

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.

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

noncomputable def CategoryTheory.Regular.frobeniusMorphism {C : Type u} [Category.{v, u} C] [Regular C] {A B : C} (f : A ⟶ B) (A' : Subobject A) (B' : Subobject B) : Subobject.underlying.obj (A' ⊓ (Subobject.pullback f).obj B') ⟶ Subobject.underlying.obj ((Subobject.exists f).obj A' ⊓ B')

Given a morphism f : A ⟶ B and subobjects A' ⟶ A and B' ⟶ B, we have a canonical morphism (A' ⊓ (Subobject.pullback f).obj B') ⟶ ((«exists» f).obj A' ⊓ B'). This morphism is part of a StrongEpiMonoFactorosation of (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f, see frobeniusStrongEpiMonoFactorisation.

theorem CategoryTheory.Regular.frobeniusMorphism_isPullback {C : Type u} [Category.{v, u} C] [Regular C] {A B : C} (f : A ⟶ B) (A' : Subobject A) (B' : Subobject B) : IsPullback (frobeniusMorphism f A' B') ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯) (((Subobject.exists f).obj A' ⊓ B').ofLE ((Subobject.exists f).obj A') ⋯) (Subobject.imageFactorisation f A').F.e

instance CategoryTheory.Regular.instIsRegularEpiFrobeniusMorphism {C : Type u} [Category.{v, u} C] [Regular C] {A B : C} (f : A ⟶ B) (A' : Subobject A) (B' : Subobject B) : IsRegularEpi (frobeniusMorphism f A' B')

noncomputable def CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation {C : Type u} [Category.{v, u} C] [Regular C] {A B : C} (f : A ⟶ B) (A' : Subobject A) (B' : Subobject B) : Limits.StrongEpiMonoFactorisation (CategoryStruct.comp (A' ⊓ (Subobject.pullback f).obj B').arrow f)

Given a morphism f : A ⟶ B and subobjects A' ⟶ A and B' ⟶ B, the frobeniusMorphism gives a StrongEpiMonoFactorisation of (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f through ((«exists» f).obj A' ⊓ B').arrow. This is an auxiliary definition to show frobenius_reciprocity.

@[simp]

theorem CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e {C : Type u} [Category.{v, u} C] [Regular C] {A B : C} (f : A ⟶ B) (A' : Subobject A) (B' : Subobject B) : (frobeniusStrongEpiMonoFactorisation f A' B').e = frobeniusMorphism f A' B'

@[simp]

theorem CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m {C : Type u} [Category.{v, u} C] [Regular C] {A B : C} (f : A ⟶ B) (A' : Subobject A) (B' : Subobject B) : (frobeniusStrongEpiMonoFactorisation f A' B').m = ((Subobject.exists f).obj A' ⊓ B').arrow

@[simp]

theorem CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I {C : Type u} [Category.{v, u} C] [Regular C] {A B : C} (f : A ⟶ B) (A' : Subobject A) (B' : Subobject B) : (frobeniusStrongEpiMonoFactorisation f A' B').I = Subobject.underlying.obj ((Subobject.exists f).obj A' ⊓ B')

theorem CategoryTheory.Regular.exists_inf_pullback_eq_exists_inf {C : Type u} [Category.{v, u} C] [Regular C] {A B : C} (f : A ⟶ B) (A' : Subobject A) (B' : Subobject B) : (Subobject.exists f).obj (A' ⊓ (Subobject.pullback f).obj B') = (Subobject.exists f).obj A' ⊓ B'

Regular categories satisfy Frobenius reciprocity. That is, in the internal language of regular categories, we have ∃ x, (P(x) ⊓ Q) iff (∃ x, P(x)) ⊓ Q, for a proposition Q not depending on x.