# Documentation

Mathlib.Topology.Category.Profinite.Basic

# 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 TopCat. The fully faithful functor is called Profinite.toTop.

## 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)
• toCompHaus : CompHaus

The underlying compact Hausdorff space of a profinite space.

• IsTotallyDisconnected : TotallyDisconnectedSpace s.toCompHaus.toTop

A profinite space is totally disconnected.

The type of profinite topological spaces.

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

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

Instances For
@[simp]
theorem Profinite.forget_ContinuousMap_mk {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTopY.toCompHaus.toTop) (hf : ) :
().map () = f
@[simp]
theorem Profinite.coe_id (X : Profinite) :
@[simp]
theorem Profinite.coe_comp {X : Profinite} {Y : Profinite} {Z : Profinite} (f : X Y) (g : Y Z) :
= g f
@[simp]
theorem profiniteToCompHaus_obj (self : Profinite) :
profiniteToCompHaus.obj self = self.toCompHaus
@[simp]
theorem profiniteToCompHaus_map :
∀ {X Y : } (f : X Y), profiniteToCompHaus.map f = f

The fully faithful embedding of Profinite in CompHaus.

Instances For
@[simp]
theorem Profinite.toTopCat_obj :
Profinite.toTopCat.obj X = X.toCompHaus.toTop
@[simp]
theorem Profinite.toTopCat_map :
∀ {X Y : CategoryTheory.InducedCategory TopCat fun X => X.toCompHaus.toTop} (f : X Y), Profinite.toTopCat.map f = f

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

Instances For

(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

Instances For

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

Instances For

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

Instances For
theorem CompHaus.toProfinite_obj' (X : CompHaus) :
(CompHaus.toProfinite.obj X).toCompHaus.toTop = ConnectedComponents X.toTop

Finite types are given the discrete topology.

Instances For
@[simp]
theorem FintypeCat.toProfinite_map_apply :
∀ {X Y : FintypeCat} (f : X Y) (a : X), ↑() a = f a
@[simp]
theorem FintypeCat.toProfinite_obj_toCompHaus_toTop_α (A : FintypeCat) :
().toCompHaus.toTop = A

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

Instances For
def Profinite.limitCone {J : Type u} (F : ) :

An explicit limit cone for a functor F : J ⥤ Profinite, defined in terms of CompHaus.limitCone, which is defined in terms of TopCat.limitCone.

Instances For

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

Instances For

The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus

Instances For

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

noncomputable instance Profinite.toTopCat.reflective :
noncomputable instance Profinite.forgetPreservesLimits :
theorem Profinite.isClosedMap {X : Profinite} {Y : Profinite} (f : X Y) :

Any morphism of profinite spaces is a closed map.

theorem Profinite.isIso_of_bijective {X : Profinite} {Y : Profinite} (f : X Y) (bij : ) :

Any continuous bijection of profinite spaces induces an isomorphism.

noncomputable def Profinite.isoOfBijective {X : Profinite} {Y : Profinite} (f : X Y) (bij : ) :
X Y

Any continuous bijection of profinite spaces induces an isomorphism.

Instances For
@[simp]
theorem Profinite.isoOfHomeo_hom {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
().hom =
@[simp]
theorem Profinite.isoOfHomeo_inv {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
().inv =
noncomputable def Profinite.isoOfHomeo {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
X Y

Construct an isomorphism from a homeomorphism.

Instances For
@[simp]
theorem Profinite.homeoOfIso_symm_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : ().obj Y.toCompHaus) :
↑() a = f.inv a
@[simp]
theorem Profinite.homeoOfIso_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : ().obj X.toCompHaus) :
↑() a = f.hom a
def Profinite.homeoOfIso {X : Profinite} {Y : Profinite} (f : X Y) :
X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop

Construct a homeomorphism from an isomorphism.

Instances For
@[simp]
theorem Profinite.isoEquivHomeo_symm_apply_inv {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) :
(Profinite.isoEquivHomeo.symm f).inv =
@[simp]
theorem Profinite.isoEquivHomeo_apply_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : ().obj X.toCompHaus) :
↑(Profinite.isoEquivHomeo f) a = f.hom a
@[simp]
theorem Profinite.isoEquivHomeo_apply_symm_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : ().obj Y.toCompHaus) :
↑(Homeomorph.symm (Profinite.isoEquivHomeo f)) a = f.inv a
@[simp]
theorem Profinite.isoEquivHomeo_symm_apply_hom_apply {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop) (a : X.toCompHaus.toTop) :
(Profinite.isoEquivHomeo.symm f).hom a = f a
noncomputable def Profinite.isoEquivHomeo {X : Profinite} {Y : Profinite} :
(X Y) (X.toCompHaus.toTop ≃ₜ Y.toCompHaus.toTop)

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

Instances For