# 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
Instances For
def Profinite.IndexFunctor.π_app {ι : Type u} {X : ιType} [(i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) (J : ιProp) :
C(C, )

The projection maps in the limit cone indexCone.

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Profinite.IndexFunctor.surjective_π_app {ι : Type u} {X : ιType} [(i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) {J : ιProp} :
theorem Profinite.IndexFunctor.map_comp_π_app {ι : Type u} {X : ιType} [(i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) {J : ιProp} {K : ιProp} (h : ∀ (i : ι), J iK i) :
=
theorem Profinite.IndexFunctor.eq_of_forall_π_app_eq {ι : Type u} {X : ιType} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} (a : C) (b : C) (h : ∀ (J : ), (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 : ι), ] (hC : ) :

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.
Instances For
noncomputable def Profinite.indexCone {ι : Type u} {X : ιType} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), ] (hC : ) :

The limit cone on indexFunctor

Equations
Instances For
instance Profinite.isIso_indexCone_lift {ι : Type u} {X : ιType} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), ] (hC : ) :
Equations
• =
noncomputable def Profinite.isoindexConeLift {ι : Type u} {X : ιType} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), ] (hC : ) :
.pt

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

Equations
Instances For
noncomputable def Profinite.asLimitindexConeIso {ι : Type u} {X : ιType} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), ] (hC : ) :

The isomorphism of cones induced by isoindexConeLift.

Equations
Instances For
noncomputable def Profinite.indexCone_isLimit {ι : Type u} {X : ιType} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), ] (hC : ) :

indexCone is a limit cone.

Equations
• = .ofIsoLimit .symm
Instances For