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 1) (mm .monic _ _ (sym (q β sym (lift-it mm sq .snd .snd)))) }

abstract is-strong-epi-is-prop : β {a b} (f : Hom a b) β is-prop (is-strong-epi f) is-strong-epi-is-prop f = hlevel!

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 }))

# Regular epis are strongπ

Suppose that $f : a \to b$ is 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β as the definition of βwell-behaved epimorphismβ, weβd certainly like regular epis 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$^{1}, 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.factors , 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.universal {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.factors))

# 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 = \operatorname{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.universal uf=vf (w , p , q) = ls (record { monic = is-equaliserβis-monic C _ ker.has-is-eq }) {u = k} {v = id} (idl _ β sym ker.factors) 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

## Extremal epimorphismsπ

Another well-behaved subclass of epimorphism are the
**extremal** epimorphisms: An epimorphism
$e : A \twoheadrightarrow B$
is extremal if when, given a factorisation
$e = mg$
through a monomorphism
$m : C \hookrightarrow B$,
then
$m$
is an isomorphism. In a finitely
complete category, every extremal epimorphism is strong; the
converse is immediate.

is-extremal-epiβis-strong-epi : β {a b} {e : Hom a b} β Finitely-complete C β (β {c} (m : c βͺ b) (g : Hom a c) β e β‘ m .mor β g β is-invertible (m .mor)) β is-strong-epi e is-extremal-epiβis-strong-epi {a} {b} {e} lex extremal = equaliser-liftsβis-strong-epi lex.equalisers Ξ» w β Mk.the-lift w where module lex = Finitely-complete lex

We adapt the proof from [Borceux (1994); Β§4.3.7]. After
`equaliser-liftsβis-strong-epi`

,
it will suffice to construct *some* lift for a square with
$ve = mu$,
with
$m$
monic. Pull
$v$
back along
$m$
to obtain the square

and obtain the unique factorisation $A \to A \times_D B$. Note that the map $u : A \times_D B \hookrightarrow B$ is a monomorphism since it results from pulling back a monomorphism.

module Mk {c d : Ob} (m : c βͺ d) {u : Hom a c} {v : Hom b d} (wit : v β e β‘ m .mor β u) where module P = Pullback (lex.pullbacks v (m .mor)) renaming (pβ to q ; pβ to p) r : Hom a P.apex r = P.universal {pβ' = e} {pβ' = u} wit abstract q-mono : is-monic P.q q-mono = is-monicβpullback-is-monic (m .monic) (rotate-pullback P.has-is-pb)

We thus have a factorisation $e = qr$ of $e$ through a monomorphism $q$, which since $e$ was assumed extremal, must be an isomorphism. We define the diagonal map $b \to c$ to be $pq^{-1}$ and compute that it commutes appropriately:

q-iso : is-invertible P.q q-iso = extremal record{ monic = q-mono } r (sym P.pββuniversal) qβ»ΒΉ = q-iso .is-invertible.inv the-lift : Ξ£ (Hom b c) Ξ» w β (w β e β‘ u) Γ (m .mor β w β‘ v) the-lift .fst = P.p β qβ»ΒΉ the-lift .snd .fst = m .monic _ _ $ m .mor β (P.p β qβ»ΒΉ) β e β‘β¨ extendl (pulll (sym P.square)) β©β‘ (v β P.q) β qβ»ΒΉ β e β‘β¨ cancel-inner (q-iso .is-invertible.invl) β©β‘ v β e β‘β¨ wit β©β‘ m .mor β u β the-lift .snd .snd = invertibleβepic q-iso _ _ $ (m .mor β (P.p β qβ»ΒΉ)) β P.q β‘β¨ pullr (cancelr (q-iso .is-invertible.invr)) β©β‘ m .mor β P.p β‘Λβ¨ P.square β©β‘Λ v β P.q β

is-strong-epiβis-extremal-epi : β {a b} {e : Hom a b} β is-strong-epi e β β {c} (m : c βͺ b) (g : Hom a c) β e β‘ m .mor β g β is-invertible (m .mor) is-strong-epiβis-extremal-epi (s , ortho) m g p = make-invertible (invβ² .centre .fst) (invβ² .centre .snd .snd) (m .monic _ _ (pulll (invβ² .centre .snd .snd) β id-comm-sym)) where invβ² = ortho m (idl _ β p)

If you care, $r$ is for βrelationβ β the intuition is that $r$ specifies the

*relations*imposed on $a$ to get $b$β©οΈ

## References

- Borceux, Francis. 1994.
*Handbook of Categorical Algebra*. Vol. 1. Encyclopedia of Mathematics and Its Applications. Cambridge University Press. https://doi.org/10.1017/CBO9780511525858.