Effective epimorphisms and finite effective epimorphic families in Profinite
#
This file proves that Profinite
is Preregular
. Together with the fact that it is
FinitaryPreExtensive
, this implies that Profinite
is Precoherent
.
To do this, we need to characterise effective epimorphisms in Profinite
. As a consequence, we also
get a characterisation of finite effective epimorphic families.
Main results #

Profinite.effectiveEpi_tfae
: For a morphism inProfinite
, the conditions surjective, epimorphic, and effective epimorphic are all equivalent. 
Profinite.effectiveEpiFamily_tfae
: For a finite family of morphisms inProfinite
with fixed target inProfinite
, the conditions jointly surjective, jointly epimorphic and effective epimorphic are all equivalent.
As a consequence, we obtain instances that Profinite
is precoherent and preregular.
 TODO: Write API for reflecting effective epimorphisms and deduce the contents of this file by
abstract nonsense from the corresponding results for
CompHaus
.
Implementation: If π
is a surjective morphism in Profinite
, then it is an effective epi.
The theorem Profinite.effectiveEpi_tfae
should be used instead.
Equations
 One or more equations did not get rendered due to their size.