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.

noncomputable def CompHausLike.effectiveEpiStruct {P : TopCatProp} {B : CompHausLike P} {X : CompHausLike P} (π : X B) (hπ : Function.Surjective π) :

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