Effective epimorphic families in Stonean
#
Let π a : X a ⟶ B
be a family of morphisms in Stonean
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 #
Stonean.effectiveEpiFamily_tfae
: characterise being an effective epimorphic family.Stonean.instPrecoherent
:Stonean
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 Stonean.effectiveEpiFamily_of_jointly_surjective
.
Implementation: A helper lemma lifting the condition
∀ {Z : Stonean} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
from Z : Stonean
to Z : CompHaus
.
The descent EffectiveEpiFamily.dec
along an effective epi family in a category C
takes this condition (for all Z
in C
) as an assumption.
In the construction in this file we start with this descent condition for all Z : Stonean
but
to apply the analogue result on CompHaus
we need extend this condition to all
Z : CompHaus
. We do this by considering the Stone-Cech compactification βZ → Z
which is an epi in CompHaus
covering Z
where βZ
lies in the image of Stonean
.
Implementation: The structure for the EffectiveEpiFamily X π
.
Instances For
One direction of effectiveEpiFamily_tfae
.
For a finite family of extremally spaces π a : X a → B
the following are equivalent:
π
is an effective epimorphic family- the map
∐ π a ⟶ B
is an epimorphism π
is jointly surjective