Documentation

Mathlib.Topology.Category.LightProfinite.EffectiveEpi

Effective epimorphisms in LightProfinite #

This file proves that EffectiveEpi and Surjective are equivalent in LightProfinite. As a consequence we deduce from the material in Mathlib.Topology.Category.CompHausLike.EffectiveEpi that LightProfinite is Preregular and Precoherent.

source
theorem LightProfinite.effectiveEpi_iff_surjective {X Y : LightProfinite} (f : X ⟶ Y) :
CategoryTheory.EffectiveEpi f ↔ Function.Surjective ⇑f
source
instance LightProfinite.instPreregular :
CategoryTheory.Preregular LightProfinite
Equations