Extremally disconnected sets

This file develops some of the basic theory of extremally disconnected compact Hausdorff spaces.

Overview

This file defines the type Stonean of all extremally (note: not "extremely"!) disconnected compact Hausdorff spaces, gives it the structure of a large category, and proves some basic observations about this category and various functors from it.

The Lean implementation: a term of type Stonean is a pair, considering of a term of type CompHaus (i.e. a compact Hausdorff topological space) plus a proof that the space is extremally disconnected. This is equivalent to the assertion that the term is projective in CompHaus, in the sense of category theory (i.e., such that morphisms out of the object can be lifted along epimorphisms).

Main definitions

• Stonean : the category of extremally disconnected compact Hausdorff spaces.
• Stonean.toCompHaus : the forgetful functor Stonean ⥤ CompHaus from Stonean spaces to compact Hausdorff spaces
• Stonean.toProfinite : the functor from Stonean spaces to profinite spaces.

structure Stonean : Type (u + 1)

Stonean is the category of extremally disconnected compact Hausdorff spaces.

• compHaus : CompHaus

  The underlying compact Hausdorff space of a Stonean space.

• extrDisc : ExtremallyDisconnected ↑self.compHaus.toTop

  A Stonean space is extremally disconnected

instance CompHaus.instExtremallyDisconnectedαTopologicalSpaceToTopTopologicalSpace_coe (X : CompHaus) [CategoryTheory.Projective X] : ExtremallyDisconnected ↑X.toTop

Projective implies ExtremallyDisconnected.

Equations

• ⋯ = ⋯

@[simp]

theorem CompHaus.toStonean_compHaus (X : CompHaus) [CategoryTheory.Projective X] : (CompHaus.toStonean X).compHaus = X

def CompHaus.toStonean (X : CompHaus) [CategoryTheory.Projective X] : Stonean

Projective implies Stonean.

Equations

• CompHaus.toStonean X = Stonean.mk X

instance Stonean.instLargeCategoryStonean : CategoryTheory.LargeCategory Stonean

Stonean spaces form a large category.

Equations

• Stonean.instLargeCategoryStonean = let_fun this := inferInstance; this

@[simp]

theorem Stonean.toCompHaus_obj : ∀ (x : Stonean), Stonean.toCompHaus.obj x = x.compHaus

@[simp]

theorem Stonean.toCompHaus_map : ∀ {X Y : CategoryTheory.InducedCategory CompHaus fun (x : Stonean) => x.compHaus} (f : X ⟶ Y), Stonean.toCompHaus.map f = f

def Stonean.toCompHaus : CategoryTheory.Functor Stonean CompHaus

The (forgetful) functor from Stonean spaces to compact Hausdorff spaces.

Equations

• Stonean.toCompHaus = CategoryTheory.inducedFunctor fun (x : Stonean) => x.compHaus

def Stonean.of (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] [ExtremallyDisconnected X] : Stonean

Construct a term of Stonean from a type endowed with the structure of a compact, Hausdorff and extremally disconnected topological space.

Equations

• Stonean.of X = Stonean.mk (CompHaus.mk { α := X, str := inferInstance })

instance Stonean.instFullStoneanInstLargeCategoryStoneanCompHausCategoryToCompHaus : CategoryTheory.Functor.Full Stonean.toCompHaus

The forgetful functor Stonean ⥤ CompHaus is full.

Equations

• Stonean.instFullStoneanInstLargeCategoryStoneanCompHausCategoryToCompHaus = ⋯

instance Stonean.instFaithfulStoneanInstLargeCategoryStoneanCompHausCategoryToCompHaus : CategoryTheory.Functor.Faithful Stonean.toCompHaus

The forgetful functor Stonean ⥤ CompHaus is faithful.

Equations

• Stonean.instFaithfulStoneanInstLargeCategoryStoneanCompHausCategoryToCompHaus = ⋯

instance Stonean.instConcreteCategoryStoneanInstLargeCategoryStonean : CategoryTheory.ConcreteCategory Stonean

Stonean spaces are a concrete category.

Equations

• Stonean.instConcreteCategoryStoneanInstLargeCategoryStonean = CategoryTheory.ConcreteCategory.mk (CategoryTheory.Functor.comp Stonean.toCompHaus (CategoryTheory.forget CompHaus))

instance Stonean.instCoeSortStoneanType : CoeSort Stonean (Type u)

Equations

• Stonean.instCoeSortStoneanType = CategoryTheory.ConcreteCategory.hasCoeToSort Stonean

instance Stonean.instFunLikeHomStoneanToQuiverToCategoryStructInstLargeCategoryStoneanCoeTypeInstCoeSortStoneanType {X : Stonean} {Y : Stonean} : FunLike (X ⟶ Y) (CoeSort.coe X) (CoeSort.coe Y)

Equations

• Stonean.instFunLikeHomStoneanToQuiverToCategoryStructInstLargeCategoryStoneanCoeTypeInstCoeSortStoneanType = CategoryTheory.ConcreteCategory.instFunLike

instance Stonean.instTopologicalSpace (X : Stonean) : TopologicalSpace (CoeSort.coe X)

Stonean spaces are topological spaces.

Equations

• Stonean.instTopologicalSpace X = let_fun this := inferInstance; this

instance Stonean.instCompactSpaceCoeStoneanTypeInstCoeSortStoneanTypeInstTopologicalSpace (X : Stonean) : CompactSpace (CoeSort.coe X)

Stonean spaces are compact.

Equations

• ⋯ = ⋯

instance Stonean.instT2SpaceCoeStoneanTypeInstCoeSortStoneanTypeInstTopologicalSpace (X : Stonean) : T2Space (CoeSort.coe X)

Stonean spaces are Hausdorff.

Equations

• ⋯ = ⋯

instance Stonean.instExtremallyDisconnectedCoeStoneanTypeInstCoeSortStoneanTypeInstTopologicalSpace (X : Stonean) : ExtremallyDisconnected (CoeSort.coe X)

Equations

• ⋯ = ⋯

@[simp]

theorem Stonean.toProfinite_obj_toCompHaus (X : Stonean) : (Stonean.toProfinite.obj X).toCompHaus = X.compHaus

@[simp]

theorem Stonean.toProfinite_map : ∀ {X Y : Stonean} (f : X ⟶ Y), Stonean.toProfinite.map f = f

def Stonean.toProfinite : CategoryTheory.Functor Stonean Profinite

The functor from Stonean spaces to profinite spaces.

Equations

• One or more equations did not get rendered due to their size.

instance Stonean.instFullStoneanInstLargeCategoryStoneanProfiniteCategoryToProfinite : CategoryTheory.Functor.Full Stonean.toProfinite

The functor from Stonean spaces to profinite spaces is full.

Equations

• Stonean.instFullStoneanInstLargeCategoryStoneanProfiniteCategoryToProfinite = ⋯

instance Stonean.instFaithfulStoneanInstLargeCategoryStoneanProfiniteCategoryToProfinite : CategoryTheory.Functor.Faithful Stonean.toProfinite

The functor from Stonean spaces to profinite spaces is faithful.

Equations

• Stonean.instFaithfulStoneanInstLargeCategoryStoneanProfiniteCategoryToProfinite = ⋯

@[simp]

theorem Stonean.isoOfHomeo_hom {X : Stonean} {Y : Stonean} (f : CoeSort.coe X ≃ₜ CoeSort.coe Y) : (Stonean.isoOfHomeo f).hom = { toFun := ⇑f, continuous_toFun := ⋯ }

@[simp]

theorem Stonean.isoOfHomeo_inv {X : Stonean} {Y : Stonean} (f : CoeSort.coe X ≃ₜ CoeSort.coe Y) : (Stonean.isoOfHomeo f).inv = CategoryTheory.inv { toFun := ⇑f, continuous_toFun := ⋯ }

noncomputable def Stonean.isoOfHomeo {X : Stonean} {Y : Stonean} (f : CoeSort.coe X ≃ₜ CoeSort.coe Y) : X ≅ Y

Construct an isomorphism from a homeomorphism.

Equations

• Stonean.isoOfHomeo f = CategoryTheory.asIso { toFun := ⇑f, continuous_toFun := ⋯ }

@[simp]

theorem Stonean.homeoOfIso_apply {X : Stonean} {Y : Stonean} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj (Stonean.toCompHaus.obj X)) : (Stonean.homeoOfIso f) a = f.hom a

@[simp]

theorem Stonean.homeoOfIso_symm_apply {X : Stonean} {Y : Stonean} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj (Stonean.toCompHaus.obj Y)) : (Homeomorph.symm (Stonean.homeoOfIso f)) a = f.inv a

def Stonean.homeoOfIso {X : Stonean} {Y : Stonean} (f : X ≅ Y) : CoeSort.coe X ≃ₜ CoeSort.coe Y

Construct a homeomorphism from an isomorphism.

Equations

• Stonean.homeoOfIso f = CompHaus.homeoOfIso (Stonean.toCompHaus.mapIso f)

@[simp]

theorem Stonean.isoEquivHomeo_apply_symm_apply {X : Stonean} {Y : Stonean} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj (Stonean.toCompHaus.obj Y)) : (Homeomorph.symm (Stonean.isoEquivHomeo f)) a = f.inv a

@[simp]

theorem Stonean.isoEquivHomeo_symm_apply_inv {X : Stonean} {Y : Stonean} (f : CoeSort.coe X ≃ₜ CoeSort.coe Y) : (Stonean.isoEquivHomeo.symm f).inv = CategoryTheory.inv { toFun := ⇑f, continuous_toFun := ⋯ }

@[simp]

theorem Stonean.isoEquivHomeo_symm_apply_hom_apply {X : Stonean} {Y : Stonean} (f : CoeSort.coe X ≃ₜ CoeSort.coe Y) (a : CoeSort.coe X) : (Stonean.isoEquivHomeo.symm f).hom a = f a

@[simp]

theorem Stonean.isoEquivHomeo_apply_apply {X : Stonean} {Y : Stonean} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj (Stonean.toCompHaus.obj X)) : (Stonean.isoEquivHomeo f) a = f.hom a

noncomputable def Stonean.isoEquivHomeo {X : Stonean} {Y : Stonean} : (X ≅ Y) ≃ (CoeSort.coe X ≃ₜ CoeSort.coe Y)

The equivalence between isomorphisms in Stonean and homeomorphisms of topological spaces.

Equations

• Stonean.isoEquivHomeo = { toFun := Stonean.homeoOfIso, invFun := Stonean.isoOfHomeo, left_inv := ⋯, right_inv := ⋯ }

def Stonean.mkFinite (X : Type u_1) [Finite X] [TopologicalSpace X] [DiscreteTopology X] : Stonean

A finite discrete space as a Stonean space.

Equations

• Stonean.mkFinite X = Stonean.mk (CompHaus.of X)

theorem Stonean.epi_iff_surjective {X : Stonean} {Y : Stonean} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑f

A morphism in Stonean is an epi iff it is surjective.

TODO: prove that forget Stonean preserves pushouts (in fact it preserves all finite colimits) and deduce this from general lemmas about concrete categories.

instance Stonean.instEpiCompHausCategoryStoneanCompHaus {X : Stonean} {Y : Stonean} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Epi f

Equations

• ⋯ = ⋯

instance Stonean.instEpiStoneanInstLargeCategoryStonean {X : Stonean} {Y : Stonean} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Epi f

Equations

• ⋯ = ⋯

instance Stonean.instProjectiveCompHausCompHaus (X : Stonean) : CategoryTheory.Projective X.compHaus

Every Stonean space is projective in CompHaus

Equations

• ⋯ = ⋯

instance Stonean.instProjectiveProfiniteCategoryObjStoneanToQuiverToCategoryStructInstLargeCategoryStoneanToPrefunctorToProfinite (X : Stonean) : CategoryTheory.Projective (Stonean.toProfinite.obj X)

Every Stonean space is projective in Profinite

Equations

• ⋯ = ⋯

instance Stonean.instProjectiveStoneanInstLargeCategoryStonean (X : Stonean) : CategoryTheory.Projective X

Every Stonean space is projective in Stonean.

Equations

• ⋯ = ⋯

noncomputable def CompHaus.presentation (X : CompHaus) : Stonean

If X is compact Hausdorff, presentation X is a Stonean space equipped with an epimorphism down to X (see CompHaus.presentation.π and CompHaus.presentation.epi_π). It is a "constructive" witness to the fact that CompHaus has enough projectives.

Equations

• CompHaus.presentation X = Stonean.mk (CompHaus.projectivePresentation X).p

noncomputable def CompHaus.presentation.π (X : CompHaus) : (CompHaus.presentation X).compHaus ⟶ X

The morphism from presentation X to X.

Equations

• CompHaus.presentation.π X = (CompHaus.projectivePresentation X).f

noncomputable instance CompHaus.presentation.epi_π (X : CompHaus) : CategoryTheory.Epi (CompHaus.presentation.π X)

The morphism from presentation X to X is an epimorphism.

Equations

• ⋯ = ⋯

noncomputable def CompHaus.lift {X : CompHaus} {Y : CompHaus} {Z : Stonean} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [CategoryTheory.Epi f] : Z.compHaus ⟶ X

               X
               |
              (f)
               |
               \/
  Z ---(e)---> Y

If Z is a Stonean space, f : X ⟶ Y an epi in CompHaus and e : Z ⟶ Y is arbitrary, then lift e f is a fixed (but arbitrary) lift of e to a morphism Z ⟶ X. It exists because Z is a projective object in CompHaus.

Equations

• CompHaus.lift e f = CategoryTheory.Projective.factorThru e f

theorem CompHaus.lift_lifts_assoc {X : CompHaus} {Y : CompHaus} {Z : Stonean} (e : Z✝.compHaus ⟶ Y) (f : X ⟶ Y) [CategoryTheory.Epi f] {Z : CompHaus} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CompHaus.lift e f) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp e h

@[simp]

theorem CompHaus.lift_lifts {X : CompHaus} {Y : CompHaus} {Z : Stonean} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.CategoryStruct.comp (CompHaus.lift e f) f = e

theorem CompHaus.Gleason (X : CompHaus) : CategoryTheory.Projective X ↔ ExtremallyDisconnected ↑X.toTop

noncomputable def Profinite.presentation (X : Profinite) : Stonean

If X is profinite, presentation X is a Stonean space equipped with an epimorphism down to X (see Profinite.presentation.π and Profinite.presentation.epi_π).

Equations

• Profinite.presentation X = Stonean.mk (CompHaus.projectivePresentation X.toCompHaus).p

noncomputable def Profinite.presentation.π (X : Profinite) : Stonean.toProfinite.obj (Profinite.presentation X) ⟶ X

The morphism from presentation X to X.

Equations

• Profinite.presentation.π X = (CompHaus.projectivePresentation X.toCompHaus).f

noncomputable instance Profinite.presentation.epi_π (X : Profinite) : CategoryTheory.Epi (Profinite.presentation.π X)

The morphism from presentation X to X is an epimorphism.

Equations

• ⋯ = ⋯

noncomputable def Profinite.lift {X : Profinite} {Y : Profinite} {Z : Stonean} (e : Stonean.toProfinite.obj Z ⟶ Y) (f : X ⟶ Y) [CategoryTheory.Epi f] : Stonean.toProfinite.obj Z ⟶ X

               X
               |
              (f)
               |
               \/
  Z ---(e)---> Y

If Z is a Stonean space, f : X ⟶ Y an epi in Profinite and e : Z ⟶ Y is arbitrary, then lift e f is a fixed (but arbitrary) lift of e to a morphism Z ⟶ X. It is CompHaus.lift e f as a morphism in Profinite.

Equations

• Profinite.lift e f = CompHaus.lift e f

theorem Profinite.lift_lifts_assoc {X : Profinite} {Y : Profinite} {Z : Stonean} (e : Stonean.toProfinite.obj Z✝ ⟶ Y) (f : X ⟶ Y) [CategoryTheory.Epi f] {Z : Profinite} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Profinite.lift e f) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp e h

@[simp]

theorem Profinite.lift_lifts {X : Profinite} {Y : Profinite} {Z : Stonean} (e : Stonean.toProfinite.obj Z ⟶ Y) (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.CategoryStruct.comp (Profinite.lift e f) f = e

theorem Profinite.projective_of_extrDisc {X : Profinite} (hX : ExtremallyDisconnected ↑X.toCompHaus.toTop) : CategoryTheory.Projective X