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

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$^{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.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

If you care, $r$ is for “relation” — the intution 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.