Documentation

Mathlib.Topology.Category.Profinite.Basic

The category of Profinite Types #

We construct the category of profinite topological spaces, often called profinite sets -- perhaps they could be called profinite types in Lean.

The type of profinite topological spaces is called Profinite. It has a category instance and is a fully faithful subcategory of TopCat. The fully faithful functor is called Profinite.toTop.

Implementation notes #

A profinite type is defined to be a topological space which is compact, Hausdorff and totally disconnected.

TODO #

  1. Link to category of projective limits of finite discrete sets.
  2. finite coproducts
  3. Clausen/Scholze topology on the category Profinite.

Tags #

profinite

structure Profinite :
Type (u_1 + 1)
  • toCompHaus : CompHaus

    The underlying compact Hausdorff space of a profinite space.

  • IsTotallyDisconnected : TotallyDisconnectedSpace s.toCompHaus.toTop

    A profinite space is totally disconnected.

The type of profinite topological spaces.

Instances For

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

    Instances For
      @[simp]
      theorem Profinite.forget_ContinuousMap_mk {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTopY.toCompHaus.toTop) (hf : Continuous f) :
      @[simp]
      theorem profiniteToCompHaus_obj (self : Profinite) :
      profiniteToCompHaus.obj self = self.toCompHaus

      The fully faithful embedding of Profinite in CompHaus.

      Instances For
        @[simp]
        theorem Profinite.toTopCat_map :
        ∀ {X Y : CategoryTheory.InducedCategory TopCat fun X => X.toCompHaus.toTop} (f : X Y), Profinite.toTopCat.map f = f

        The fully faithful embedding of Profinite in TopCat. This is definitionally the same as the obvious composite.

        Instances For

          (Implementation) The object part of the connected_components functor from compact Hausdorff spaces to Profinite spaces, given by quotienting a space by its connected components. See: https://stacks.math.columbia.edu/tag/0900

          Instances For

            (Implementation) The bijection of homsets to establish the reflective adjunction of Profinite spaces in compact Hausdorff spaces.

            Instances For

              The connected_components functor from compact Hausdorff spaces to profinite spaces, left adjoint to the inclusion functor.

              Instances For
                theorem CompHaus.toProfinite_obj' (X : CompHaus) :
                (CompHaus.toProfinite.obj X).toCompHaus.toTop = ConnectedComponents X.toTop

                Finite types are given the discrete topology.

                Instances For
                  @[simp]
                  theorem FintypeCat.toProfinite_map_apply :
                  ∀ {X Y : FintypeCat} (f : X Y) (a : X), ↑(FintypeCat.toProfinite.map f) a = f a
                  @[simp]

                  The natural functor from Fintype to Profinite, endowing a finite type with the discrete topology.

                  Instances For

                    An explicit limit cone for a functor F : J ⥤ Profinite, defined in terms of CompHaus.limitCone, which is defined in terms of TopCat.limitCone.

                    Instances For

                      The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus

                      Instances For

                        The category of profinite sets is reflective in the category of compact Hausdorff spaces

                        theorem Profinite.isClosedMap {X : Profinite} {Y : Profinite} (f : X Y) :

                        Any morphism of profinite spaces is a closed map.

                        Any continuous bijection of profinite spaces induces an isomorphism.

                        noncomputable def Profinite.isoOfBijective {X : Profinite} {Y : Profinite} (f : X Y) (bij : Function.Bijective f) :
                        X Y

                        Any continuous bijection of profinite spaces induces an isomorphism.

                        Instances For
                          @[simp]
                          theorem Profinite.isoOfHomeo_hom {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
                          @[simp]
                          theorem Profinite.isoOfHomeo_inv {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
                          noncomputable def Profinite.isoOfHomeo {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
                          X Y

                          Construct an isomorphism from a homeomorphism.

                          Instances For
                            @[simp]
                            theorem Profinite.homeoOfIso_symm_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : (CategoryTheory.forget CompHaus).obj Y.toCompHaus) :
                            ↑(Homeomorph.symm (Profinite.homeoOfIso f)) a = f.inv a
                            @[simp]
                            theorem Profinite.homeoOfIso_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : (CategoryTheory.forget CompHaus).obj X.toCompHaus) :
                            ↑(Profinite.homeoOfIso f) a = f.hom a
                            def Profinite.homeoOfIso {X : Profinite} {Y : Profinite} (f : X Y) :
                            X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop

                            Construct a homeomorphism from an isomorphism.

                            Instances For
                              @[simp]
                              theorem Profinite.isoEquivHomeo_symm_apply_inv {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
                              (Profinite.isoEquivHomeo.symm f).inv = CategoryTheory.inv (ContinuousMap.mk f)
                              @[simp]
                              theorem Profinite.isoEquivHomeo_apply_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : (CategoryTheory.forget CompHaus).obj X.toCompHaus) :
                              ↑(Profinite.isoEquivHomeo f) a = f.hom a
                              @[simp]
                              theorem Profinite.isoEquivHomeo_apply_symm_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : (CategoryTheory.forget CompHaus).obj Y.toCompHaus) :
                              ↑(Homeomorph.symm (Profinite.isoEquivHomeo f)) a = f.inv a
                              @[simp]
                              theorem Profinite.isoEquivHomeo_symm_apply_hom_apply {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) (a : X.toCompHaus.toTop) :
                              (Profinite.isoEquivHomeo.symm f).hom a = f a
                              noncomputable def Profinite.isoEquivHomeo {X : Profinite} {Y : Profinite} :
                              (X Y) (X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop)

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

                              Instances For