Effective epimorphic families in Profinite
#
Let π a : X a ⟶ B
be a family of morphisms in Profinite
indexed by a finite type α
.
In this file, we show that the following are all equivalent:
- The family
π
is effective epimorphic. - The induced map
∐ X ⟶ B
is epimorphic. - The family
π
is jointly surjective.
Main results #
Profinite.effectiveEpiFamily_tfae
: characterise being an effective epimorphic family.Profinite.instPrecoherent
:Profinite
is precoherent.
Implementation notes #
The entire section EffectiveEpiFamily
comprises exclusively a technical construction for
the main proof and does not contain any statements that would be useful in other contexts.
This section contains exclusively technical definitions and results that are used
in the proof of Profinite.effectiveEpiFamily_of_jointly_surjective
.
The construction of QB
as a quotient of the maps X a → B
is analoguous to the
construction in the file CompHaus.EffectiveEpi
,
but one has to start with an equivalence relation on Profinite
instead.
Implementation: This is a setoid on the explicit finite coproduct of X
whose quotient
will be isomorphic to B
provided that X a → B
is an effective epi family.
Instances For
Implementation: The map from the quotient of relation π
to B
, which will eventually
become the function underlying an isomorphism, provided that X a → B
is an effective epi family.
Instances For
Implementation: ιFun
as isomorphism in CompHaus
.
Instances For
Implementation: The function ιFun
, considered as a morphism in Profinite
.
Instances For
Implementation: ιFun
as an isomorphism in Profinite
.
Instances For
Implementation: The family of morphisms X a ⟶ QB
which will be shown to be effective epi.
Instances For
Implementation: ιIso ∘ (π' a) : X a → QB → B
is exactly π a
.
Implementation: ιIso⁻¹ ∘ (π a) : X a → B → QB
is exactly π' a
.
Implementation: The family X
is an effective epi, provided that π
are jointly surjective.
The theorem Profinite.effectiveEpiFamily_tfae
should be used instead.
Instances For
One direction of Profinite.effectiveEpiFamily_tfae
For a finite family of profinite spaces π a : X a → B
the following are equivalent:
π
is an effective epimorphic family- the map
∐ π a ⟶ B
is an epimorphism π
is jointly surjective
The category of profinite spaces is precoherent