# Documentation

Mathlib.Topology.Category.Stonean.EffectiveEpi

# 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.

@[inline, reducible]

Implementation: Abbreviation for the fully faithful functor Stonean ⥤ CompHaus.

Instances For
theorem Stonean.EffectiveEpiFamily.lift_desc_condition {α : Type} {B : Stonean} {X : αStonean} (π : (a : α) → X a B) {W : Stonean} {e : (a : α) → X a W} (h : ∀ {Z : Stonean} (a₁ a₂ : α) (g₁ : Z X a₁) (g₂ : Z X a₂), = = ) {Z : CompHaus} (a₁ : α) (a₂ : α) (g₁ : Z Stonean.EffectiveEpiFamily.F.obj (X a₁)) (g₂ : Z Stonean.EffectiveEpiFamily.F.obj (X a₂)) :
= =

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.

noncomputable def Stonean.EffectiveEpiFamily.struct {α : Type} [] {B : Stonean} {X : αStonean} (π : (a : α) → X a B) (surj : ∀ (b : ), a x, ↑(π a) x = b) :

Implementation: The structure for the EffectiveEpiFamily X π.

Instances For
theorem Stonean.effectiveEpiFamily_of_jointly_surjective {α : Type} [] {B : Stonean} (X : αStonean) (π : (a : α) → X a B) (surj : ∀ (b : ), a x, ↑(π a) x = b) :

One direction of effectiveEpiFamily_tfae.

theorem Stonean.effectiveEpiFamily_tfae {α : Type} [] {B : Stonean} (X : αStonean) (π : (a : α) → X a B) :
List.TFAE [, , ∀ (b : ), a x, ↑(π a) x = b]

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
theorem CategoryTheory.EffectiveEpiFamily.toCompHaus {α : Type} [] {B : Stonean} {X : αStonean} {π : (a : α) → X a B} (H : ) :