mathlibdocumentation

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)
• to_CompHaus : CompHaus
• is_totally_disconnected :

The type of profinite topological spaces.

Instances for Profinite
def Profinite.of (X : Type u_1) [t2_space X]  :

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

Equations
Instances for Profinite.of
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def Profinite.has_coe_to_sort  :
(Type u_1)
Equations
@[protected, instance]
@[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
@[protected, instance]
@[simp]
@[simp]
theorem Profinite_to_CompHaus_map (f : x y) :
@[protected, instance]

The fully faithful embedding of Profinite in CompHaus.

Equations
Instances for Profinite_to_CompHaus
@[simp]
theorem Profinite.to_Top_map (f : x y) :
@[protected, instance]
@[simp]

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

Equations
Instances for Profinite.to_Top
@[protected, instance]
@[simp]

(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.α) :
= f ᾰ

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

Equations
@[simp]
def Profinite.limit_cone {J : Type u} (F : J Profinite) :

An explicit limit cone for a functor F : J ⥤ Profinite, defined in terms of Top.limit_cone.

Equations
def Profinite.limit_cone_is_limit {J : Type u} (F : J Profinite) :

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

Equations

The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus

Equations
@[protected, instance]

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

Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def Profinite.to_Top.reflective  :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
theorem Profinite.is_closed_map {X Y : Profinite} (f : X Y) :

Any morphism of profinite spaces is a closed map.

theorem Profinite.is_iso_of_bijective {X Y : Profinite} (f : X Y) (bij : function.bijective f) :

Any continuous bijection of profinite spaces induces an isomorphism.

noncomputable 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
• = let _inst : := _ in
@[protected, instance]
def Profinite.iso_of_homeo {X Y : Profinite} (f : X ≃ₜ Y) :
X Y

Construct an isomorphism from a homeomorphism.

Equations
@[simp]
@[simp]
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)) :
.symm) = (f.inv) ᾰ
@[simp]
theorem Profinite.homeo_of_iso_apply {X Y : Profinite} (f : X Y) (ᾰ : (X.to_CompHaus.to_Top)) :
= (f.hom) ᾰ
@[simp]

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

Equations
@[simp]
theorem Profinite.iso_equiv_homeo_apply {X Y : Profinite} (f : X Y) :
theorem Profinite.epi_iff_surjective {X Y : Profinite} (f : X Y) :
theorem Profinite.mono_iff_injective {X Y : Profinite} (f : X Y) :