module Cat.Morphism.StrongEpi {o ℓ} (C : Precategory o ℓ) where

open Cat.Reasoning C

A strong epimorphism is an epimorphism which is, additionally, left orthogonal to every monomorphism. Unfolding that definition, for $f : a {\twoheadrightarrow}b$ to be a strong epimorphism means that, given $g : c {\hookrightarrow}b$ any mono, and $u$, $v$ arbitrarily fit into a commutative diagram like

there is a contractible space of maps $b \to c$ which make the two triangles commute. In the particular case of strong epimorphisms, it actually suffices to have any lift: they are automatically unique.

is-strong-epi : ∀ {a b} → Hom a b → Type _
is-strong-epi f = is-epic f × ∀ {c d} (m : c ↪ d) → m⊥m C f (m .mor)

lifts→is-strong-epi
  : ∀ {a b} {f : Hom a b}
  → is-epic f
  → ( ∀ {c d} (m : c ↪ d) {u} {v} → v ∘ f ≡ m .mor ∘ u
    → Σ[ w ∈ Hom b c ] ((w ∘ f ≡ u) × (m .mor ∘ w ≡ v)))
  → is-strong-epi f
lifts→is-strong-epi epic lift-it = epic , λ {c} {d} mm sq →
  contr (lift-it mm sq) λ { (x , p , q) → Σ-prop-path (λ _ → hlevel )
    (mm .monic _ _ (sym (q ∙ sym (lift-it mm sq .snd .snd)))) }

To see that the uniqueness needed for orthogonality against a monomorphism is redundant, suppose you’d had two fillers $\alpha$, $\beta$, as in

Since $g$ is a monomorphism, it suffices to have $g\alpha = g\beta$, but by commutativity of the lower triangles we have $g\alpha = u = g\beta$.

Properties🔗

The proofs here are transcribed from (Borceux 1994, vol. 1, sec. 4.3). Strong epimorphisms are closed under composition, for suppose that $f$ and $g$ are strong epics, and $m$ is the monomorphism to lift against. Fit them in a skewed commutative rectangle like

By considering most of the right half as a single, weirdly-shaped square (the $vfg = zu$ commutative “square”), we get an intermediate lift $w : b \to d$ such that $wg = u$ and $zw=vf$ — such that $z$, $w$, $f$, and $v$ organise into the faces of a lifting diagram, too$ Since $f$ is a strong epic, we have a second lift $t : c \to d$, now satisfying $tf=w$ and $zt=v$. A quick calculation, implicit in the diagram, shows that $t$ is precisely the lift for $fg$ against $z$.

strong-epi-compose
  : ∀ {a b c} (g : Hom a b) (f : Hom b c)
  → is-strong-epi g
  → is-strong-epi f
  → is-strong-epi (f ∘ g)
strong-epi-compose g f (g-e , g-s) (f-e , f-s) =
  lifts→is-strong-epi epi fg-s
  where
  epi : is-epic (f ∘ g)
  epi α β p = f-e α β $ g-e (α ∘ f) (β ∘ f) $
    sym (assoc _ _ _) ·· p ·· assoc _ _ _
  fg-s : ∀ {c d} (m : c ↪ d) {u v} → v ∘ f ∘ g ≡ m .mor ∘ u → _
  fg-s z {u} {v} vfg=zu =
    let
      (w , wg=u , zw=vf) = g-s z (sym (assoc _ _ _) ∙ vfg=zu) .centre
      (t , tf=w , zt=v)  = f-s z (sym zw=vf) .centre
    in t , pulll tf=w ∙ wg=u , zt=v

Additionally, there is a partial converse to this result: If the composite $gf$ is a strong epi, then $g$ is, too! Still thinking of the same diagram, suppose the whole diagram is a strong epi, and you’re given $zw = vf$ to lift $f$ against $z$. We don’t have a $u$ as before, but we can take $u = wg$ to get a lift $t$.

strong-epi-cancel-l
  : ∀ {a b c} (f : Hom b c) (g : Hom a b)
  → is-strong-epi (f ∘ g)
  → is-strong-epi f
strong-epi-cancel-l g f (gf-epi , gf-str) = lifts→is-strong-epi epi lifts where
  epi : is-epic g
  epi α β p = gf-epi α β (extendl p)

  lifts : ∀ {c d} (m : c ↪ d) {u} {v} → v ∘ g ≡ m .mor ∘ u → _
  lifts {α} {β} mm {u} {v} sq = lifted .fst , lemma , lifted .snd .snd where
    lifted = gf-str mm {u = u ∘ f} {v = v} (extendl sq) .centre
    lemma = mm .monic _ _ (pulll (lifted .snd .snd) ∙ sq)

As an immediate consequence of the definition, a monic strong epi is an isomorphism. This is because, being left orthogonal to all monos, it’d be, in particular, left orthogonal to itself, and the only self-orthogonal maps are isos.

strong-epi-mono→is-invertible
  : ∀ {a b} {f : Hom a b} → is-monic f → is-strong-epi f → is-invertible f
strong-epi-mono→is-invertible mono (_ , epi) =
  self-orthogonal→is-iso C _ (epi (record { monic = mono }))

Covers are strong🔗

Suppose that $f : a \to b$ is a cover (better known as a regular epimorphism), that is, it identifies $b$ as some quotient of $a$ — the stuff of $b$ is that of $a$, but with new potential identifications thrown in. Since we’re taking “strong epimorphism” to mean “well-behaved epimorphism”, we’d certainly like covers to be strong epis!

This is fortunately the case. Suppose that $f : a \to b$ is the coequaliser of some maps $s, t : r \to a$¹, and that $z : c {\hookrightarrow}b$ is a monomorphism we want to lift against.

By the universal property of a coequaliser, to “slide $u$ over” to a map $b \to c$, it suffices to show that it also coequalises the pair $s, t$, i.e. that $us = ut$. Since $z$ is a mono, it’ll suffice to show that $zus = zut$, but note that $zu = vf$ since the square commutes. Then we have

$$zus = vfs = vft = zut{\text{,}}$$

so there is a map $m : b \to c$ such that $mf = u$ — that’s commutativity of the top triangle handled. For the bottom triangle, since $f$ is a regular epic (thus an epic), to show $zm = v$, it’ll suffice to show that $zmf = vf$. But $vf = zu$ by assumption, and $mf = u$ by the universal property! We’re done.

is-regular-epi→is-strong-epi
  : ∀ {a b} (f : Hom a b)
  → is-regular-epi C f
  → is-strong-epi f
is-regular-epi→is-strong-epi {a} {b} f regular =
  lifts→is-strong-epi
    r.is-regular-epi→is-epic
    (λ m x → map m x , r.universal , lemma m x)
    where
    module r = is-regular-epi regular renaming (arr₁ to s ; arr₂ to t)
    module _ {c} {d} (z : c ↪ d) {u} {v} (vf=zu : v ∘ f ≡ z .mor ∘ u) where
      module z = _↪_ z
      map : Hom b c
      map = r.coequalise {e′ = u} $ z.monic _ _ $
        z .mor ∘ u ∘ r.s ≡⟨ extendl (sym vf=zu) ⟩≡
        v ∘ f ∘ r.s      ≡⟨ refl⟩∘⟨ r.coequal ⟩≡
        v ∘ f ∘ r.t      ≡˘⟨ extendl (sym vf=zu) ⟩≡˘
        z .mor ∘ u ∘ r.t ∎
      lemma = r.is-regular-epi→is-epic _ _ $
        sym (vf=zu ∙ pushr (sym r.universal))

Images🔗

Now we come to the raison d’être for strong epimorphisms: Images. The definition of image we use is very complicated, and the justification is already present there, but the short of it is that the image of a morphism $f : a \to b$ is a monomorphism $\operatorname*{im}(f) {\hookrightarrow}b$ which is universal amongst those through which $f$ factors.

Since images have a universal property, and one involving comma categories of slice categories at that, they are tricky to come by. However, in the case where we factor $f : a \to b$ as

$$a {\xtwoheadrightarrow{\~f}} \operatorname*{im}(f) {\hookrightarrow}b\text{,}$$

and the epimorphism is strong, then we automatically have an image factorisation of $f$ on our hands!

strong-epi-mono→image
  : ∀ {a b im} (f : Hom a b)
  → (a→im : Hom a im) → is-strong-epi a→im
  → (im→b : Hom im b) → is-monic im→b
  → im→b ∘ a→im ≡ f
  → Image C f
strong-epi-mono→image f a→im (_ , str-epi) im→b mono fact = go where
  open Initial
  open /-Obj
  open /-Hom
  open ↓Obj
  open ↓Hom

  obj : ↓Obj (Const (cut f)) (Forget-full-subcat {P = is-monic ⊙ map})
  obj .x = tt
  obj .y = restrict (cut im→b) mono
  obj .map = record { map = a→im ; commutes = fact }

Actually, for an image factorisation, we don’t need that $a {\twoheadrightarrow}\operatorname*{im}(f)$ be an epimorphism — we just need it to be orthogonal to every monomorphism. This turns out to be precisely the data of being initial in the relevant comma categories.

  go : Image C f
  go .bot = obj
  go .has⊥ other = contr dh unique where
    module o = ↓Obj other

    the-lifting =
      str-epi
        (record { monic = o.y .witness })
        {u = o.map .map}
        {v = im→b} (sym (o.map .commutes ∙ sym fact))

    dh : ↓Hom (Const (cut f)) _ obj other
    dh .α = tt
    dh .β .map = the-lifting .centre .fst
    dh .β .commutes = the-lifting .centre .snd .snd
    dh .sq = /-Hom-path (idr _ ∙ sym (the-lifting .centre .snd .fst))

    unique : ∀ om → dh ≡ om
    unique om = ↓Hom-path _ _ refl $ /-Hom-path $ ap fst $ the-lifting .paths $
      om .β .map , sym (ap map (om .sq)) ∙ idr _ , om .β .commutes

In the lex case🔗

Suppose that $\mathcal{C}$ is additionally left exact, or more restrictively, that it has all equalisers. In that case, a map left orthogonal to all monomorphisms is automatically an epimorphism, thus a strong epi. Let’s see how. First, there’s a quick observation to be made about epimorphisms: if $f$ is such that there exists a $g$ with $fg = {{\mathrm{id}}_{}}$, then $f$ is an epimorphism. You can think of this as a special case of “$fg$ epic implies $f$ epic” or as a short calculation:

retract-is-epi
  : ∀ {a b} {f : Hom a b} {g : Hom b a}
  → f ∘ g ≡ id
  → is-epic f
retract-is-epi {f = f} {g} p α β q =
  α         ≡⟨ intror p ⟩≡
  α ∘ f ∘ g ≡⟨ extendl q ⟩≡
  β ∘ f ∘ g ≡⟨ elimr p ⟩≡
  β         ∎

We already know that if lifts exist and the map is epic, then it’s a strong epi, so let’s assume that lifts exist — we’ll have no need for uniqueness, here. Given $u, v$ and $uf = vf$ to lift against, form their equaliser $Eq(u,v)$ and arrange them like

equaliser-lifts→is-strong-epi
  : ∀ {a b} {f : Hom a b}
  → (∀ {a b} (f g : Hom a b) → Equaliser C f g)
  → ( ∀ {c d} (m : c ↪ d) {u} {v} → v ∘ f ≡ m .mor ∘ u
    → Σ[ w ∈ Hom b c ] ((w ∘ f ≡ u) × (m .mor ∘ w ≡ v)))
  → is-strong-epi f
equaliser-lifts→is-strong-epi {f = f} eqs ls = lifts→is-strong-epi epi ls where

By the universal property of $Eq(u,v)$, since there’s $uf = vf$, there’s a unique map $k : a \to Eq(u,v)$ such that $ek = f$. Arranging $k$, $f$, $e$ and the identity(!) into a lifting square like the one above, we conclude the existence of a dotted map $w$ satisfying, most importantly, $ew = \mathrm{id}$ — so that $e$, being a retract, is an epimorphism.

  epi : is-epic f
  epi u v uf=vf =
    let
      module ker = Equaliser (eqs u v)
      k = ker.limiting uf=vf
      (w , p , q) = ls
        (record { monic = is-equaliser→is-monic C _ ker.has-is-eq })
        {u = k} {v = id}
        (idl _ ∙ sym ker.universal)
      e-epi : is-epic ker.equ
      e-epi = retract-is-epi q

Now, $e : Eq(u,v) \to B$ is the universal map which equalises $u$ and $v$ — so that we have $ue = ve$, and since we’ve just shown that $e$ is epic, this means we have $u = v$ — exactly what we wanted!

    in e-epi u v ker.equal