mathlib3 documentation

topology.category.Profinite.basic

The category of Profinite Types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
structure Profinite  :
Type (u_1+1)

The type of profinite topological spaces.

Instances for Profinite
source
def Profinite.of (X : Type u_1) [topological_space X] [compact_space X] [t2_space X] [totally_disconnected_space X] :
Profinite

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
source
@[protected, instance]
def Profinite.inhabited  :
inhabited Profinite
Equations
source
@[protected, instance]
def Profinite.category  :
category_theory.category Profinite
Equations
source
@[protected, instance]
def Profinite.concrete_category  :
category_theory.concrete_category Profinite
Equations
source
@[protected, instance]
def Profinite.has_forget₂  :
category_theory.has_forget₂ Profinite Top
Equations
source
@[protected, instance]
def Profinite.has_coe_to_sort  :
has_coe_to_sort Profinite (Type u_1)
Equations
source
@[protected, instance]
def Profinite.totally_disconnected_space {X : Profinite} :
totally_disconnected_space ↥X
source
@[simp]
theorem Profinite.coe_to_CompHaus {X : Profinite} :
↥(X.to_CompHaus) = ↥X
source
@[simp]
theorem Profinite.coe_id (X : Profinite) :
⇑(𝟙 X) = id
source
@[simp]
theorem Profinite.coe_comp {X Y Z : Profinite} (f : X ⟶ Y) (g : Y ⟶ Z) :
⇑(f ≫ g) = ⇑g ∘ ⇑f
source
@[protected, instance]
def Profinite_to_CompHaus.full  :
category_theory.full Profinite_to_CompHaus
source
@[simp]
theorem Profinite_to_CompHaus_obj (self : Profinite) :
Profinite_to_CompHaus.obj self = self.to_CompHaus
source
@[simp]
theorem Profinite_to_CompHaus_map (x y : category_theory.induced_category CompHaus Profinite.to_CompHaus) (f : x ⟶ y) :
Profinite_to_CompHaus.map f = f
source
@[protected, instance]
def Profinite_to_CompHaus.faithful  :
category_theory.faithful Profinite_to_CompHaus
source
def Profinite_to_CompHaus  :
Profinite ⥤ CompHaus

The fully faithful embedding of Profinite in CompHaus.

Equations
Instances for Profinite_to_CompHaus
source
@[simp]
theorem Profinite.to_Top_map (x y : category_theory.induced_category Top (λ (X : category_theory.induced_category CompHaus Profinite.to_CompHaus), X.to_CompHaus.to_Top)) (f : x ⟶ y) :
Profinite.to_Top.map f = f
source
@[protected, instance]
def Profinite.to_Top.faithful  :
category_theory.faithful Profinite.to_Top
source
@[simp]
theorem Profinite.to_Top_obj (X : category_theory.induced_category CompHaus Profinite.to_CompHaus) :
Profinite.to_Top.obj X = X.to_CompHaus.to_Top
source
def Profinite.to_Top  :
Profinite ⥤ Top

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

Equations
Instances for Profinite.to_Top
source
@[protected, instance]
def Profinite.to_Top.full  :
category_theory.full Profinite.to_Top
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
theorem CompHaus.to_Profinite_obj' (X : CompHaus) :
↥(CompHaus.to_Profinite.obj X) = connected_components ↥X
source
def Fintype.bot_topology (A : Fintype) :
topological_space ↥A

Finite types are given the discrete topology.

Equations
source
theorem Fintype.discrete_topology (A : Fintype) :
discrete_topology ↥A
source
@[simp]
theorem Fintype.to_Profinite_map_apply (_x _x_1 : Fintype) (f : _x ⟶ _x_1) (ᾰ : _x.α) :
⇑(Fintype.to_Profinite.map f) ᾰ = f ᾰ
source
def Fintype.to_Profinite  :
Fintype ⥤ Profinite

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

Equations
source
@[simp]
theorem Fintype.to_Profinite_obj (A : Fintype) :
Fintype.to_Profinite.obj A = Profinite.of ↥A
source
def Profinite.limit_cone {J : Type u} [category_theory.small_category J] (F : J ⥤ Profinite) :
category_theory.limits.cone F

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

Equations
source
def Profinite.limit_cone_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ Profinite) :
category_theory.limits.is_limit (Profinite.limit_cone F)

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

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
@[protected, 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
source
@[protected, instance]
noncomputable def Profinite.to_CompHaus.creates_limits  :
category_theory.creates_limits Profinite_to_CompHaus
Equations
source
@[protected, instance]
noncomputable def Profinite.to_Top.reflective  :
category_theory.reflective Profinite.to_Top
Equations
source
@[protected, instance]
noncomputable def Profinite.to_Top.creates_limits  :
category_theory.creates_limits Profinite.to_Top
Equations
source
@[protected, instance]
def Profinite.has_limits  :
category_theory.limits.has_limits Profinite
source
@[protected, instance]
def Profinite.has_colimits  :
category_theory.limits.has_colimits Profinite
source
@[protected, instance]
noncomputable def Profinite.forget_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget Profinite)
Equations
source
theorem Profinite.is_closed_map {X Y : Profinite} (f : X ⟶ Y) :
is_closed_map ⇑f

Any morphism of profinite spaces is a closed map.

source
theorem Profinite.is_iso_of_bijective {X Y : Profinite} (f : X ⟶ Y) (bij : function.bijective ⇑f) :
category_theory.is_iso f

Any continuous bijection of profinite spaces induces an isomorphism.

source
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
source
@[protected, instance]
def Profinite.forget_reflects_isomorphisms  :
category_theory.reflects_isomorphisms (category_theory.forget Profinite)
source
def Profinite.iso_of_homeo {X Y : Profinite} (f : ↥X ≃ₜ ↥Y) :
X ≅ Y

Construct an isomorphism from a homeomorphism.

Equations
source
@[simp]
theorem Profinite.iso_of_homeo_inv {X Y : Profinite} (f : ↥X ≃ₜ ↥Y) :
(Profinite.iso_of_homeo f).inv = {to_fun := ⇑(f.symm), continuous_to_fun := _}
source
@[simp]
theorem Profinite.iso_of_homeo_hom {X Y : Profinite} (f : ↥X ≃ₜ ↥Y) :
(Profinite.iso_of_homeo f).hom = {to_fun := ⇑f, continuous_to_fun := _}
source
def Profinite.homeo_of_iso {X Y : Profinite} (f : X ≅ Y) :
↥X ≃ₜ ↥Y

Construct a homeomorphism from an isomorphism.

Equations
source
@[simp]
theorem Profinite.homeo_of_iso_symm_apply {X Y : Profinite} (f : X ≅ Y) (ᾰ : ↥(Y.to_CompHaus.to_Top)) :
⇑((Profinite.homeo_of_iso f).symm) ᾰ = ⇑(f.inv) ᾰ
source
@[simp]
theorem Profinite.homeo_of_iso_apply {X Y : Profinite} (f : X ≅ Y) (ᾰ : ↥(X.to_CompHaus.to_Top)) :
⇑(Profinite.homeo_of_iso f) ᾰ = ⇑(f.hom) ᾰ
source
@[simp]
theorem Profinite.iso_equiv_homeo_symm_apply {X Y : Profinite} (f : ↥X ≃ₜ ↥Y) :
⇑(Profinite.iso_equiv_homeo.symm) f = Profinite.iso_of_homeo f
source
def Profinite.iso_equiv_homeo {X Y : Profinite} :
(X ≅ Y) ≃ (↥X ≃ₜ ↥Y)

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

Equations
source
@[simp]
theorem Profinite.iso_equiv_homeo_apply {X Y : Profinite} (f : X ≅ Y) :
⇑Profinite.iso_equiv_homeo f = Profinite.homeo_of_iso f
source
theorem Profinite.epi_iff_surjective {X Y : Profinite} (f : X ⟶ Y) :
category_theory.epi f ↔ function.surjective ⇑f
source
theorem Profinite.mono_iff_injective {X Y : Profinite} (f : X ⟶ Y) :
category_theory.mono f ↔ function.injective ⇑f