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:

Main results #

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

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₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂)CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e 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} [Fintype α] {B : Stonean} {X : αStonean} (π : (a : α) → X a B) (surj : ∀ (b : CoeSort.coe B), a x, ↑(π a) x = b) :

    Implementation: The structure for the EffectiveEpiFamily X π.

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

      One direction of effectiveEpiFamily_tfae.

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