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.

Implementation

The category Stonean is defined using the structure CompHausLike. See the file CompHausLike.Basic for more information.

@[reducible, inline]

abbrev Stonean : Type (u_1 + 1)

Stonean is the category of extremally disconnected compact Hausdorff spaces.

instance CompHaus.instExtremallyDisconnectedCarrierToTopTrueOfProjective (X : CompHaus) [CategoryTheory.Projective X] : ExtremallyDisconnected ↑X.toTop

Projective implies ExtremallyDisconnected.

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

Projective implies Stonean.

@[simp]

theorem CompHaus.toStonean_toTop (X : CompHaus) [CategoryTheory.Projective X] : X.toStonean.toTop = X.toTop

@[reducible, inline]

abbrev Stonean.toCompHaus : CategoryTheory.Functor Stonean CompHaus

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

@[reducible, inline]

abbrev Stonean.fullyFaithfulToCompHaus : toCompHaus.FullyFaithful

The forgetful functor Stonean ⥤ CompHaus is fully faithful.

instance Stonean.instHasPropExtremallyDisconnectedCarrier (X : Type u_1) [TopologicalSpace X] [ExtremallyDisconnected X] : CompHausLike.HasProp (fun (Y : TopCat) => ExtremallyDisconnected ↑Y) X

@[reducible, inline]

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

instance Stonean.instExtremallyDisconnectedCarrierToTop (X : Stonean) : ExtremallyDisconnected ↑X.toTop

@[reducible, inline]

abbrev Stonean.toProfinite : CategoryTheory.Functor Stonean Profinite

The functor from Stonean spaces to profinite spaces.

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

A finite discrete space as a Stonean space.

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

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

instance Stonean.instProjectiveCompHausCompHaus (X : Stonean) : CategoryTheory.Projective (toCompHaus.obj X)

Every Stonean space is projective in CompHaus

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

Every Stonean space is projective in Profinite

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

Every Stonean space is projective in Stonean.

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.

noncomputable def CompHaus.presentation.π (X : CompHaus) : Stonean.toCompHaus.obj X.presentation ⟶ X

The morphism from presentation X to X.

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

The morphism from presentation X to X is an epimorphism.

@[reducible, inline]

abbrev Stonean.compHaus (X : Stonean) : CompHaus

The underlying CompHaus of a Stonean.

noncomputable def CompHaus.lift {X 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.

@[simp]

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

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

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_π).

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

The morphism from presentation X to X.

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

The morphism from presentation X to X is an epimorphism.

noncomputable def Profinite.lift {X 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.

@[simp]

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

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

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