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.

Equations

• Profinite.IndexFunctor.obj C J = ⇑(ContinuousMap.precomp Subtype.val) '' C

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

The projection maps in the limit cone indexCone.

Equations

• Profinite.IndexFunctor.π_app C J = { toFun := Set.MapsTo.restrict (⇑(ContinuousMap.precomp Subtype.val)) C (Profinite.IndexFunctor.obj C J) ⋯, continuous_toFun := ⋯ }

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(↑(Profinite.IndexFunctor.obj C K), ↑(Profinite.IndexFunctor.obj C J))

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

Equations

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

theorem Profinite.IndexFunctor.surjective_π_app {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) {J : ι → Prop} : Function.Surjective ⇑(Profinite.IndexFunctor.π_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) : ⇑(Profinite.IndexFunctor.map C h) ∘ ⇑(Profinite.IndexFunctor.π_app C K) = ⇑(Profinite.IndexFunctor.π_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 ι), (Profinite.IndexFunctor.π_app C fun (x : ι) => x ∈ J) a = (Profinite.IndexFunctor.π_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.

Equations

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

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 (Profinite.indexFunctor hC)

The limit cone on indexFunctor

Equations

• Profinite.indexCone hC = { pt := Profinite.of ↑C, π := { app := fun (J : (Finset ι)ᵒᵖ) => Profinite.IndexFunctor.π_app C fun (x : ι) => x ∈ Opposite.unop J, naturality := ⋯ } }

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 ((Profinite.limitConeIsLimit (Profinite.indexFunctor hC)).lift (Profinite.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) : Profinite.of ↑C ≅ (Profinite.limitCone (Profinite.indexFunctor hC)).pt

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

Equations

• Profinite.isoindexConeLift hC = CategoryTheory.asIso ((Profinite.limitConeIsLimit (Profinite.indexFunctor hC)).lift (Profinite.indexCone hC))

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) : Profinite.indexCone hC ≅ Profinite.limitCone (Profinite.indexFunctor hC)

The isomorphism of cones induced by isoindexConeLift.

Equations

• Profinite.asLimitindexConeIso hC = CategoryTheory.Limits.Cones.ext (Profinite.isoindexConeLift hC) ⋯

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 (Profinite.indexCone hC)

indexCone is a limit cone.

Equations

• Profinite.indexCone_isLimit hC = (Profinite.limitConeIsLimit (Profinite.indexFunctor hC)).ofIsoLimit (Profinite.asLimitindexConeIso hC).symm