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)

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

Instances For
    theorem Stonean.extrDisc (self : Stonean) :
    ExtremallyDisconnected self.compHaus.toTop

    A Stonean space is extremally disconnected

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

    Projective implies Stonean.

    Equations
    Instances For

      Stonean spaces form a large category.

      Equations
      @[simp]
      theorem Stonean.toCompHaus_map :
      ∀ {X Y : CategoryTheory.InducedCategory CompHaus fun (x : Stonean) => x.compHaus} (f : X Y), Stonean.toCompHaus.map f = f
      @[simp]
      theorem Stonean.toCompHaus_obj :
      ∀ (x : Stonean), Stonean.toCompHaus.obj x = x.compHaus

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

      Equations
      Instances For

        The forgetful functor StoneanCompHaus is fully faithful.

        Equations
        Instances For

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

          Equations
          Instances For
            Equations
            • Stonean.instFunLikeHomCoe = CategoryTheory.ConcreteCategory.instFunLike

            Stonean spaces are topological spaces.

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

            Stonean spaces are compact.

            Equations
            • =

            Stonean spaces are Hausdorff.

            Equations
            • =
            @[simp]
            theorem Stonean.toProfinite_obj_toTop (X : Stonean) :
            (Stonean.toProfinite.obj X).toTop = X.compHaus.toTop
            @[simp]
            theorem Stonean.toProfinite_map :
            ∀ {X Y : Stonean} (f : X Y), Stonean.toProfinite.map f = f

            The functor from Stonean spaces to profinite spaces.

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

              The functor from Stonean spaces to profinite spaces is full.

              Equations

              The functor from Stonean spaces to profinite spaces is faithful.

              Equations
              @[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
              Instances For
                @[simp]
                theorem Stonean.homeoOfIso_apply {X : Stonean} {Y : Stonean} (f : X Y) (a : (Stonean.toCompHaus.obj X).toTop) :
                (Stonean.homeoOfIso f) a = f.hom a
                @[simp]
                theorem Stonean.homeoOfIso_symm_apply {X : Stonean} {Y : Stonean} (f : X Y) (a : (Stonean.toCompHaus.obj Y).toTop) :
                (Stonean.homeoOfIso f).symm a = f.inv a

                Construct a homeomorphism from an isomorphism.

                Equations
                Instances For
                  @[simp]
                  theorem Stonean.isoEquivHomeo_apply_symm_apply {X : Stonean} {Y : Stonean} (f : X Y) (a : (Stonean.toCompHaus.obj Y).toTop) :
                  (Stonean.isoEquivHomeo f).symm a = f.inv a
                  @[simp]
                  theorem Stonean.isoEquivHomeo_apply_apply {X : Stonean} {Y : Stonean} (f : X Y) (a : (Stonean.toCompHaus.obj X).toTop) :
                  (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 { 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
                  noncomputable def Stonean.isoEquivHomeo {X : Stonean} {Y : Stonean} :

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

                  Equations
                  • Stonean.isoEquivHomeo = { toFun := Stonean.homeoOfIso, invFun := Stonean.isoOfHomeo, left_inv := , right_inv := }
                  Instances For

                    A finite discrete space as a Stonean space.

                    Equations
                    Instances For

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

                      Equations
                      • =
                      Equations
                      • =

                      Every Stonean space is projective in CompHaus

                      Equations
                      • =

                      Every Stonean space is projective in Profinite

                      Equations
                      • =

                      Every Stonean space is projective in Stonean.

                      Equations
                      • =
                      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
                      Instances For
                        noncomputable def CompHaus.presentation.π (X : CompHaus) :
                        X.presentation.compHaus X

                        The morphism from presentation X to X.

                        Equations
                        Instances For

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

                            Equations
                            Instances For
                              noncomputable def Profinite.presentation.π (X : Profinite) :
                              Stonean.toProfinite.obj X.presentation X

                              The morphism from presentation X to X.

                              Equations
                              Instances For

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