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

@[reducible, inline]

abbrev Profinite : Type (u_1 + 1)

The type of profinite topological spaces.

Equations

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

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

Equations

• ⋯ = ⋯

@[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_1 + 1} }

instance Profinite.instTotallyDisconnectedSpaceαTopologicalSpaceToTop {X : Profinite} : TotallyDisconnectedSpace ↑X.toTop

Equations

• ⋯ = ⋯

instance Profinite.instTotallyDisconnectedSpaceObjForget {X : Profinite} : TotallyDisconnectedSpace ((CategoryTheory.forget Profinite).obj X)

Equations

• ⋯ = ⋯

@[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 instTotallyDisconnectedSpaceαTopologicalSpaceToTopTrueObjProfiniteCompHausProfiniteToCompHaus {X : Profinite} : TotallyDisconnectedSpace ↑(profiniteToCompHaus.obj X).toTop

Equations

• ⋯ = ⋯

@[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. See: https://stacks.math.columbia.edu/tag/0900

Equations

• X.toProfiniteObj = CompHausLike.mk (TopCat.of (ConnectedComponents ↑X.toTop)) ⋯

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_1

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

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

Finite types are given the discrete topology.

Equations

• A.botTopology = ⊥

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

@[simp]

theorem FintypeCat.toProfinite_obj (A : FintypeCat) : FintypeCat.toProfinite.obj A = Profinite.of ↑A

@[simp]

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

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.

def FintypeCat.toProfiniteFullyFaithful : FintypeCat.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

Equations

• instFaithfulFintypeCatProfiniteToProfinite = ⋯

instance instFullFintypeCatProfiniteToProfinite : FintypeCat.toProfinite.Full

Equations

• instFullFintypeCatProfiniteToProfinite = ⋯

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 (Profinite.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_1

instance Profinite.toCompHaus.reflective : CategoryTheory.Reflective profiniteToCompHaus

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

Equations

• Profinite.toCompHaus.reflective = CategoryTheory.Reflective.mk CompHaus.toProfinite Profinite.toProfiniteAdjToCompHaus

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

Equations

• Profinite.toCompHaus.createsLimits = CategoryTheory.monadicCreatesLimits profiniteToCompHaus

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

Equations

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

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

Equations

• Profinite.toTopCat.createsLimits = CategoryTheory.monadicCreatesLimits Profinite.toTopCat

instance Profinite.hasLimits : CategoryTheory.Limits.HasLimits Profinite

Equations

• Profinite.hasLimits = ⋯

instance Profinite.hasColimits : CategoryTheory.Limits.HasColimits Profinite

Equations

• Profinite.hasColimits = ⋯

noncomputable instance Profinite.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget Profinite)

Equations

• Profinite.forgetPreservesLimits = CategoryTheory.Limits.compPreservesLimits Profinite.toTopCat (CategoryTheory.forget TopCat)

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