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 #

Link to category of projective limits of finite discrete sets.
finite coproducts
Clausen/Scholze topology on the category Profinite.

Tags #

profinite

source

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

source

def Profinite.of (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] :

Profinite

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

Instances For

source

instance Profinite.instInhabitedProfinite :

Inhabited Profinite

source

instance Profinite.category :

CategoryTheory.Category.{u_1, u_1 + 1} Profinite

source

instance Profinite.concreteCategory :

CategoryTheory.ConcreteCategory Profinite

source

instance Profinite.hasForget₂ :

CategoryTheory.HasForget₂ Profinite TopCat

source

instance Profinite.instCoeSortProfiniteType :

CoeSort Profinite (Type u_1)

source

@[simp]

theorem Profinite.forget_ContinuousMap_mk {X : Profinite} {Y : Profinite} (f : ↑X.toCompHaus.toTop → ↑Y.toCompHaus.toTop) (hf : Continuous f) :

(CategoryTheory.forget Profinite).map (ContinuousMap.mk f) = f

source

instance Profinite.instTotallyDisconnectedSpaceαTopologicalSpaceToTopToCompHausTopologicalSpace_coe {X : Profinite} :

TotallyDisconnectedSpace ↑X.toCompHaus.toTop

source

instance Profinite.instTopologicalSpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory {X : Profinite} :

TopologicalSpace ((CategoryTheory.forget Profinite).obj X)

source

instance Profinite.instTotallyDisconnectedSpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategoryInstTopologicalSpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory {X : Profinite} :

TotallyDisconnectedSpace ((CategoryTheory.forget Profinite).obj X)

source

instance Profinite.instCompactSpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategoryInstTopologicalSpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory {X : Profinite} :

CompactSpace ((CategoryTheory.forget Profinite).obj X)

source

instance Profinite.instT2SpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategoryInstTopologicalSpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory {X : Profinite} :

T2Space ((CategoryTheory.forget Profinite).obj X)

source

@[simp]

theorem Profinite.coe_id (X : Profinite) :

CategoryTheory.CategoryStruct.id ((CategoryTheory.forget Profinite).obj X) = id

source

@[simp]

theorem Profinite.coe_comp {X : Profinite} {Y : Profinite} {Z : Profinite} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget Profinite).map f) ((CategoryTheory.forget Profinite).map g) = ↑g ∘ ↑f

source

@[simp]

theorem profiniteToCompHaus_obj (self : Profinite) :

profiniteToCompHaus.obj self = self.toCompHaus

source

@[simp]

theorem profiniteToCompHaus_map :

∀ {X Y : CategoryTheory.InducedCategory CompHaus Profinite.toCompHaus} (f : X ⟶ Y), profiniteToCompHaus.map f = f

source

def profiniteToCompHaus :

CategoryTheory.Functor Profinite CompHaus

The fully faithful embedding of Profinite in CompHaus.

Instances For

source

instance instFullProfiniteCategoryCompHausCategoryProfiniteToCompHaus :

CategoryTheory.Full profiniteToCompHaus

source

instance instFaithfulProfiniteCategoryCompHausCategoryProfiniteToCompHaus :

CategoryTheory.Faithful profiniteToCompHaus

source

instance instTotallyDisconnectedSpaceαTopologicalSpaceToTopObjProfiniteToQuiverToCategoryStructCategoryCompHausCategoryToPrefunctorProfiniteToCompHausTopologicalSpace_coe {X : Profinite} :

TotallyDisconnectedSpace ↑(profiniteToCompHaus.obj X).toTop

source

@[simp]

theorem Profinite.toTopCat_obj (X : CategoryTheory.InducedCategory CompHaus Profinite.toCompHaus) :

Profinite.toTopCat.obj X = X.toCompHaus.toTop

source

@[simp]

theorem Profinite.toTopCat_map :

∀ {X Y : CategoryTheory.InducedCategory TopCat fun X => X.toCompHaus.toTop} (f : X ⟶ Y), Profinite.toTopCat.map f = f

source

def Profinite.toTopCat :

CategoryTheory.Functor Profinite TopCat

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

Instances For

source

instance instFullProfiniteCategoryTopCatInstTopCatLargeCategoryToTopCat :

CategoryTheory.Full Profinite.toTopCat

source

instance instFaithfulProfiniteCategoryTopCatInstTopCatLargeCategoryToTopCat :

CategoryTheory.Faithful Profinite.toTopCat

source

@[simp]

theorem Profinite.to_compHausToTopCat :

CategoryTheory.Functor.comp profiniteToCompHaus compHausToTop = Profinite.toTopCat

source

def CompHaus.toProfiniteObj (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

Instances For

source

def Profinite.toCompHausEquivalence (X : CompHaus) (Y : Profinite) :

(CompHaus.toProfiniteObj X ⟶ Y) ≃ (X ⟶ profiniteToCompHaus.obj Y)

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

Instances For

source

def CompHaus.toProfinite :

CategoryTheory.Functor CompHaus Profinite

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

Instances For

source

theorem CompHaus.toProfinite_obj' (X : CompHaus) :

↑(CompHaus.toProfinite.obj X).toCompHaus.toTop = ConnectedComponents ↑X.toTop

source

def FintypeCat.botTopology (A : FintypeCat) :

TopologicalSpace ↑A

Finite types are given the discrete topology.

Instances For

source

theorem FintypeCat.discreteTopology (A : FintypeCat) :

DiscreteTopology ↑A

source

@[simp]

theorem FintypeCat.toProfinite_map_apply :

∀ {X Y : FintypeCat} (f : X ⟶ Y) (a : ↑X), ↑(FintypeCat.toProfinite.map f) a = f a

source

@[simp]

theorem FintypeCat.toProfinite_obj_toCompHaus_toTop_str_IsOpen (A : FintypeCat) (u : Set ↑A) :

TopologicalSpace.IsOpen u = (u ∈ ⊤)

source

@[simp]

theorem FintypeCat.toProfinite_obj_toCompHaus_toTop_α (A : FintypeCat) :

↑(FintypeCat.toProfinite.obj A).toCompHaus.toTop = ↑A

source

def FintypeCat.toProfinite :

CategoryTheory.Functor FintypeCat Profinite

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

Instances For

source

def Profinite.limitCone {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J Profinite) :

CategoryTheory.Limits.Cone 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

source

def Profinite.limitConeIsLimit {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J Profinite) :

CategoryTheory.Limits.IsLimit (Profinite.limitCone F)

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

Instances For

source

def Profinite.toProfiniteAdjToCompHaus :

CompHaus.toProfinite ⊣ profiniteToCompHaus

The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus

Instances For

source

instance Profinite.toCompHaus.reflective :

CategoryTheory.Reflective profiniteToCompHaus

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

source

noncomputable instance Profinite.toCompHaus.createsLimits :

CategoryTheory.CreatesLimits profiniteToCompHaus

source

noncomputable instance Profinite.toTopCat.reflective :

CategoryTheory.Reflective Profinite.toTopCat

source

noncomputable instance Profinite.toTopCat.createsLimits :

CategoryTheory.CreatesLimits Profinite.toTopCat

source

instance Profinite.hasLimits :

CategoryTheory.Limits.HasLimits Profinite

source

instance Profinite.hasColimits :

CategoryTheory.Limits.HasColimits Profinite

source

noncomputable instance Profinite.forgetPreservesLimits :

CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget Profinite)

source

theorem Profinite.isClosedMap {X : Profinite} {Y : Profinite} (f : X ⟶ Y) :

IsClosedMap ↑f

Any morphism of profinite spaces is a closed map.

source

theorem Profinite.isIso_of_bijective {X : Profinite} {Y : Profinite} (f : X ⟶ Y) (bij : Function.Bijective ↑f) :

CategoryTheory.IsIso f

Any continuous bijection of profinite spaces induces an isomorphism.

source

noncomputable def Profinite.isoOfBijective {X : Profinite} {Y : Profinite} (f : X ⟶ Y) (bij : Function.Bijective ↑f) :

X ≅ Y

Any continuous bijection of profinite spaces induces an isomorphism.

Instances For

source

instance Profinite.forget_reflectsIsomorphisms :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget Profinite)

source

@[simp]

theorem Profinite.isoOfHomeo_hom {X : Profinite} {Y : Profinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) :

(Profinite.isoOfHomeo f).hom = ContinuousMap.mk ↑f

source

@[simp]

theorem Profinite.isoOfHomeo_inv {X : Profinite} {Y : Profinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) :

(Profinite.isoOfHomeo f).inv = CategoryTheory.inv (ContinuousMap.mk ↑f)

source

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

source

@[simp]

theorem Profinite.homeoOfIso_symm_apply {X : Profinite} {Y : Profinite} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj Y.toCompHaus) :

↑(Homeomorph.symm (Profinite.homeoOfIso f)) a = ↑f.inv a

source

@[simp]

theorem Profinite.homeoOfIso_apply {X : Profinite} {Y : Profinite} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj X.toCompHaus) :

↑(Profinite.homeoOfIso f) a = ↑f.hom a

source

def Profinite.homeoOfIso {X : Profinite} {Y : Profinite} (f : X ≅ Y) :

↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop

Construct a homeomorphism from an isomorphism.

Instances For

source

@[simp]

theorem Profinite.isoEquivHomeo_symm_apply_inv {X : Profinite} {Y : Profinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) :

(↑Profinite.isoEquivHomeo.symm f).inv = CategoryTheory.inv (ContinuousMap.mk ↑f)

source

@[simp]

theorem Profinite.isoEquivHomeo_apply_apply {X : Profinite} {Y : Profinite} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj X.toCompHaus) :

↑(↑Profinite.isoEquivHomeo f) a = ↑f.hom a

source

@[simp]

theorem Profinite.isoEquivHomeo_apply_symm_apply {X : Profinite} {Y : Profinite} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj Y.toCompHaus) :

↑(Homeomorph.symm (↑Profinite.isoEquivHomeo f)) a = ↑f.inv a

source

@[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

source

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

source

theorem Profinite.epi_iff_surjective {X : Profinite} {Y : Profinite} (f : X ⟶ Y) :

CategoryTheory.Epi f ↔ Function.Surjective ↑f

source

instance Profinite.instEpiCompHausCategoryToCompHaus {X : Profinite} {Y : Profinite} (f : X ⟶ Y) [CategoryTheory.Epi f] :

CategoryTheory.Epi f

source

instance Profinite.instEpiProfiniteCategory {X : Profinite} {Y : Profinite} (f : X ⟶ Y) [CategoryTheory.Epi f] :

CategoryTheory.Epi f

source

theorem Profinite.mono_iff_injective {X : Profinite} {Y : Profinite} (f : X ⟶ Y) :

CategoryTheory.Mono f ↔ Function.Injective ↑f