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.lean that LightProfinite is Preregular
and Precoherent.
theorem
LightProfinite.effectiveEpi_iff_surjective
{X Y : LightProfinite}
(f : X ⟶ Y)
:
CategoryTheory.EffectiveEpi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)