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 ↠ b$ to be a strong epimorphism means that, given $g : c ↪ 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!
    (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 $α,$ $β,$ as in

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

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 $v f g = z u$ commutative “square”), we get an intermediate lift $w : b \to d$ such that $w g = u$ and $z w = v f$ — 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 $t f = w$ and $z t = v .$ A quick calculation, implicit in the diagram, shows that $t$ is precisely the lift for $f g$ 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 $g f$ 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 $z w = v f$ to lift $f$ against $z .$ We don’t have a $u$ as before, but we can take $u = w g$ 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$ ¹, and that $z : c ↪ 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 $u s = u t .$ Since $z$ is a mono, it’ll suffice to show that $z u s = z u t,$ but note that $z u = v f$ since the square commutes. Then we have

z u s = v f s = v f t = z u t,

so there is a map $m : b \to c$ such that $m f = u$ — that’s commutativity of the top triangle handled. For the bottom triangle, since $f$ is a regular epic (thus an epic), to show $z m = v,$ it’ll suffice to show that $z m f = v f .$ But $v f = z u$ by assumption, and $m f = 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 $im (f) ↪ 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 \tilde{f} im (f) ↪ b,

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 ↠ 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 = ext (idr _ ∙ sym (the-lifting .centre .snd .fst))

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

In the lex case🔗

Suppose that $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 $f g = id,$ then $f$ is an epimorphism. You can think of this as a special case of “ $f g$ 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 $u f = v f$ 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 $u f = v f,$ there’s a unique map $k : a \to Eq (u, v)$ such that $e k = 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, $e w = 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 _ 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 $u e = v e,$ 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 ↠ B$ is extremal if when, given a factorisation $e = m g$ through a monomorphism $m : C ↪ 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 $v e = m u,$ 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 ↪ 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 = q r$ 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 $p q^{- 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                      ∎

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.