Source: ProCGroups.InverseSystems.ProfiniteSpace
1import Mathlib.Topology.Category.Profinite.Basic
2import Mathlib.Topology.DiscreteQuotient
3import ProCGroups.InverseSystems.CofinalityAndDensity
5/-!
6# Profinite spaces as limits of finite discrete quotients
8Clopen equivalence relations on a compact Hausdorff totally disconnected space form an inverse
9system of finite discrete quotients. This module constructs the canonical homeomorphism from
10the space to that inverse limit and also proves the clopen-basis criterion used in the converse
11direction.
12-/
14open scoped Topology
16namespace ProCGroups.InverseSystems
18universe u v w
20/-- A compact Hausdorff totally disconnected space has a basis of clopen sets. -/
21theorem isTopologicalBasis_isClopen_of_compact_t2_totallyDisconnected {X : Type w}
22 [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] :
23 TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s} :=
24 isTopologicalBasis_isClopen
26/-- Every open neighborhood in a profinite space contains a clopen neighborhood of the point. -/
27theorem exists_clopen_subset_of_mem_open {X : Type w} [TopologicalSpace X]
28 [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
29 {x : X} {U : Set X} (hU : IsOpen U) (hx : x ∈ U) :
30 ∃ V : Set X, IsClopen V ∧ x ∈ V ∧ V ⊆ U :=
31 compact_exists_isClopen_in_isOpen hU hx
33/-- The inverse system of all discrete quotients of \(X\). -/
34def discreteQuotientSystem (X : Type w) [TopologicalSpace X] :
35 InverseSystem (I := OrderDual (DiscreteQuotient X)) where
36 X := fun Q => Quotient (show DiscreteQuotient X from Q).toSetoid
37 topologicalSpace := fun _ => inferInstance
38 map := fun {Q R} h => DiscreteQuotient.ofLE h
39 continuous_map := fun {Q R} _ => continuous_of_discreteTopology
40 map_id := fun Q => by
41 funext x
42 exact DiscreteQuotient.ofLE_refl_apply (A := (Q : DiscreteQuotient X)) x
43 map_comp := fun {Q R T} hQR hRT => by
44 funext x
45 exact congrFun (DiscreteQuotient.ofLE_comp_ofLE hRT hQR) x
47/-- The discrete quotient projections form a compatible family of maps. -/
48private theorem compatibleMaps_discreteQuotientProj (X : Type w) [TopologicalSpace X] :
49 (discreteQuotientSystem X).CompatibleMaps
50 (fun Q : OrderDual (DiscreteQuotient X) => (Q : DiscreteQuotient X).proj) := by
51 intro Q R h
52 funext x
53 exact DiscreteQuotient.ofLE_proj h x
55/-- A compact Hausdorff totally disconnected space is profinite. -/
56noncomputable def homeomorph_inverseLimit_discreteQuotientSystem (X : Type w)
57 [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] :
58 X ≃ₜ (discreteQuotientSystem X).inverseLimit := by
59 let S := discreteQuotientSystem X
60 letI : ∀ Q : OrderDual (DiscreteQuotient X), CompactSpace (S.X Q) := fun Q => by
61 change CompactSpace (Quotient (show DiscreteQuotient X from Q).toSetoid)
62 let _ : Fintype (Quotient (show DiscreteQuotient X from Q).toSetoid) := by
63 have : Finite (show DiscreteQuotient X from Q) := inferInstance
64 exact Fintype.ofFinite _
65 infer_instance
66 letI : ∀ Q : OrderDual (DiscreteQuotient X), T2Space (S.X Q) := fun Q => by
67 change T2Space (Quotient (show DiscreteQuotient X from Q).toSetoid)
68 infer_instance
69 letI : ∀ Q : OrderDual (DiscreteQuotient X), TotallyDisconnectedSpace (S.X Q) := fun Q => by
70 change TotallyDisconnectedSpace (Quotient (show DiscreteQuotient X from Q).toSetoid)
71 infer_instance
72 letI : CompactSpace S.inverseLimit := inferInstance
73 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
74 letI : TotallyDisconnectedSpace S.inverseLimit := S.totallyDisconnectedSpace_inverseLimit
75 let f : X → S.inverseLimit :=
76 S.inverseLimitLift (fun Q : OrderDual (DiscreteQuotient X) => (Q : DiscreteQuotient X).proj)
77 (compatibleMaps_discreteQuotientProj X)
78 have hf_continuous : Continuous f :=
79 S.continuous_inverseLimitLift (fun Q : OrderDual (DiscreteQuotient X) => (Q :
80 DiscreteQuotient X).proj)
81 (fun Q => (Q : DiscreteQuotient X).proj_continuous) (compatibleMaps_discreteQuotientProj X)
82 have hf_inj : Function.Injective f := by
83 intro x y hxy
84 exact DiscreteQuotient.eq_of_forall_proj_eq fun Q => by
85 have hQ := congrArg (fun z => S.projection (show OrderDual (DiscreteQuotient X) from Q) z) hxy
86 change (show DiscreteQuotient X from Q).proj x =
87 (show DiscreteQuotient X from Q).proj y at hQ
88 exact hQ
89 have hf_surj : Function.Surjective f := by
90 intro y
91 let qs : (Q : DiscreteQuotient X) → Q := fun Q => S.projection (show OrderDual
92 (DiscreteQuotient X) from Q) y
93 have hqs :
94 ∀ (A B : DiscreteQuotient X) (h : A ≤ B), DiscreteQuotient.ofLE h (qs A) = qs B := by
95 intro A B h
96 have hcompat :=
97 S.projection_compatible y (show OrderDual (DiscreteQuotient X) from B)
98 (show OrderDual (DiscreteQuotient X) from A) h
99 change DiscreteQuotient.ofLE h (qs A) = qs B at hcompat
100 exact hcompat
101 rcases DiscreteQuotient.exists_of_compat qs hqs with ⟨x, hx⟩
102 refine ⟨x, S.ext ?_⟩
103 intro Q
104 have hQ := hx (show DiscreteQuotient X from Q)
105 change (show DiscreteQuotient X from Q).proj x =
106 qs (show DiscreteQuotient X from Q)
107 exact hQ
108 let fHom : Profinite.of X ⟶ Profinite.of S.inverseLimit := CompHausLike.ofHom _ ⟨f, hf_continuous⟩
109 exact CompHausLike.homeoOfIso (CompHausLike.isoOfBijective fHom ⟨hf_inj, hf_surj⟩)
111/--
112The homeomorphism from a compact Hausdorff totally disconnected space to the inverse limit of
113its discrete quotients has \(Q\)-coordinate equal to the quotient projection of the point.
114-/
115@[simp] theorem discreteQuotientSystem_projection_homeomorph (X : Type w)
116 [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
117 (Q : OrderDual (DiscreteQuotient X)) (x : X) :
118 (discreteQuotientSystem X).projection Q
119 (homeomorph_inverseLimit_discreteQuotientSystem X x) =
120 (show DiscreteQuotient X from Q).proj x := by
121 let S := discreteQuotientSystem X
122 change (S.inverseLimitLift (fun Q : OrderDual (DiscreteQuotient X) =>
123 (show DiscreteQuotient X from Q).proj)
124 (compatibleMaps_discreteQuotientProj X) x).1 Q =
125 (show DiscreteQuotient X from Q).proj x
126 rfl
128/-- A Hausdorff space with a clopen basis is totally disconnected. -/
129theorem totallyDisconnectedSpace_of_t2_basis_clopen (X : Type w) [TopologicalSpace X] [T2Space X]
130 (hX : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}) :
131 TotallyDisconnectedSpace X := by
132 let _ : TotallySeparatedSpace X := totallySeparatedSpace_of_t0_of_basis_clopen hX
133 infer_instance
135end ProCGroups.InverseSystems