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.ConcreteCategory.hom π))
:
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
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))
:
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))
: