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 #

Tags #

profinite

structure Profinite :
Type (u_1 + 1)

The type of profinite topological spaces.

  • toCompHaus : CompHaus

    The underlying compact Hausdorff space of a profinite space.

  • isTotallyDisconnected : TotallyDisconnectedSpace self.toCompHaus.toTop

    A profinite space is totally disconnected.

Instances For

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

    Equations
    Instances For
      Equations
      @[simp]
      theorem Profinite.forget_ContinuousMap_mk {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTopY.toCompHaus.toTop) (hf : Continuous f) :
      (CategoryTheory.forget Profinite).map { toFun := f, continuous_toFun := hf } = f
      Equations
      • Profinite.instTopologicalSpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory = let_fun this := inferInstance; this
      @[simp]
      theorem profiniteToCompHaus_obj (self : Profinite) :
      profiniteToCompHaus.obj self = self.toCompHaus

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

      Equations
      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

        Equations
        Instances For

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

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

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

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

              Finite types are given the discrete topology.

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[inline, reducible]
                  abbrev ProfiniteMax :
                  Type ((max w w') + 1)

                  Many definitions involving universe inequalities in Mathlib are expressed through use of max u v. Unfortunately, this leads to unbound universes which cannot be solved for during unification, eg max u v =?= max v ?. The current solution is to wrap Type max u v in TypeMax.{u,v} to expose both universe parameters directly.

                  Similarly, for other concrete categories for which we need to refer to the maximum of two universes (e.g. any category for which we are constructing limits), we need an analogous abbreviation.

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

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

                      The limit cone Profinite.limitCone F is indeed a limit cone.

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

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

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

                        Equations
                        Instances For
                          @[simp]
                          theorem Profinite.isoOfHomeo_hom {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
                          (Profinite.isoOfHomeo f).hom = { toFun := f, continuous_toFun := }
                          @[simp]
                          theorem Profinite.isoOfHomeo_inv {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
                          (Profinite.isoOfHomeo f).inv = CategoryTheory.inv { toFun := f, continuous_toFun := }
                          noncomputable def Profinite.isoOfHomeo {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
                          X Y

                          Construct an isomorphism from a homeomorphism.

                          Equations
                          Instances For
                            @[simp]
                            theorem Profinite.homeoOfIso_symm_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : (CategoryTheory.forget CompHaus).obj Y.toCompHaus) :
                            @[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.

                            Equations
                            Instances For
                              @[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
                              @[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 { toFun := f, continuous_toFun := }
                              @[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
                              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.

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