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.

Equations

• Profinite = CompHausLike fun (X : TopCat) => TotallyDisconnectedSpace ↑X

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.

Equations

• Profinite.of X = CompHausLike.of (fun (X : TopCat) => TotallyDisconnectedSpace ↑X) X

instance Profinite.instInhabited : Inhabited Profinite

Equations

• Profinite.instInhabited = { default := Profinite.of PEmpty.{?u.2 + 1} }

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

@[reducible, inline]

abbrev profiniteToCompHaus : CategoryTheory.Functor Profinite CompHaus

The fully faithful embedding of Profinite in CompHaus.

Equations

• profiniteToCompHaus = compHausLikeToCompHaus fun (X : TopCat) => TotallyDisconnectedSpace ↑X

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.

Equations

• Profinite.toTopCat = CompHausLike.compHausLikeToTop fun (X : TopCat) => TotallyDisconnectedSpace ↑X

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.

Stacks Tag 0900

Equations

• X.toProfiniteObj = { toTop := TopCat.of (ConnectedComponents ↑X.toTop), is_compact := ⋯, is_hausdorff := ⋯, prop := ⋯ }

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.

Equations

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

def CompHaus.toProfinite : CategoryTheory.Functor CompHaus Profinite

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

Equations

• CompHaus.toProfinite = CategoryTheory.Adjunction.leftAdjointOfEquiv Profinite.toCompHausEquivalence CompHaus.toProfinite._proof_20

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

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

Finite types are given the discrete topology.

Equations

• A.botTopology = ⊥

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

def FintypeCat.toProfinite : CategoryTheory.Functor FintypeCat Profinite

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.

theorem FintypeCat.toProfinite_map_hom_apply {X✝ Y✝ : FintypeCat} (f : X✝ ⟶ Y✝) (a✝ : X✝.carrier) : (TopCat.Hom.hom (toProfinite.map f)) a✝ = f a✝

def FintypeCat.toProfiniteFullyFaithful : toProfinite.FullyFaithful

FintypeCat.toLightProfinite is fully faithful.

Equations

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

instance instFaithfulFintypeCatProfiniteToProfinite : FintypeCat.toProfinite.Faithful

instance instFullFintypeCatProfiniteToProfinite : FintypeCat.toProfinite.Full

instance instFintypeCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite (X : FintypeCat) : Fintype ↑(FintypeCat.toProfinite.obj X).toTop

Equations

• instFintypeCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite X = inferInstanceAs (Fintype X.carrier)

instance instFintypeCarrierToTopTotallyDisconnectedSpaceOfCarrier (X : FintypeCat) : Fintype ↑(Profinite.of X.carrier).toTop

Equations

• instFintypeCarrierToTopTotallyDisconnectedSpaceOfCarrier X = inferInstanceAs (Fintype X.carrier)

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.

Equations

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

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.

Equations

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

def Profinite.toProfiniteAdjToCompHaus : CompHaus.toProfinite ⊣ profiniteToCompHaus

The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus

Equations

• Profinite.toProfiniteAdjToCompHaus = CategoryTheory.Adjunction.adjunctionOfEquivLeft Profinite.toCompHausEquivalence CompHaus.toProfinite._proof_20

instance Profinite.toCompHaus.reflective : CategoryTheory.Reflective profiniteToCompHaus

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

Equations

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

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

Equations

• Profinite.toCompHaus.createsLimits = CategoryTheory.monadicCreatesLimits profiniteToCompHaus

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

Equations

• Profinite.toTopCat.reflective = CategoryTheory.Reflective.comp profiniteToCompHaus compHausToTop

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

Equations

• Profinite.toTopCat.createsLimits = CategoryTheory.monadicCreatesLimits Profinite.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.

Equations

• Profinite.pi β = Profinite.of ((a : α) → ↑(β a).toTop)