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

@[reducible, inline]
abbrev Profinite :
Type (u_1 + 1)

The type of profinite topological spaces.

Equations
Instances For
    @[reducible, inline]

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

    Equations
    Instances For
      @[reducible, inline]

      The fully faithful embedding of Profinite in CompHaus.

      Equations
      Instances For
        @[reducible, inline]

        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
            def Profinite.toCompHausEquivalence (X : CompHaus) (Y : Profinite) :
            (X.toProfiniteObj Y) (X profiniteToCompHaus.obj Y)

            (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

                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

                  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

                    FintypeCat.toLightProfinite is fully faithful.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    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