Documentation

Mathlib.Topology.Category.CompHausLike.EffectiveEpi

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.

source
noncomputable def CompHausLike.effectiveEpiStruct {P : TopCat → Prop} {B X : CompHausLike P} (π : X ⟶ B) (hπ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)) :
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.
Instances For
    source
    theorem CompHausLike.preregular {P : TopCat → Prop} [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) :
    CategoryTheory.Preregular (CompHausLike P)
    source
    theorem CompHausLike.precoherent {P : TopCat → Prop} [HasExplicitPullbacks P] [HasExplicitFiniteCoproducts P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) :
    CategoryTheory.Precoherent (CompHausLike P)