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 to be a strong epimorphism means that, given any mono, and , arbitrarily fit into a commutative diagram like
there is a contractible space of maps 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 , , as in
Since is a monomorphism, it suffices to have , but by commutativity of the lower triangles we have .
Properties🔗
The proofs here are transcribed from (Borceux 1994, vol. 1, sec. 4.3). Strong epimorphisms are closed under composition, for suppose that and are strong epics, and 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 commutative “square”), we get an intermediate lift such that and — such that , , , and organise into the faces of a lifting diagram, too$ Since is a strong epic, we have a second lift , now satisfying and . A quick calculation, implicit in the diagram, shows that is precisely the lift for against .
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 is a strong epi, then is, too! Still thinking of the same diagram, suppose the whole diagram is a strong epi, and you’re given to lift against . We don’t have a as before, but we can take to get a lift .
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 is a cover (better known as a regular epimorphism), that is, it identifies as some quotient of — the stuff of is that of , 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 is the coequaliser of some maps 1, and that is a monomorphism we want to lift against.
By the universal property of a coequaliser, to “slide over” to a map , it suffices to show that it also coequalises the pair , i.e. that . Since is a mono, it’ll suffice to show that , but note that since the square commutes. Then we have
so there is a map such that — that’s commutativity of the top triangle handled. For the bottom triangle, since is a regular epic (thus an epic), to show , it’ll suffice to show that . But by assumption, and 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 is a monomorphism which is universal amongst those through which 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 as
and the epimorphism is strong, then we automatically have an image factorisation of 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 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 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 is such that there exists a with , then is an epimorphism. You can think of this as a special case of “ epic implies 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 and to lift against, form their equaliser 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 , since there’s , there’s a unique map such that . Arranging , , and the identity(!) into a lifting square like the one above, we conclude the existence of a dotted map satisfying, most importantly, — so that , 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, is the universal map which equalises and — so that we have , and since we’ve just shown that is epic, this means we have — exactly what we wanted!
in e-epi u v ker.equal
If you care, is for “relation” — the intution is that specifies the relations imposed on to get ↩︎
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.