open import Cat.Diagram.Coequaliser open import Cat.Diagram.Pullback open import Cat.Diagram.Initial open import Cat.Prelude import Cat.Reasoning 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 = eff where module reg = is-regular-epi reg module kp = Pullback kp open is-effective-epi open is-coequaliser eff : is-effective-epi f eff .kernel = kp.apex eff .pβ = kp.pβ eff .pβ = kp.pβ eff .is-kernel-pair = kp.has-is-pb eff .has-is-coeq .coequal = kp.square eff .has-is-coeq .coequalise {F = F} {eβ²} p = reg.coequalise q where q : eβ² β reg.arrβ β‘ eβ² β reg.arrβ q = eβ² β reg.arrβ β‘β¨ ap (eβ² β_) (sym kp.pββlimiting) β©β‘ eβ² β kp.pβ β kp.limiting (sym reg.coequal) β‘β¨ pulll (sym p) β©β‘ (eβ² β kp.pβ) β kp.limiting _ β‘β¨ pullr kp.pββlimiting β©β‘ eβ² β reg.arrβ β eff .has-is-coeq .universal = reg.universal eff .has-is-coeq .unique = reg.unique