Compact subsets of products as limits in Profinite

This file exhibits a compact subset C of a product (i : ι) → X i of totally disconnected Hausdorff spaces as a cofiltered limit in Profinite indexed by Finset ι.

Main definitions

• Profinite.indexFunctor is the functor (Finset ι)ᵒᵖ ⥤ Profinite indexing the limit. It maps J to the restriction of C to J
• Profinite.indexCone is a cone on Profinite.indexFunctor with cone point C

Main results

• Profinite.isIso_indexCone_lift says that the natural map from the cone point of the explicit limit cone in Profinite on indexFunctor to the cone point of indexCone is an isomorphism
• Profinite.asLimitindexConeIso is the induced isomorphism of cones.
• Profinite.indexCone_isLimit says that indexCone is a limit cone.

def Profinite.IndexFunctor.obj {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) (J : ι → Prop) : Set ((i : { i : ι // J i }) → X ↑i)

The object part of the functor indexFunctor : (Finset ι)ᵒᵖ ⥤ Profinite.

def Profinite.IndexFunctor.π_app {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) (J : ι → Prop) : C(↑C, ↑(obj C J))

The projection maps in the limit cone indexCone.

def Profinite.IndexFunctor.map {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) {J K : ι → Prop} (h : ∀ (i : ι), J i → K i) : C(↑(obj C K), ↑(obj C J))

The morphism part of the functor indexFunctor : (Finset ι)ᵒᵖ ⥤ Profinite.

theorem Profinite.IndexFunctor.surjective_π_app {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) {J : ι → Prop} : Function.Surjective ⇑(π_app C J)

theorem Profinite.IndexFunctor.map_comp_π_app {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) {J K : ι → Prop} (h : ∀ (i : ι), J i → K i) : ⇑(map C h) ∘ ⇑(π_app C K) = ⇑(π_app C J)

theorem Profinite.IndexFunctor.eq_of_forall_π_app_eq {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} (a b : ↑C) (h : ∀ (J : Finset ι), (π_app C fun (x : ι) => x ∈ J) a = (π_app C fun (x : ι) => x ∈ J) b) : a = b

noncomputable def Profinite.indexFunctor {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), TotallyDisconnectedSpace (X i)] (hC : IsCompact C) : CategoryTheory.Functor (Finset ι)ᵒᵖ Profinite

The functor from the poset of finsets of ι to Profinite, indexing the limit.

noncomputable def Profinite.indexCone {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), TotallyDisconnectedSpace (X i)] (hC : IsCompact C) : CategoryTheory.Limits.Cone (indexFunctor hC)

The limit cone on indexFunctor

instance Profinite.isIso_indexCone_lift {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), TotallyDisconnectedSpace (X i)] (hC : IsCompact C) : CategoryTheory.IsIso ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))

noncomputable def Profinite.isoindexConeLift {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), TotallyDisconnectedSpace (X i)] (hC : IsCompact C) : of ↑C ≅ (limitCone (indexFunctor hC)).pt

The canonical map from C to the explicit limit as an isomorphism.

noncomputable def Profinite.asLimitindexConeIso {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), TotallyDisconnectedSpace (X i)] (hC : IsCompact C) : indexCone hC ≅ limitCone (indexFunctor hC)

The isomorphism of cones induced by isoindexConeLift.

noncomputable def Profinite.indexCone_isLimit {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), TotallyDisconnectedSpace (X i)] (hC : IsCompact C) : CategoryTheory.Limits.IsLimit (indexCone hC)

indexCone is a limit cone.