module Cat.Regular where

Regular categoriesπŸ”—

A regular category is a category with pullback-stable image factorisations. To define regular categories, we use the theory of orthogonal morphisms, specifically strong epimorphisms: A regular category is one where every morphism factors as a strong epimorphism followed by a monomorphism, and strong epimorphisms are stable under pullback.

At face value, it’s a bit weird to take the definition of regular categories to talk about strong, rather than regular, epimorphisms. But it turns out that strong epimorphisms correspond pretty directly to the idea of an image factorisation, or at least much more directly than regular epimorphisms do. As we shall see, in a regular category, every strong epimorphism is regular.

  record is-regular : Type (o βŠ” β„“) where
    field
      factor : βˆ€ {a b} (f : C.Hom a b) β†’ Factorisation π’ž StrongEpi Mono f
      stable : is-pullback-stable π’ž (is-strong-epi π’ž)
      has-is-lex : Finitely-complete π’ž

    module factor {a b} (f : C.Hom a b) = Factorisation (factor f)
    module lex = Finitely-complete has-is-lex

We also introduce some more palatable names for the components of the provided factorisations: Letting be a map and its image factorisation, we refer to as to as aβ† im[_], and as im[_]β†ͺb. These latter two names have a placeholder for the morphism we are factoring.

    im[_] : βˆ€ {a b} (f : C.Hom a b) β†’ C.Ob
    im[ f ] = factor f .Factorisation.mediating

    im[_]β†ͺb : βˆ€ {a b} (f : C.Hom a b) β†’ im[ f ] C.β†ͺ b
    im[ f ]β†ͺb = record { monic = out! (factor f .Factorisation.forget∈M) }

    aβ† im[_] : βˆ€ {a b} (f : C.Hom a b) β†’ C.Hom a im[ f ]
    a↠im[ f ] = factor f .Factorisation.mediate

MotivationπŸ”—

Regular categories are interesting in the study of categorical logic since they have exactly the structure required for their subobject fibrations to interpret existential quantifiers, and for these to commute with substitution which, in this case, is interpreted as pullback.

We’ve already seen that, in a category with pullbacks, arbitrary morphisms induce an adjunction between the right adjoint models the substitution (base change) along and the left adjoint models the dependent sum over Between subobject categories, though, pullbacks are not enough structure: this can be seen type-theoretically by noting that, even if is a family of propositions, the sum will generally not be.

Instead, the existential quantifier must be truncated to work correctly, and it is this truncation that the pullback-stable image factorisations in a regular category exist to model. In a category with pullbacks and images, we have adjunctions now between However, the existence of images is not enough to guarantee they behave type-theoretically. In a regular category, since images are stable under pullback, the equation

holds as long as and fit into a pullback square, expressing that existential quantification commutes with substitution.

Another reason to be interested in regular categories is their well-behaved calculus of relations: any category with pullbacks has an associated bicategory of spans, but images are precisely what’s missing to interpret composition of relations. Indeed, the existential quantifier in a regular category allows us to interpret the formula for relational composition,

internally to an arbitrary category. Regularity comes in when we want to show that composition of relations is associative: indeed, associativity in the formula above, modulo associativity of the conjunction is exactly a question of commutativity between and substitution. It follows, but we do not establish here, that a category is regular exactly when its composition of relations is associative.

As a universe for interpreting logic, regular categories allow us to talk about formulae (in arbitrary contexts) consisting of conjunction, equality, truth, and existential quantification, and all of these connectives commute with substitution. This subset of logic is, unsurprisingly, called regular logic. For working with regular categories, one notes that is regular, and that regularity is preserved by slicing.

Strong epis are regularπŸ”—

This section formalises the proof of A1.3.4 from (Johnstone 2002), which says that every strong epimorphism1 in a regular category is regular. Actually, we’ll show that every strong epimorphism in a regular category is effective: it’s the coequaliser of its kernel pair.

  -- Johnstone, A.1.3.4
  module _ (r : is-regular) {A B} (f : C.Hom A B) (is-s : is-strong-epi π’ž f) where
    private
      module r = is-regular r
      module kp = Pullback (r.lex.pullbacks f f)
        renaming (apex to R ; p₁ to a ; pβ‚‚ to b)

For a strong epimorphism start by pulling back along itself to form the kernel pair We want to show that coequalises and which means that any morphism satisfying should have a unique factorisation through So, quantify over such morphisms and let’s get started.

    private module Make {C} {c : C.Hom A C} (w : c C.∘ a ≑ c C.∘ b) where

We start by calculating the image factorisation of

      dgh : Factorisation π’ž StrongEpi Mono ⟨ f , c ⟩
      dgh = r.factor ⟨ f , c ⟩
      module dgh = Factorisation dgh
        renaming (mediating to D ; forget to gh ; mediate to d)
      open dgh using (D ; d ; gh)

      g : C.Hom D B
      g = π₁ C.∘ gh

      h : C.Hom D C
      h = Ο€β‚‚ C.∘ gh

Following Johnstone, we show that is an isomorphism, so that is the factorisation we’re looking for.2 Since is an extremal epimorphism, any monomorphism through which it factors must be an iso. And since we have

it will suffice to show that is a monomorphism. So assume you’re given with Let’s show that Start by pulling back along obtaining

      g-monic : C.is-monic g
      g-monic {e} k l w' = out! dgh.forget∈M _ _ remβ‚ˆ where
        dΓ—d = Γ—-functor .F₁ (d , d)
        module pb = Pullback (r.lex.pullbacks ⟨ k , l ⟩ dΓ—d)
          renaming (p₁ to p ; apex to P ; pβ‚‚ to mn ; square to sq'-)
        open pb using (p ; P ; mn ; sq'-)
        m = π₁ C.∘ mn
        n = Ο€β‚‚ C.∘ mn
        sq' : ⟨ k C.∘ p , l C.∘ p ⟩ ≑ ⟨ d C.∘ m , d C.∘ n ⟩
        sq' = sym (⟨⟩∘ _) βˆ™ sq'- βˆ™ ⟨⟩-unique _ (C.pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ C.pullr refl)
                                               (C.pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ C.pullr refl)

We define a map into the kernel pair of factoring through Using this morphism we may conclude that (rem₁).

        q : C.Hom P R
        q = kp.universal $
          f ∘ m         β‰‘βŸ¨ C.pushl (extend-π₁ dgh.factors βˆ™ C.pulll refl) βŸ©β‰‘
          g ∘ d ∘ m     β‰‘Λ˜βŸ¨ refl⟩∘⟨ by-π₁ sq' βŸ©β‰‘Λ˜
          g ∘ k ∘ p     β‰‘βŸ¨ C.extendl w' βŸ©β‰‘
          g ∘ l ∘ p     β‰‘βŸ¨ refl⟩∘⟨ by-Ο€β‚‚ sq' βŸ©β‰‘
          g ∘ d ∘ n     β‰‘Λ˜βŸ¨ C.pushl (extend-π₁ dgh.factors βˆ™ C.pulll refl) βŸ©β‰‘Λ˜
          f ∘ n         ∎

        rem₁ = h ∘ k ∘ p     β‰‘βŸ¨ refl⟩∘⟨ by-π₁ sq' βŸ©β‰‘
               h ∘ d ∘ m     β‰‘βŸ¨ pulll (pullr (sym dgh.factors) βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©) βŸ©β‰‘
               c ∘ m         β‰‘Λ˜βŸ¨ refl⟩∘⟨ kp.pβ‚βˆ˜universal βŸ©β‰‘Λ˜
               c ∘ a ∘ q     β‰‘βŸ¨ extendl w βŸ©β‰‘
               c ∘ b ∘ q     β‰‘βŸ¨ refl⟩∘⟨ kp.pβ‚‚βˆ˜universal βŸ©β‰‘
               c ∘ n         β‰‘Λ˜βŸ¨ pulll (pullr (sym dgh.factors) βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©) βŸ©β‰‘Λ˜
               h ∘ d ∘ n     β‰‘Λ˜βŸ¨ refl⟩∘⟨ by-Ο€β‚‚ sq' βŸ©β‰‘Λ˜
               h ∘ l ∘ p     ∎

We want to show that for which it will suffice for to be an epimorphism. Since we’re working in a regular category, we can show that is a strong epimorphism by showing that is a composite of strong epis. But is the composite and both of those maps are pullbacks of which is a strong epimorphism since it arises from an image factorisation.

This <details> tag contains the proof that and are pullbacks of You may choose to unfold or skip it.
        open is-pullback

        remβ‚‚ : is-strong-epi π’ž (Γ—-functor .F₁ (d , id))
        remβ‚‚ = r.stable d π₁ {p2 = π₁} (out! dgh.mediate∈E) Ξ» where
          .square β†’ Ο€β‚βˆ˜βŸ¨βŸ©
          .universal {p₁' = p₁'} {pβ‚‚'} p β†’ ⟨ pβ‚‚' , Ο€β‚‚ ∘ p₁' ⟩
          .pβ‚βˆ˜universal {p₁' = p₁'} {pβ‚‚'} {p = p} β†’ ⟨⟩∘ _
            Β·Β· apβ‚‚ ⟨_,_⟩ (pullr Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ sym p) (pullr Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ idl _)
            ·· sym (⟨⟩-unique _ refl refl)
          .pβ‚‚βˆ˜universal β†’ Ο€β‚βˆ˜βŸ¨βŸ©
          .unique {p = p} {lim'} q r β†’ ⟨⟩-unique _ r $ sym $
            ap (Ο€β‚‚ ∘_) (sym q) βˆ™ pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ ap (_∘ lim') (idl _)

        rem₃ : is-strong-epi π’ž (Γ—-functor .F₁ (id , d))
        rem₃ = r.stable d Ο€β‚‚ {p2 = Ο€β‚‚} (out! dgh.mediate∈E) Ξ» where
          .square β†’ Ο€β‚‚βˆ˜βŸ¨βŸ©
          .universal {p₁' = p₁'} {pβ‚‚'} p β†’ ⟨ π₁ ∘ p₁' , pβ‚‚' ⟩
          .pβ‚βˆ˜universal {p = p} β†’ ⟨⟩∘ _
            Β·Β· apβ‚‚ ⟨_,_⟩ (pullr Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ idl _) (pullr Ο€β‚‚βˆ˜βŸ¨βŸ©)
            ·· sym (⟨⟩-unique _ refl p)
          .pβ‚‚βˆ˜universal β†’ Ο€β‚‚βˆ˜βŸ¨βŸ©
          .unique {p = p} {lim'} q r β†’ ⟨⟩-unique _
            (sym (ap (π₁ ∘_) (sym q) βˆ™ pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ ap (_∘ lim') (idl _)))
            r

        remβ‚„ = sym (Γ—-functor .F-∘ _ _)
             βˆ™ ap (Γ—-functor .F₁) (Ξ£-pathp (idl _) (idr _))

So is a strong epimorphism by the above remarks, and is a pullback of so it is also strong epic (rem₆); We obtain (rem₇). By pushing some symbols, this gives (remβ‚ˆ), but is a monomorphism by construction, so β€” so is also monic.

        remβ‚… : is-strong-epi π’ž dΓ—d
        remβ‚… = subst (is-strong-epi π’ž) remβ‚„ (strong-epi-compose π’ž _ _ remβ‚‚ rem₃)

        rem₆ : is-strong-epi π’ž p
        rem₆ = r.stable _ _ remβ‚… pb.has-is-pb

        rem₇ : h ∘ k ≑ h ∘ l
        rem₇ = rem₆ .fst _ _ $
          (h ∘ k) ∘ p   β‰‘βŸ¨ sym (assoc _ _ _) βˆ™ rem₁ βŸ©β‰‘
          h ∘ l ∘ p     β‰‘βŸ¨ pulll refl βŸ©β‰‘
          (h ∘ l) ∘ p   ∎

        remβ‚ˆ : gh C.∘ k ≑ gh C.∘ l
        remβ‚ˆ =
          gh ∘ k              β‰‘βŸ¨ ⟨⟩-unique _ refl refl ⟩∘⟨refl βŸ©β‰‘
          ⟨ g , h ⟩ ∘ k       β‰‘βŸ¨ ⟨⟩∘ _ βŸ©β‰‘
          ⟨ g ∘ k , h ∘ k ⟩   β‰‘βŸ¨ apβ‚‚ ⟨_,_⟩ w' rem₇ βŸ©β‰‘
          ⟨ g ∘ l , h ∘ l ⟩   β‰‘Λ˜βŸ¨ ⟨⟩∘ _ βŸ©β‰‘Λ˜
          ⟨ g , h ⟩ ∘ l       β‰‘Λ˜βŸ¨ ⟨⟩-unique _ refl refl ⟩∘⟨refl βŸ©β‰‘Λ˜
          gh ∘ l              ∎

Having shown that is monic, and knowing that β€” a strong (thus extremal) epimorphism β€” factors through it, we conclude that is an isomorphism. It remains to compute that which we do below.

      compute =
        (h ∘ g.from) ∘ f                           β‰‘βŸ¨ pullr refl βˆ™ pullr refl βŸ©β‰‘
        Ο€β‚‚ ∘ dgh.gh ∘ g.from ∘ f                   β‰‘βŸ¨ refl ⟩∘⟨ ⟨⟩-unique _ refl refl ⟩∘⟨ refl βŸ©β‰‘
        Ο€β‚‚ ∘ ⟨ g , h ⟩ ∘ g.from ∘ f                β‰‘βŸ¨ refl⟩∘⟨ ⟨⟩∘ _ βŸ©β‰‘
        Ο€β‚‚ ∘ ⟨ g ∘ g.from ∘ f , h ∘ g.from ∘ f ⟩   β‰‘βŸ¨ Ο€β‚‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
        h ∘ g.from ∘ f                             β‰‘βŸ¨ refl⟩∘⟨ g-ortho.p .centre .snd .fst βŸ©β‰‘
        h ∘ dgh.d                                  β‰‘βŸ¨ pullr (sym dgh.factors) βŸ©β‰‘
        Ο€β‚‚ ∘ ⟨ f , c ⟩                             β‰‘βŸ¨ Ο€β‚‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
        c                                          ∎

This proves that an arbitrary strong epi, coequalises its kernel pair. It’s an effective epimorphism! So it’s definitely the case that it coequalises some pair of maps.

    open is-regular-epi renaming (r to Kp)
    open is-coequaliser
    is-strong-epiβ†’is-regular-epi : is-regular-epi π’ž f
    is-strong-epi→is-regular-epi = go where
      go : is-regular-epi π’ž f
      go .Kp = kp.R
      go .arr₁ = kp.a
      go .arrβ‚‚ = kp.b
      go .has-is-coeq .coequal = kp.square
      go .has-is-coeq .universal w = Make.h w ∘ Make.g.from w
      go .has-is-coeq .factors {e' = e'} {p = w} = Make.compute w
      go .has-is-coeq .unique {e' = e'} {p = p} {colim} q = is-s .fst _ _ $
        colim ∘ f                      β‰‘βŸ¨ q βŸ©β‰‘
        e'                             β‰‘Λ˜βŸ¨ Make.compute p βŸ©β‰‘Λ˜
        (Make.h p ∘ Make.g.from p) ∘ f ∎

  1. Note: Johnstone prefers to work with β€œcovers” instead, which in our lingo are extremal epimorphisms. In a finitely complete category, strong and extremal epimorphisms coincideβ†©οΈŽ

  2. Johnstone says it’s clearly unique, but the tiny calculation is included at the end of the proof since it wasn’t clear to meβ†©οΈŽ


References

  • Johnstone, Peter T. 2002. Sketches of an Elephant: a Topos Theory Compendium. Oxford Logic Guides. New York, NY: Oxford Univ. Press. https://cds.cern.ch/record/592033.