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

source
structure Profinite  :
Type (u_1+1)

The type of profinite topological spaces.

source
@[instance]
def Profinite.inhabited  :
inhabited Profinite
Equations
source
@[instance]
def Profinite.has_coe_to_sort  :
has_coe_to_sort Profinite
Equations
source
@[instance]
def Profinite.compact_space {X : Profinite} :
compact_space ↥X
source
@[instance]
def Profinite.t2_space {X : Profinite} :
t2_space ↥X
source
@[instance]
def Profinite.totally_disconnected_space {X : Profinite} :
totally_disconnected_space ↥X
source
@[instance]
def Profinite.category  :
category_theory.category Profinite
Equations
source
@[simp]
theorem Profinite.coe_to_Top {X : Profinite} :
↥(X.to_Top) = ↥X
source
def Profinite_to_Top  :
Profinite ⥤ Top

The fully faithful embedding of Profinite in Top.

Equations
source
@[simp]
theorem Profinite_to_Top_map (x y : category_theory.induced_category Top Profinite.to_Top) (f : x ⟶ y) :
Profinite_to_Top.map f = f
source
@[instance]
def Profinite_to_Top.faithful  :
category_theory.faithful Profinite_to_Top
source
@[instance]
def Profinite_to_Top.full  :
category_theory.full Profinite_to_Top
source
@[simp]
theorem Profinite_to_Top_obj (c : Profinite) :
Profinite_to_Top.obj c = c.to_Top
source
@[simp]
theorem Profinite.to_CompHaus_map (_x _x_1 : Profinite) (f : _x ⟶ _x_1) :
Profinite.to_CompHaus.map f = f
source
def Profinite.to_CompHaus  :
Profinite ⥤ CompHaus

The fully faithful embedding of Profinite in CompHaus.

Equations
source
@[simp]
theorem Profinite.to_CompHaus_obj_to_Top (X : Profinite) :
(Profinite.to_CompHaus.obj X).to_Top = X.to_Top
source
@[instance]
def Profinite.to_CompHaus.category_theory.full  :
category_theory.full Profinite.to_CompHaus
Equations
source
@[instance]
def Profinite.to_CompHaus.category_theory.faithful  :
category_theory.faithful Profinite.to_CompHaus
source
@[simp]
theorem Profinite.to_CompHaus_to_Top  :
Profinite.to_CompHaus ⋙ CompHaus_to_Top = Profinite_to_Top
source
def CompHaus.to_Profinite_obj (X : CompHaus) :
Profinite

(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
source
def Profinite.to_CompHaus_equivalence (X : CompHaus) (Y : Profinite) :
(X.to_Profinite_obj ⟶ Y) ≃ (X ⟶ Profinite.to_CompHaus.obj Y)

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

Equations
source
def CompHaus.to_Profinite  :
CompHaus ⥤ Profinite

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

Equations
source
def Profinite.to_Profinite_adj_to_CompHaus  :
CompHaus.to_Profinite ⊣ Profinite.to_CompHaus

The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus

Equations
source
theorem CompHaus.to_Profinite_obj' (X : CompHaus) :
↥(CompHaus.to_Profinite.obj X) = connected_components X.to_Top.α
source
@[instance]
def Profinite.to_CompHaus.reflective  :
category_theory.reflective Profinite.to_CompHaus

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

Equations