Effective epimorphisms in CompHausLike

In any category of compact Hausdorff spaces, continuous surjections are effective epimorphisms.

We deduce that if the converse holds and explicit pullbacks exist, then CompHausLike P is preregular.

If furthermore explicit finite coproducts exist, then CompHausLike P is precoherent.

noncomputable def CompHausLike.effectiveEpiStruct {P : TopCat → Prop} {B X : CompHausLike P} (π : X ⟶ B) (hπ : Function.Surjective ⇑π) : CategoryTheory.EffectiveEpiStruct π

If π is a surjective morphism in CompHausLike P, then it is an effective epi.

Equations

• One or more equations did not get rendered due to their size.

theorem CompHausLike.preregular {P : TopCat → Prop} [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) : CategoryTheory.Preregular (CompHausLike P)

theorem CompHausLike.precoherent {P : TopCat → Prop} [CompHausLike.HasExplicitPullbacks P] [CompHausLike.HasExplicitFiniteCoproducts P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) : CategoryTheory.Precoherent (CompHausLike P)