ProCGroups/InverseSystems/ProfiniteSpace.lean
1import Mathlib.Topology.Category.Profinite.Basic
2import Mathlib.Topology.DiscreteQuotient
3import ProCGroups.InverseSystems.CofinalityAndDensity
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/InverseSystems/ProfiniteSpace.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Inverse systems and inverse limits
16Defines inverse systems of topological groups and proves lift, projection, exactness, quotient, stagewise isomorphism, and finite-stage factorization results.
17-/
19open scoped Topology
21namespace ProCGroups.InverseSystems
23universe u v w
25/-- A compact Hausdorff totally disconnected space has a basis of
26clopen sets. -/
27theorem isTopologicalBasis_isClopen_of_compact_t2_totallyDisconnected {X : Type w}
28 [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] :
29 TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s} :=
30 isTopologicalBasis_isClopen
32/-- Every open neighborhood in a profinite space contains a clopen neighborhood of the point. -/
33theorem exists_clopen_subset_of_mem_open {X : Type w} [TopologicalSpace X]
34 [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
35 {x : X} {U : Set X} (hU : IsOpen U) (hx : x ∈ U) :
36 ∃ V : Set X, IsClopen V ∧ x ∈ V ∧ V ⊆ U :=
37 compact_exists_isClopen_in_isOpen hU hx
39/-- A profinite space, in the unbundled form matching Mathlib's `Profinite.of` constructor. -/
40abbrev IsProfiniteSpace (X : Type w) [TopologicalSpace X] : Prop :=
41 CompactSpace X ∧ T2Space X ∧ TotallyDisconnectedSpace X
43namespace IsProfiniteSpace
45variable {X : Type w} [TopologicalSpace X]
47/-- The compactness component of a profinite space. -/
48theorem compactSpace (hX : IsProfiniteSpace X) : CompactSpace X :=
49 hX.1
51/-- The Hausdorff component of a profinite space. -/
52theorem t2Space (hX : IsProfiniteSpace X) : T2Space X :=
53 hX.2.1
55/-- The `T1` component of a profinite space. -/
56theorem t1Space (hX : IsProfiniteSpace X) : T1Space X := by
57 letI : T2Space X := hX.t2Space
58 infer_instance
60/-- The totally disconnected component of a profinite space. -/
61theorem totallyDisconnectedSpace (hX : IsProfiniteSpace X) : TotallyDisconnectedSpace X :=
62 hX.2.2
64/-- Bundle an unbundled profinite space as Mathlib's `Profinite`. -/
65noncomputable def toProfinite (hX : IsProfiniteSpace X) : Profinite.{w} := by
66 letI : CompactSpace X := hX.compactSpace
67 letI : T2Space X := hX.t2Space
68 letI : TotallyDisconnectedSpace X := hX.totallyDisconnectedSpace
69 exact Profinite.of X
71/-- The profinite-space wrapper has the same underlying type as the original space. -/
72@[simp] theorem coe_toProfinite (hX : IsProfiniteSpace X) :
73 (hX.toProfinite : Type w) = X := by
74 letI : CompactSpace X := hX.compactSpace
75 letI : T2Space X := hX.t2Space
76 letI : TotallyDisconnectedSpace X := hX.totallyDisconnectedSpace
77 rfl
79/-- Every Mathlib bundled profinite space is profinite in the unbundled sense. -/
80theorem of_profinite (X : Profinite.{w}) : IsProfiniteSpace X :=
81 ⟨inferInstance, inferInstance, inferInstance⟩
85/-- The inverse system of all discrete quotients of `X`. -/
86def discreteQuotientSystem (X : Type w) [TopologicalSpace X] :
87 InverseSystem (I := OrderDual (DiscreteQuotient X)) where
88 X := fun Q => Quotient (show DiscreteQuotient X from Q).toSetoid
89 topologicalSpace := fun _ => inferInstance
90 map := fun {Q R} h => DiscreteQuotient.ofLE h
91 continuous_map := fun {Q R} _ => continuous_of_discreteTopology
92 map_id := fun Q => by
93 funext x
94 exact DiscreteQuotient.ofLE_refl_apply (A := (Q : DiscreteQuotient X)) x
95 map_comp := fun {Q R T} hQR hRT => by
96 funext x
97 exact congrFun (DiscreteQuotient.ofLE_comp_ofLE hRT hQR) x
99private theorem compatibleMaps_discreteQuotientProj (X : Type w) [TopologicalSpace X] :
101 (fun Q : OrderDual (DiscreteQuotient X) => (Q : DiscreteQuotient X).proj) := by
102 intro Q R h
103 funext x
104 exact DiscreteQuotient.ofLE_proj h x
106/-- A compact Hausdorff totally disconnected space is profinite. -/
107noncomputable def homeomorph_inverseLimit_discreteQuotientSystem (X : Type w)
108 [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] :
109 X ≃ₜ (discreteQuotientSystem X).inverseLimit := by
110 let S := discreteQuotientSystem X
111 letI : ∀ Q : OrderDual (DiscreteQuotient X), CompactSpace (S.X Q) := fun Q => by
112 change CompactSpace (Quotient (show DiscreteQuotient X from Q).toSetoid)
113 let _ : Fintype (Quotient (show DiscreteQuotient X from Q).toSetoid) := by
114 have : Finite (show DiscreteQuotient X from Q) := inferInstance
115 exact Fintype.ofFinite _
116 infer_instance
117 letI : ∀ Q : OrderDual (DiscreteQuotient X), T2Space (S.X Q) := fun Q => by
118 change T2Space (Quotient (show DiscreteQuotient X from Q).toSetoid)
119 infer_instance
120 letI : ∀ Q : OrderDual (DiscreteQuotient X), TotallyDisconnectedSpace (S.X Q) := fun Q => by
121 change TotallyDisconnectedSpace (Quotient (show DiscreteQuotient X from Q).toSetoid)
122 infer_instance
123 letI : CompactSpace S.inverseLimit := inferInstance
124 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
125 letI : TotallyDisconnectedSpace S.inverseLimit := S.totallyDisconnectedSpace_inverseLimit
126 let f : X → S.inverseLimit :=
127 S.inverseLimitLift (fun Q : OrderDual (DiscreteQuotient X) => (Q : DiscreteQuotient X).proj)
129 have hf_continuous : Continuous f :=
130 S.continuous_inverseLimitLift (fun Q : OrderDual (DiscreteQuotient X) => (Q : DiscreteQuotient X).proj)
131 (fun Q => (Q : DiscreteQuotient X).proj_continuous) (compatibleMaps_discreteQuotientProj X)
132 have hf_inj : Function.Injective f := by
133 intro x y hxy
134 exact DiscreteQuotient.eq_of_forall_proj_eq fun Q => by
135 have hQ := congrArg (fun z => S.projection (show OrderDual (DiscreteQuotient X) from Q) z) hxy
136 simpa [f] using hQ
137 have hf_surj : Function.Surjective f := by
138 intro y
139 let qs : (Q : DiscreteQuotient X) → Q := fun Q => S.projection (show OrderDual (DiscreteQuotient X) from Q) y
140 have hqs :
141 ∀ (A B : DiscreteQuotient X) (h : A ≤ B), DiscreteQuotient.ofLE h (qs A) = qs B := by
142 intro A B h
143 simpa [qs] using
144 S.projection_compatible y (show OrderDual (DiscreteQuotient X) from B)
145 (show OrderDual (DiscreteQuotient X) from A) h
146 rcases DiscreteQuotient.exists_of_compat qs hqs with ⟨x, hx⟩
147 refine ⟨x, S.ext ?_⟩
148 intro Q
149 simpa [f] using hx Q
150 let fHom : Profinite.of X ⟶ Profinite.of S.inverseLimit := CompHausLike.ofHom _ ⟨f, hf_continuous⟩
151 exact CompHausLike.homeoOfIso (CompHausLike.isoOfBijective fHom ⟨hf_inj, hf_surj⟩)
153@[simp] theorem discreteQuotientSystem_projection_homeomorph (X : Type w)
154 [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
155 (Q : OrderDual (DiscreteQuotient X)) (x : X) :
156 (discreteQuotientSystem X).projection Q
158 (show DiscreteQuotient X from Q).proj x := by
159 let S := discreteQuotientSystem X
160 change (S.inverseLimitLift (fun Q : OrderDual (DiscreteQuotient X) =>
161 (show DiscreteQuotient X from Q).proj)
162 (compatibleMaps_discreteQuotientProj X) x).1 Q =
163 (show DiscreteQuotient X from Q).proj x
164 rfl
166/-- A compact Hausdorff totally disconnected space is a profinite space. -/
167theorem isProfiniteSpace_of_compact_t2_totallyDisconnected (X : Type w) [TopologicalSpace X]
168 [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] :
169 IsProfiniteSpace X :=
170 ⟨inferInstance, inferInstance, inferInstance⟩
172/-- A profinite space is compact, Hausdorff, and totally disconnected. -/
173theorem compact_t2_totallyDisconnected_of_isProfiniteSpace (X : Type w) [TopologicalSpace X]
174 (hX : IsProfiniteSpace X) :
175 CompactSpace X ∧ T2Space X ∧ TotallyDisconnectedSpace X :=
176 hX
178/-- A Hausdorff space with a clopen basis is totally disconnected. -/
179theorem totallyDisconnectedSpace_of_t2_basis_clopen (X : Type w) [TopologicalSpace X] [T2Space X]
180 (hX : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}) :
181 TotallyDisconnectedSpace X := by
182 let _ : TotallySeparatedSpace X := totallySeparatedSpace_of_t0_of_basis_clopen hX
183 infer_instance
185/-- The inverse-limit definition of a profinite space is equivalent to the usual compact Hausdorff
186totally disconnected characterization. -/
187theorem isProfiniteSpace_iff_compact_t2_totallyDisconnected {X : Type w} [TopologicalSpace X] :
188 IsProfiniteSpace X ↔ CompactSpace X ∧ T2Space X ∧ TotallyDisconnectedSpace X :=
189 Iff.rfl
191/-- A compact Hausdorff space is profinite exactly when the clopen sets form a basis. -/
192theorem isProfiniteSpace_iff_compact_t2_basis_clopen {X : Type w} [TopologicalSpace X] :
193 IsProfiniteSpace X ↔
194 CompactSpace X ∧ T2Space X ∧ TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s} := by
195 constructor
196 · intro hX
197 rcases compact_t2_totallyDisconnected_of_isProfiniteSpace X hX with ⟨hcompact, hT2, htot⟩
198 let _ : CompactSpace X := hcompact
199 let _ : T2Space X := hT2
200 let _ : TotallyDisconnectedSpace X := htot
201 exact ⟨hcompact, hT2, isTopologicalBasis_isClopen_of_compact_t2_totallyDisconnected⟩
202 · rintro ⟨hcompact, hT2, hbasis⟩
203 let _ : CompactSpace X := hcompact
204 let _ : T2Space X := hT2
205 let _ : TotallyDisconnectedSpace X := totallyDisconnectedSpace_of_t2_basis_clopen X hbasis
208end ProCGroups.InverseSystems