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.

theorem Profinite.isTotallyDisconnected (self : Profinite) : TotallyDisconnectedSpace ↑self.toCompHaus.toTop

A profinite space is totally disconnected.

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.

Equations

• Profinite.of X = Profinite.mk (CompHaus.mk { α := X, str := inferInstance })

instance Profinite.instInhabited : Inhabited Profinite

Equations

• Profinite.instInhabited = { default := Profinite.of PEmpty.{u_1 + 1} }

instance Profinite.category : CategoryTheory.Category.{u_1, u_1 + 1} Profinite

Equations

• Profinite.category = CategoryTheory.InducedCategory.category Profinite.toCompHaus

instance Profinite.concreteCategory : CategoryTheory.ConcreteCategory Profinite

Equations

• Profinite.concreteCategory = CategoryTheory.InducedCategory.concreteCategory Profinite.toCompHaus

instance Profinite.hasForget₂ : CategoryTheory.HasForget₂ Profinite TopCat

Equations

• Profinite.hasForget₂ = CategoryTheory.InducedCategory.hasForget₂ fun (X : CategoryTheory.InducedCategory CompHaus Profinite.toCompHaus) => X.toCompHaus.toTop

instance Profinite.instCoeSortType : CoeSort Profinite (Type u_1)

Equations

• Profinite.instCoeSortType = { coe := fun (X : Profinite) => ↑X.toCompHaus.toTop }

@[simp]

theorem Profinite.forget_ContinuousMap_mk {X : Profinite} {Y : Profinite} (f : ↑X.toCompHaus.toTop → ↑Y.toCompHaus.toTop) (hf : Continuous f) : (CategoryTheory.forget Profinite).map { toFun := f, continuous_toFun := hf } = f

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

Equations

• ⋯ = ⋯

instance Profinite.instTopologicalSpaceObjForget {X : Profinite} : TopologicalSpace ((CategoryTheory.forget Profinite).obj X)

Equations

• Profinite.instTopologicalSpaceObjForget = let_fun this := inferInstance; this

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

Equations

• ⋯ = ⋯

instance Profinite.instCompactSpaceObjForget {X : Profinite} : CompactSpace ((CategoryTheory.forget Profinite).obj X)

Equations

• ⋯ = ⋯

instance Profinite.instT2SpaceObjForget {X : Profinite} : T2Space ((CategoryTheory.forget Profinite).obj X)

Equations

• ⋯ = ⋯

@[simp]

theorem Profinite.coe_id (X : Profinite) : CategoryTheory.CategoryStruct.id ((CategoryTheory.forget Profinite).obj X) = id

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

@[simp]

theorem profiniteToCompHaus_obj (self : Profinite) : profiniteToCompHaus.obj self = self.toCompHaus

@[simp]

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

def profiniteToCompHaus : CategoryTheory.Functor Profinite CompHaus

The fully faithful embedding of Profinite in CompHaus.

Equations

• profiniteToCompHaus = CategoryTheory.inducedFunctor Profinite.toCompHaus

instance instFullProfiniteCompHausProfiniteToCompHaus : profiniteToCompHaus.Full

Equations

• instFullProfiniteCompHausProfiniteToCompHaus = ⋯

instance instFaithfulProfiniteCompHausProfiniteToCompHaus : profiniteToCompHaus.Faithful

Equations

• instFaithfulProfiniteCompHausProfiniteToCompHaus = ⋯

instance instTotallyDisconnectedSpaceαTopologicalSpaceToTopObjProfiniteCompHausProfiniteToCompHaus {X : Profinite} : TotallyDisconnectedSpace ↑(profiniteToCompHaus.obj X).toTop

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

theorem Profinite.toTopCat_obj (X : CategoryTheory.InducedCategory CompHaus Profinite.toCompHaus) : Profinite.toTopCat.obj X = X.toCompHaus.toTop

def 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 = CategoryTheory.forget₂ Profinite TopCat

instance instFullProfiniteTopCatToTopCat : Profinite.toTopCat.Full

Equations

• instFullProfiniteTopCatToTopCat = ⋯

instance instFaithfulProfiniteTopCatToTopCat : Profinite.toTopCat.Faithful

Equations

• instFaithfulProfiniteTopCatToTopCat = ⋯

@[simp]

theorem Profinite.to_compHausToTopCat : profiniteToCompHaus.comp compHausToTop = Profinite.toTopCat

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 = Profinite.mk (CompHaus.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).toCompHaus.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_toCompHaus_toTop_α (A : FintypeCat) : ↑(FintypeCat.toProfinite.obj A).toCompHaus.toTop = ↑A

@[simp]

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

@[simp]

theorem FintypeCat.toProfinite_obj_toCompHaus_toTop_str_IsOpen (A : FintypeCat) (u : Set ↑A) : TopologicalSpace.IsOpen u = (u ∈ ⊤)

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.

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

• Profinite.limitCone F = { pt := Profinite.mk (CompHaus.limitCone (F.comp profiniteToCompHaus)).pt, π := { app := (CompHaus.limitCone (F.comp profiniteToCompHaus)).π.app, naturality := ⋯ } }

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.isClosedMap {X : Profinite} {Y : Profinite} (f : X ⟶ Y) : IsClosedMap ⇑f

Any morphism of profinite spaces is a closed map.

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.

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.

Equations

• Profinite.isoOfBijective f bij = CategoryTheory.asIso f

instance Profinite.forget_reflectsIsomorphisms : (CategoryTheory.forget Profinite).ReflectsIsomorphisms

Equations

• Profinite.forget_reflectsIsomorphisms = ⋯

@[simp]

theorem Profinite.isoOfHomeo_hom {X : Profinite} {Y : Profinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) : (Profinite.isoOfHomeo f).hom = { toFun := ⇑f, continuous_toFun := ⋯ }

@[simp]

theorem Profinite.isoOfHomeo_inv {X : Profinite} {Y : Profinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) : (Profinite.isoOfHomeo f).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

• Profinite.isoOfHomeo f = CategoryTheory.asIso { toFun := ⇑f, continuous_toFun := ⋯ }

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

@[simp]

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

def Profinite.homeoOfIso {X : Profinite} {Y : Profinite} (f : X ≅ Y) : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop

Construct a homeomorphism from an isomorphism.

Equations

• Profinite.homeoOfIso f = CompHaus.homeoOfIso (profiniteToCompHaus.mapIso f)

@[simp]

theorem Profinite.isoEquivHomeo_apply_symm_apply {X : Profinite} {Y : Profinite} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj Y.toCompHaus) : (Profinite.isoEquivHomeo f).symm a = f.inv 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 : (CategoryTheory.forget CompHaus).obj X.toCompHaus) : (Profinite.isoEquivHomeo f) a = f.hom 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

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 := ⋯ }

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem Profinite.mono_iff_injective {X : Profinite} {Y : Profinite} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑f