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 #

• Define procategories and prove that Profinite is equivalent to Pro (FintypeCat).

Tags #

profinite

structure Profinite :
Type (u_1 + 1)

The type of profinite topological spaces.

• toCompHaus : CompHaus

The underlying compact Hausdorff space of a profinite space.

• isTotallyDisconnected : TotallyDisconnectedSpace self.toCompHaus.toTop

A profinite space is totally disconnected.

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.

Equations
Instances For
Equations
@[simp]
theorem Profinite.forget_ContinuousMap_mk {X : Profinite} {Y : Profinite} (f : X.toCompHaus.toTopY.toCompHaus.toTop) (hf : ) :
{ toFun := f, continuous_toFun := hf } = f
Equations
• Profinite.instTopologicalSpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory = let_fun this := inferInstance; this
@[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) :
self = self.toCompHaus
@[simp]
theorem profiniteToCompHaus_map :
∀ {X Y : } (f : X Y), f = f

The fully faithful embedding of Profinite in CompHaus.

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

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

Equations
Instances For
Equations

(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
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

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

Finite types are given the discrete topology.

Equations
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[inline, reducible]
abbrev ProfiniteMax :
Type ((max w w') + 1)

Many definitions involving universe inequalities in Mathlib are expressed through use of max u v. Unfortunately, this leads to unbound universes which cannot be solved for during unification, eg max u v =?= max v ?. The current solution is to wrap Type max u v in TypeMax.{u,v} to expose both universe parameters directly.

Similarly, for other concrete categories for which we need to refer to the maximum of two universes (e.g. any category for which we are constructing limits), we need an analogous abbreviation.

Equations
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus

Equations
Instances For

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

Equations
Equations
Equations
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.

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

Construct an isomorphism from a homeomorphism.

Equations
Instances For
@[simp]
theorem Profinite.homeoOfIso_symm_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : Y.toCompHaus) :
= f.inv a
@[simp]
theorem Profinite.homeoOfIso_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : 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.

Equations
Instances For
@[simp]
theorem Profinite.isoEquivHomeo_apply_symm_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : 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
@[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 { toFun := f, continuous_toFun := }
@[simp]
theorem Profinite.isoEquivHomeo_apply_apply {X : Profinite} {Y : Profinite} (f : X Y) (a : X.toCompHaus) :
(Profinite.isoEquivHomeo f) a = f.hom 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.

Equations
• Profinite.isoEquivHomeo = { toFun := Profinite.homeoOfIso, invFun := Profinite.isoOfHomeo, left_inv := , right_inv := }
Instances For
Equations
• =
Equations
• =