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.

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.instInhabitedProfinite : Inhabited Profinite

Equations

• Profinite.instInhabitedProfinite = { 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.instCoeSortProfiniteType : CoeSort Profinite (Type u_1)

Equations

• Profinite.instCoeSortProfiniteType = { 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αTopologicalSpaceToTopToCompHausTopologicalSpace_coe {X : Profinite} : TotallyDisconnectedSpace ↑X.toCompHaus.toTop

Equations

• ⋯ = ⋯

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Profinite.instT2SpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategoryInstTopologicalSpaceObjProfiniteToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory {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 instFullProfiniteCategoryCompHausCategoryProfiniteToCompHaus : CategoryTheory.Functor.Full profiniteToCompHaus

Equations

• instFullProfiniteCategoryCompHausCategoryProfiniteToCompHaus = ⋯

instance instFaithfulProfiniteCategoryCompHausCategoryProfiniteToCompHaus : CategoryTheory.Functor.Faithful profiniteToCompHaus

Equations

• instFaithfulProfiniteCategoryCompHausCategoryProfiniteToCompHaus = ⋯

instance instTotallyDisconnectedSpaceαTopologicalSpaceToTopObjProfiniteToQuiverToCategoryStructCategoryCompHausCategoryToPrefunctorProfiniteToCompHausTopologicalSpace_coe {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 instFullProfiniteCategoryTopCatInstTopCatLargeCategoryToTopCat : CategoryTheory.Functor.Full Profinite.toTopCat

Equations

• instFullProfiniteCategoryTopCatInstTopCatLargeCategoryToTopCat = ⋯

instance instFaithfulProfiniteCategoryTopCatInstTopCatLargeCategoryToTopCat : CategoryTheory.Functor.Faithful Profinite.toTopCat

Equations

• instFaithfulProfiniteCategoryTopCatInstTopCatLargeCategoryToTopCat = ⋯

@[simp]

theorem Profinite.to_compHausToTopCat : CategoryTheory.Functor.comp profiniteToCompHaus 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

• CompHaus.toProfiniteObj X = Profinite.mk (CompHaus.mk (TopCat.of (ConnectedComponents ↑X.toTop)))

def Profinite.toCompHausEquivalence (X : CompHaus) (Y : Profinite) : (CompHaus.toProfiniteObj X ⟶ 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

• FintypeCat.botTopology A = ⊥

theorem FintypeCat.discreteTopology (A : FintypeCat) : DiscreteTopology ↑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 ∈ ⊤)

@[simp]

theorem FintypeCat.toProfinite_obj_toCompHaus_toTop_α (A : FintypeCat) : ↑(FintypeCat.toProfinite.obj A).toCompHaus.toTop = ↑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.

instance instFaithfulFintypeCatInstCategoryFintypeCatProfiniteCategoryToProfinite : CategoryTheory.Functor.Faithful FintypeCat.toProfinite

Equations

• instFaithfulFintypeCatInstCategoryFintypeCatProfiniteCategoryToProfinite = ⋯

instance instFullFintypeCatInstCategoryFintypeCatProfiniteCategoryToProfinite : CategoryTheory.Functor.Full FintypeCat.toProfinite

Equations

• instFullFintypeCatInstCategoryFintypeCatProfiniteCategoryToProfinite = ⋯

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

• ProfiniteMax = Profinite

def Profinite.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteMax) : 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 ProfiniteMax) : 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

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.Functor.ReflectsIsomorphisms (CategoryTheory.forget Profinite)

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

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

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) : (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 : (CategoryTheory.forget CompHaus).obj 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 := ⋯ }

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

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

Equations

• ⋯ = ⋯

instance Profinite.instEpiProfiniteCategory {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