mathlib documentation

topology.category.Profinite.default

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. finite coproducts
  3. Clausen/Scholze topology on the category Profinite.

Tags #

profinite

structure Profinite  :
Type (u_1+1)

The type of profinite topological spaces.

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

Equations
@[instance]
Equations
@[simp]
theorem Profinite.coe_id (X : Profinite) :
@[simp]
theorem Profinite.coe_comp {X Y Z : Profinite} (f : X Y) (g : Y Z) :
(f g) = g f

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

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

Finite types are given the discrete topology.

Equations
@[simp]
theorem Fintype.to_Profinite_map_to_fun (_x _x_1 : Fintype) (f : _x _x_1) (ᾰ : _x.α) :

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

Equations
@[instance]

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

Equations
theorem Profinite.is_closed_map {X Y : Profinite} (f : X Y) :

Any morphism of profinite spaces is a closed map.

Any continuous bijection of profinite spaces induces an isomorphism.

def Profinite.iso_of_bijective {X Y : Profinite} (f : X Y) (bij : function.bijective f) :
X Y

Any continuous bijection of profinite spaces induces an isomorphism.

Equations
def Profinite.iso_of_homeo {X Y : Profinite} (f : X ≃ₜ Y) :
X Y

Construct an isomorphism from a homeomorphism.

Equations
def Profinite.homeo_of_iso {X Y : Profinite} (f : X Y) :

Construct a homeomorphism from an isomorphism.

Equations
@[simp]
theorem Profinite.homeo_of_iso_symm_apply {X Y : Profinite} (f : X Y) (ᾰ : (Y.to_CompHaus.to_Top)) :
@[simp]
theorem Profinite.homeo_of_iso_apply {X Y : Profinite} (f : X Y) (ᾰ : (X.to_CompHaus.to_Top)) :

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

Equations