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.

The category Profinite is defined using the structure CompHausLike. See the file CompHausLike.Basic for more information.

TODO

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

Tags

profinite

@[reducible, inline]

abbrev Profinite : Type (u_1 + 1)

The type of profinite topological spaces.

instance Profinite.instHasPropTotallyDisconnectedSpaceCarrier (X : Type u_1) [TopologicalSpace X] [TotallyDisconnectedSpace X] : CompHausLike.HasProp (fun (Y : TopCat) => TotallyDisconnectedSpace ↑Y) X

@[reducible, inline]

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

@[implicit_reducible]

instance Profinite.instInhabited : Inhabited Profinite

instance Profinite.instTotallyDisconnectedSpaceCarrierToTop {X : Profinite} : TotallyDisconnectedSpace ↑X.toTop

@[reducible, inline]

abbrev profiniteToCompHaus : CategoryTheory.Functor Profinite CompHaus

The fully faithful embedding of Profinite in CompHaus.

instance instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus {X : Profinite} : TotallyDisconnectedSpace ↑(profiniteToCompHaus.obj X).toTop

@[reducible, inline]

abbrev Profinite.toTopCat : CategoryTheory.Functor Profinite TopCat

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

def CompHaus.toProfiniteObj (X : CompHaus) : Profinite

(Implementation) The object part of the connectedComponents functor from compact Hausdorff spaces to Profinite spaces, given by quotienting a space by its connected components.

def Profinite.toCompHausEquivalence (X : CompHaus) (Y : Profinite) : (X.toProfiniteObj ⟶ Y) ≃ (X ⟶ profiniteToCompHaus.obj Y)

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

def CompHaus.toProfinite : CategoryTheory.Functor CompHaus Profinite

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

theorem CompHaus.toProfinite_obj' (X : CompHaus) : ↑(toProfinite.obj X).toTop = ConnectedComponents ↑X.toTop

@[implicit_reducible]

def FintypeCat.botTopology (A : FintypeCat) : TopologicalSpace A.obj

Finite types are given the discrete topology.

theorem FintypeCat.discreteTopology (A : FintypeCat) : DiscreteTopology A.obj

def FintypeCat.toProfinite : CategoryTheory.Functor FintypeCat Profinite

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

theorem FintypeCat.toProfinite_map_hom_hom_apply {X✝ Y✝ : FintypeCat} (f : X✝ ⟶ Y✝) (a : X✝.obj) : (TopCat.Hom.hom (toProfinite.map f).hom) a = (CategoryTheory.ConcreteCategory.hom f) a

def FintypeCat.toProfiniteFullyFaithful : toProfinite.FullyFaithful

FintypeCat.toLightProfinite is fully faithful.

instance instFaithfulFintypeCatProfiniteToProfinite : FintypeCat.toProfinite.Faithful

instance instFullFintypeCatProfiniteToProfinite : FintypeCat.toProfinite.Full

instance instFiniteCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite (X : FintypeCat) : Finite ↑(FintypeCat.toProfinite.obj X).toTop

instance instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj (X : FintypeCat) : Finite ↑(Profinite.of X.obj).toTop

def Profinite.limitCone {J : Type v} [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.

def Profinite.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J Profinite) : CategoryTheory.Limits.IsLimit (limitCone F)

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

def Profinite.toProfiniteAdjToCompHaus : CompHaus.toProfinite ⊣ profiniteToCompHaus

The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus

@[implicit_reducible]

instance Profinite.toCompHaus.reflective : CategoryTheory.Reflective profiniteToCompHaus

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

@[implicit_reducible]

noncomputable instance Profinite.toCompHaus.createsLimits : CategoryTheory.CreatesLimits profiniteToCompHaus

@[implicit_reducible]

noncomputable instance Profinite.toTopCat.reflective : CategoryTheory.Reflective toTopCat

@[implicit_reducible]

noncomputable instance Profinite.toTopCat.createsLimits : CategoryTheory.CreatesLimits toTopCat

instance Profinite.hasLimits : CategoryTheory.Limits.HasLimits Profinite

instance Profinite.hasColimits : CategoryTheory.Limits.HasColimits Profinite

instance Profinite.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget Profinite)

theorem Profinite.epi_iff_surjective {X Y : Profinite} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)

def Profinite.pi {α : Type u} (β : α → Profinite) : Profinite

The pi-type of profinite spaces is profinite.