mathlib documentation

topology.category.Profinite

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 Top. The fully faithful functor is called Profinite_to_Top.

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. existence of products, limits(?), finite coproducts
  3. Profinite_to_Top creates limits?
  4. Clausen/Scholze topology on the category Profinite.

Tags #

profinite

structure Profinite  :
Type (u_1+1)

The type of profinite topological spaces.

@[instance]
Equations
@[instance]
Equations
@[instance]
@[simp]
theorem Profinite.coe_to_Top {X : Profinite} :
@[simp]
theorem Profinite.to_CompHaus_map (_x _x_1 : Profinite) (f : _x _x_1) :

The fully faithful embedding of Profinite in CompHaus.

Equations

(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

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

Equations

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

Equations
@[instance]

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

Equations