module Cat.Diagram.Coequaliser.RegularEpi {o β} (C : Precategory o β) where
Regular epimorphismsπ
Dually to regular monomorphisms, which behave as embeddings, regular epimorphisms behave like covers: A regular epimorphism expresses as βa union of parts of , possibly glued togetherβ.
The definition is also precisely dual: A map is a regular epimorphism if it is the coequaliser of some pair of arrows .
record is-regular-epi (f : Hom a b) : Type (o β β) where no-eta-equality constructor reg-epi field {r} : Ob {arrβ} {arrβ} : Hom r a has-is-coeq : is-coequaliser C arrβ arrβ f open is-coequaliser has-is-coeq public
From the definition we can directly conclude that regular epis are in fact epic:
is-regular-epiβis-epic : is-epic f is-regular-epiβis-epic = is-coequaliserβis-epic C _ has-is-coeq open is-regular-epi using (is-regular-epiβis-epic) public
Effective episπ
Again by duality, we have a pair of canonical choices of maps which may coequalise: Its kernel pair, that is, the pullback of along itself. An epimorphism which coequalises its kernel pair is called an effective epi, and effective epis are immediately seen to be regular epis:
record is-effective-epi (f : Hom a b) : Type (o β β) where no-eta-equality field {kernel} : Ob pβ pβ : Hom kernel a is-kernel-pair : is-pullback C pβ f pβ f has-is-coeq : is-coequaliser C pβ pβ f is-effective-epiβis-regular-epi : is-regular-epi f is-effective-epiβis-regular-epi = re where open is-regular-epi hiding (has-is-coeq) re : is-regular-epi f re .r = _ re .arrβ = _ re .arrβ = _ re .is-regular-epi.has-is-coeq = has-is-coeq
If a regular epimorphism (a coequaliser) has a kernel pair, then it is also the coequaliser of its kernel pair. That is: If the pullback of exists, then is also an effective epimorphism.
is-regular-epiβis-effective-epi : β {a b} {f : Hom a b} β Pullback C f f β is-regular-epi f β is-effective-epi f is-regular-epiβis-effective-epi {f = f} kp reg = epi where module reg = is-regular-epi reg module kp = Pullback kp open is-effective-epi open is-coequaliser epi : is-effective-epi f epi .kernel = kp.apex epi .pβ = kp.pβ epi .pβ = kp.pβ epi .is-kernel-pair = kp.has-is-pb epi .has-is-coeq .coequal = kp.square epi .has-is-coeq .universal {F = F} {e'} p = reg.universal q where q : e' β reg.arrβ β‘ e' β reg.arrβ q = e' β reg.arrβ β‘β¨ ap (e' β_) (sym kp.pββuniversal) β©β‘ e' β kp.pβ β kp.universal (sym reg.coequal) β‘β¨ pulll (sym p) β©β‘ (e' β kp.pβ) β kp.universal _ β‘β¨ pullr kp.pββuniversal β©β‘ e' β reg.arrβ β epi .has-is-coeq .factors = reg.factors epi .has-is-coeq .unique = reg.unique