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 #

structure Stonean :
Type (u + 1)
  • compHaus : CompHaus

    The underlying compact Hausdorff space of a Stonean space.

  • extrDisc : ExtremallyDisconnected s.compHaus.toTop

    A Stonean space is extremally disconnected

Stonean is the category of extremally disconnected compact Hausdorff spaces.

Instances For

    Projective implies Stonean.

    Instances For

      Stonean spaces form a large category.

      @[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 => x.compHaus} (f : X Y), Stonean.toCompHaus.map f = f

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

      Instances For

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

        Instances For

          Stonean spaces are topological spaces.

          @[simp]
          theorem Stonean.toProfinite_map :
          ∀ {X Y : Stonean} (f : X Y), Stonean.toProfinite.map f = f
          @[simp]
          theorem Stonean.toProfinite_obj_toCompHaus (X : Stonean) :
          (Stonean.toProfinite.obj X).toCompHaus = X.compHaus

          The functor from Stonean spaces to profinite spaces.

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

            Construct an isomorphism from a homeomorphism.

            Instances For
              @[simp]
              @[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

              Construct a homeomorphism from an isomorphism.

              Instances For
                @[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
                @[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 (ContinuousMap.mk f)
                @[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_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
                noncomputable def Stonean.isoEquivHomeo {X : Stonean} {Y : Stonean} :

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

                Instances For

                  A finite discrete space as a Stonean space.

                  Instances For

                    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.

                    Every Stonean space is projective in CompHaus

                    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.

                    Instances For
                      noncomputable def CompHaus.presentation.π (X : CompHaus) :
                      (CompHaus.presentation X).compHaus X

                      The morphism from presentation X to X.

                      Instances For

                        The morphism from presentation X to X is an epimorphism.

                        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.

                        Instances For
                          @[simp]
                          theorem CompHaus.lift_lifts {X : CompHaus} {Y : CompHaus} {Z : Stonean} (e : Z.compHaus Y) (f : X Y) [CategoryTheory.Epi f] :
                          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_π).

                          Instances For

                            The morphism from presentation X to X.

                            Instances For

                              The morphism from presentation X to X is an epimorphism.

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

                              Instances For