module Cat.Diagram.Coequaliser.RegularEpi where

Regular epimorphismsπŸ”—

Dually to regular monomorphisms, which behave as embeddings, regular epimorphisms behave like covers: A regular epimorphism expresses as β€œa union of parts of possibly glued together”.

The definition is also precisely dual: A map is a regular epimorphism if it is the coequaliser of some pair of arrows

  record is-regular-epi (f : Hom a b) : Type (o βŠ” β„“) where
    no-eta-equality
    constructor reg-epi
    field
      {r}           : Ob
      {arr₁} {arrβ‚‚} : Hom r a
      has-is-coeq   : is-coequaliser C arr₁ arrβ‚‚ f

    open is-coequaliser has-is-coeq public

From the definition we can directly conclude that regular epis are in fact epic:

    is-regular-epi→is-epic : is-epic f
    is-regular-epi→is-epic = is-coequaliser→is-epic _ has-is-coeq

  open is-regular-epi using (is-regular-epi→is-epic) public

Effective episπŸ”—

Again by duality, we have a pair of canonical choices of maps which may coequalise: Its kernel pair, that is, the pullback of along itself. An epimorphism which coequalises its kernel pair is called an effective epi, and effective epis are immediately seen to be regular epis:

  record is-effective-epi (f : Hom a b) : Type (o βŠ” β„“) where
    no-eta-equality
    field
      {kernel}       : Ob
      p₁ pβ‚‚          : Hom kernel a
      has-kernel-pair : is-kernel-pair C p₁ pβ‚‚ f
      has-is-coeq    : is-coequaliser C p₁ pβ‚‚ f

    is-effective-epi→is-regular-epi : is-regular-epi f
    is-effective-epi→is-regular-epi = re where
      open is-regular-epi hiding (has-is-coeq)
      re : is-regular-epi f
      re .r = _
      re .arr₁ = _
      re .arrβ‚‚ = _
      re .is-regular-epi.has-is-coeq = has-is-coeq

If a regular epimorphism (a coequaliser) has a kernel pair, then it is also the coequaliser of its kernel pair. That is: If the pullback of exists, then is also an effective epimorphism.

  is-regular-epi→is-effective-epi
    : βˆ€ {a b} {f : Hom a b}
    β†’ Pullback C f f
    β†’ is-regular-epi C f
    β†’ is-effective-epi C f
  is-regular-epi→is-effective-epi {f = f} kp reg = epi where
    module reg = is-regular-epi reg
    module kp = Pullback kp

    open is-effective-epi
    open is-coequaliser
    epi : is-effective-epi C f
    epi .kernel = kp.apex
    epi .p₁ = kp.p₁
    epi .pβ‚‚ = kp.pβ‚‚
    epi .has-kernel-pair = kp.has-is-pb
    epi .has-is-coeq .coequal = kp.square
    epi .has-is-coeq .universal {F = F} {e'} p = reg.universal q where
      q : e' ∘ reg.arr₁ ≑ e' ∘ reg.arrβ‚‚
      q =
        e' ∘ reg.arr₁                               β‰‘βŸ¨ ap (e' ∘_) (sym kp.pβ‚‚βˆ˜universal) βŸ©β‰‘
        e' ∘ kp.pβ‚‚ ∘ kp.universal (sym reg.coequal)  β‰‘βŸ¨ pulll (sym p) βŸ©β‰‘
        (e' ∘ kp.p₁) ∘ kp.universal _                β‰‘βŸ¨ pullr kp.pβ‚βˆ˜universal βŸ©β‰‘
        e' ∘ reg.arrβ‚‚                               ∎
    epi .has-is-coeq .factors = reg.factors
    epi .has-is-coeq .unique = reg.unique

Existence of regular episπŸ”—

Let be a categories such that has coproducts indexed by the objects and arrows of and let be a functor with a colimit in The canonical map is a regular epimorphism

module _ {o β„“ oj β„“j}
  {C : Precategory o β„“} {J : Precategory oj β„“j}
  {F : Functor J C}
  (∐Ob : has-coproducts-indexed-by C ⌞ J ⌟)
  (∐Hom : has-coproducts-indexed-by C (Arrows J))
  (∐F : Colimit F)
  where
  indexed-coproductβ†’regular-epi : is-regular-epi C (∐Ob.match F.β‚€ ∐F.ψ)

We start by constructing a pair of maps via the universal property of

  indexed-coproductβ†’regular-epi .r = ∐Hom.Ξ£F Ξ» (i , j , f) β†’ F.β‚€ i
  indexed-coproductβ†’regular-epi .arr₁ = ∐Hom.match _ Ξ» (i , j , f) β†’ ∐Ob.ΞΉ F.β‚€ j C.∘ F.₁ f
  indexed-coproductβ†’regular-epi .arrβ‚‚ = ∐Hom.match _ Ξ» (i , j , f) β†’ ∐Ob.ΞΉ F.β‚€ i

By some rather tedious calculations, we can show that and coequalize

  indexed-coproduct→regular-epi .has-is-coeq .coequal =
    ∐Hom.uniqueβ‚‚ _ Ξ» (i , j , f) β†’
    (∐Ob.match F.β‚€ ∐F.ψ C.∘ ∐Hom.match _ _) C.∘ ∐Hom.ΞΉ _ (i , j , f) β‰‘βŸ¨ C.pullr (∐Hom.commute _) βŸ©β‰‘
    ∐Ob.match F.β‚€ ∐F.ψ C.∘ ∐Ob.ΞΉ _ j C.∘ F.₁ f                       β‰‘βŸ¨ C.pulll (∐Ob.commute _) βŸ©β‰‘
    ∐F.ψ j C.∘ F.₁ f                                                 β‰‘βŸ¨ ∐F.commutes f βŸ©β‰‘
    ∐F.ψ i                                                           β‰‘Λ˜βŸ¨ ∐Ob.commute _ βŸ©β‰‘Λ˜
    ∐Ob.match F.β‚€ ∐F.ψ C.∘ ∐Ob.ΞΉ _ i                                 β‰‘Λ˜βŸ¨ C.pullr (∐Hom.commute _) βŸ©β‰‘Λ˜
    (∐Ob.match F.β‚€ ∐F.ψ C.∘ ∐Hom.match _ _) C.∘ ∐Hom.ΞΉ _ (i , j , f) ∎

Moreover, and form the universal such coequalizing pair. This follows by yet more brute-force calculation.

  indexed-coproduct→regular-epi .has-is-coeq .universal {e' = e'} p =
    ∐F.universal (Ξ» j β†’ e' C.∘ ∐Ob.ΞΉ F.β‚€ j) comm
    where abstract
      comm
        : βˆ€ {i j} (f : J.Hom i j)
        β†’ (e' C.∘ ∐Ob.ΞΉ F.β‚€ j) C.∘ F.₁ f ≑ e' C.∘ ∐Ob.ΞΉ F.β‚€ i
      comm {i} {j} f =
        (e' C.∘ ∐Ob.ΞΉ F.β‚€ j) C.∘ F.₁ f                   β‰‘βŸ¨ C.pullr (sym (∐Hom.commute _)) βŸ©β‰‘
        e' C.∘ (∐Hom.match _ _ C.∘ ∐Hom.ΞΉ _ (i , j , f)) β‰‘βŸ¨ C.extendl p βŸ©β‰‘
        e' C.∘ (∐Hom.match _ _ C.∘ ∐Hom.ΞΉ _ (i , j , f)) β‰‘βŸ¨ apβ‚‚ C._∘_ refl (∐Hom.commute _) βŸ©β‰‘
        e' C.∘ ∐Ob.ΞΉ F.β‚€ i                               ∎
  indexed-coproduct→regular-epi .has-is-coeq .factors {e' = e'} {p = p} =
    ∐Ob.uniqueβ‚‚ F.β‚€ Ξ» j β†’
      (∐F.universal _ _ C.∘ ∐Ob.match F.β‚€ ∐F.ψ) C.∘ ∐Ob.ΞΉ F.β‚€ j β‰‘βŸ¨ C.pullr (∐Ob.commute _) βŸ©β‰‘
      ∐F.universal _ _ C.∘ ∐F.ψ j                               β‰‘βŸ¨ ∐F.factors _ _ βŸ©β‰‘
      e' C.∘ ∐Ob.ΞΉ F.β‚€ j                                        ∎
  indexed-coproduct→regular-epi .has-is-coeq .unique {e' = e'} {colim = h} p =
    ∐F.unique _ _ _ Ξ» j β†’
      h C.∘ ∐F.ψ j                               β‰‘Λ˜βŸ¨ apβ‚‚ C._∘_ refl (∐Ob.commute _) βŸ©β‰‘Λ˜
      h C.∘ (∐Ob.match F.β‚€ ∐F.ψ C.∘ ∐Ob.ΞΉ F.β‚€ j) β‰‘βŸ¨ C.pulll p βŸ©β‰‘
      e' C.∘ ∐Ob.ΞΉ F.β‚€ j                         ∎