Documentation

Mathlib.Topology.Category.Stonean.Basic

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 #

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.

Equations
@[reducible, inline]

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

Equations
@[reducible, inline]

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

Equations
@[reducible, inline]

The functor from Stonean spaces to profinite spaces.

Equations

A finite discrete space as a Stonean space.

Equations

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

Every Stonean space is projective in Stonean.

noncomputable def CompHaus.presentation (X : CompHaus) :

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

The morphism from presentation X to X is an epimorphism.

@[reducible, inline]

The underlying CompHaus of a Stonean.

Equations
noncomputable def CompHaus.lift {X Y : CompHaus} {Z : Stonean} (e : Z.compHaus Y) (f : X Y) [CategoryTheory.Epi f] :
               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
@[simp]
noncomputable def Profinite.presentation (X : Profinite) :

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

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] :
               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