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↠bf : a \twoheadrightarrow b to be a strong epimorphism means that, given g:c↪bg : c \hookrightarrow b any mono, and uu, vv arbitrarily fit into a commutative diagram like

there is a contractible space of maps b→cb \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)

  : ∀ {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 gg is a monomorphism, it suffices to have gα=gβg\alpha = g\beta, but by commutativity of the lower triangles we have gα=u=gβg\alpha = u = g\beta.


The proofs here are transcribed from (Borceux 1994, vol. 1, sec. 4.3). Strong epimorphisms are closed under composition, for suppose that ff and gg are strong epics, and mm 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=zuvfg = zu commutative “square”), we get an intermediate lift w:b→dw : b \to d such that wg=uwg = u and zw=vfzw=vf — such that zz, ww, ff, and vv organise into the faces of a lifting diagram, too$ Since ff is a strong epic, we have a second lift t:c→dt : c \to d, now satisfying tf=wtf=w and zt=vzt=v. A quick calculation, implicit in the diagram, shows that tt is precisely the lift for fgfg against zz.

  : ∀ {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
  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 =
      (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 gfgf is a strong epi, then gg is, too! Still thinking of the same diagram, suppose the whole diagram is a strong epi, and you’re given zw=vfzw = vf to lift ff against zz. We don’t have a uu as before, but we can take u=wgu = wg to get a lift tt.

  : ∀ {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.

  : ∀ {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→bf : a \to b is a regular epimorphism, that is, it identifies bb as some quotient of aa — the stuff of bb is that of aa, 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→bf : a \to b is the coequaliser of some maps s,t:r→as, t : r \to a1, and that z:c↪bz : c \hookrightarrow b is a monomorphism we want to lift against.

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

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

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

  : ∀ {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 =
    (λ m x → map m x , r.factors , lemma m x)
    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 =→is-epic _ _ $
        sym (vf=zu ∙ pushr (sym r.factors))


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→bf : a \to b is a monomorphism im⁡(f)↪b\operatorname*{im}(f) \hookrightarrow b which is universal amongst those through which ff 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→bf : a \to b as

a↠f˜im⁡(f)↪b, a \xtwoheadrightarrow{\~f} \operatorname*{im}(f) \hookrightarrow b\text{,}

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

  : ∀ {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)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 =
        (record { monic = o.y .witness })
        {u = .map}
        {v = im→b} (sym ( .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 C\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 ff is such that there exists a gg with fg=id⁡fg = \operatorname{id}_{}, then ff is an epimorphism. You can think of this as a special case of “fgfg epic implies ff epic” or as a short calculation:

  : ∀ {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,vu, v and uf=vfuf = vf to lift against, form their equaliser Eq(u,v)Eq(u,v) and arrange them like

  : ∀ {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)Eq(u,v), since there’s uf=vfuf = vf, there’s a unique map k:a→Eq(u,v)k : a \to Eq(u,v) such that ek=fek = f. Arranging kk, ff, ee and the identity(!) into a lifting square like the one above, we conclude the existence of a dotted map ww satisfying, most importantly, ew=idew = \mathrm{id} — so that ee, being a retract, is an epimorphism.

  epi : is-epic f
  epi u v uf=vf =
      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)→Be : Eq(u,v) \to B is the universal map which equalises uu and vv — so that we have ue=veue = ve, and since we’ve just shown that ee is epic, this means we have u=vu = 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↠Be : A \twoheadrightarrow B is extremal if when, given a factorisation e=mge = mg through a monomorphism m:C↪Bm : C \hookrightarrow B, then mm is an isomorphism. In a finitely complete category, every extremal epimorphism is strong; the converse is immediate.

  : ∀ {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=muve = mu, with mm monic. Pull vv back along mm to obtain the square

and obtain the unique factorisation A→A×DBA \to A \times_D B. Note that the map u:A×DB↪Bu : 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

        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=qre = qr of ee through a monomorphism qq, which since ee was assumed extremal, must be an isomorphism. We define the diagonal map b→cb \to c to be pq−1pq^{-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                      ∎

  1. If you care, rr is for “relation” — the intuition is that rr specifies the relations imposed on aa to get bb↩︎