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]

abbrev Stonean.EffectiveEpiFamily.F : CategoryTheory.Functor Stonean CompHaus

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

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₂)) : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e 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) : CategoryTheory.EffectiveEpiFamilyStruct X π

Implementation: The structure for the EffectiveEpiFamily X π.

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) : CategoryTheory.EffectiveEpiFamily X π

One direction of effectiveEpiFamily_tfae.

theorem Stonean.effectiveEpiFamily_tfae {α : Type} [Fintype α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B) : List.TFAE [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : CoeSort.coe 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} [Fintype α] {B : Stonean} {X : α → Stonean} {π : (a : α) → X a ⟶ B} (H : CategoryTheory.EffectiveEpiFamily X π) : CategoryTheory.EffectiveEpiFamily (fun x => Stonean.toCompHaus.obj (X x)) fun x => Stonean.toCompHaus.map (π x)

instance Stonean.instPrecoherent : CategoryTheory.Precoherent Stonean