ProCGroups/InverseSystems/CofinalityAndDensity.lean
1import ProCGroups.InverseSystems.CompatibilityAndSurjectivity
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/InverseSystems/CofinalityAndDensity.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Inverse systems and inverse limits
14Defines inverse systems of topological groups and proves lift, projection, exactness, quotient, stagewise isomorphism, and finite-stage factorization results.
15-/
17open Set
18open scoped Topology
20namespace ProCGroups.InverseSystems
22universe u v w
24section
26variable {I : Type u} [Preorder I]
28attribute [instance] InverseSystem.topologicalSpace
30namespace InverseSystem
32variable (S : InverseSystem (I := I))
34/-- Every open neighborhood in the inverse limit contains
36theorem exists_projection_preimage_subset [Nonempty I]
37 (hdir : Directed (· ≤ ·) (id : I → I)) {x : S.inverseLimit} {U : Set S.inverseLimit}
38 (hU : IsOpen U) (hx : x ∈ U) :
39 ∃ i, ∃ V : Set (S.X i), IsOpen V ∧ S.projection i x ∈ V ∧ S.projection i ⁻¹' V ⊆ U := by
40 classical
41 have hUx : U ∈ 𝓝 x := hU.mem_nhds hx
42 rw [nhds_subtype_eq_comap, Filter.mem_comap] at hUx
43 rcases hUx with ⟨W, hW, hWU⟩
44 rw [mem_nhds_iff] at hW
45 rcases hW with ⟨W', hW'W, hW'open, hxW'⟩
46 rcases (isOpen_pi_iff.mp hW'open) x.1 hxW' with ⟨s, Us, hUs, hsW'⟩
47 by_cases hs : s.Nonempty
48 · rcases exists_upperBound_finset (I := I) hdir s hs with ⟨j, hj⟩
49 let V : Set (S.X j) := ⋂ i ∈ s, if hi : i ∈ s then S.map (hj i hi) ⁻¹' Us i else univ
50 refine ⟨j, V, ?_, ?_, ?_⟩
51 · refine isOpen_biInter_finset fun i hi => ?_
52 simpa [hi] using (hUs i hi).1.preimage (S.continuous_map (hj i hi))
53 · change S.projection j x ∈ ⋂ i ∈ s, if hi : i ∈ s then S.map (hj i hi) ⁻¹' Us i else univ
54 rw [Set.mem_iInter]
55 intro i
56 rw [Set.mem_iInter]
57 intro hi
58 have hxji : S.map (hj i hi) (S.projection j x) ∈ Us i := by
59 rw [S.projection_compatible x i j (hj i hi)]
60 exact (hUs i hi).2
61 simpa [hi, Set.mem_preimage] using hxji
62 · intro y hy
63 apply hWU
64 apply hW'W
65 apply hsW'
66 change S.projection j y ∈ ⋂ i ∈ s, if hi : i ∈ s then S.map (hj i hi) ⁻¹' Us i else univ at hy
67 rw [Set.mem_iInter] at hy
68 intro i hi
69 have hyi : S.map (hj i hi) (S.projection j y) ∈ Us i := by
70 have hyji := Set.mem_iInter.1 (hy i) hi
71 have hif :
72 (if hi' : i ∈ s then S.map (hj i hi') ⁻¹' Us i else univ) =
73 S.map (hj i hi) ⁻¹' Us i := by
74 ext z
75 by_cases h : i ∈ s
76 · rw [dif_pos h]
77 · exact (h.elim hi)
78 rw [hif] at hyji
79 simpa [Set.mem_preimage] using hyji
80 rw [S.projection_compatible y i j (hj i hi)] at hyi
81 exact hyi
82 · let j : I := Classical.choice ‹Nonempty I›
83 refine ⟨j, univ, isOpen_univ, mem_univ _, ?_⟩
84 intro y hy
85 apply hWU
86 apply hW'W
87 apply hsW'
88 have hs' : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs
89 have : y.1 ∈ ((↑s : Set I).pi Us) := by
90 simp only [hs', Finset.coe_empty, empty_pi, mem_univ]
91 exact this
93/-- A compatible family of surjections induces a dense map to the inverse limit.
96set is nonempty. -/
97theorem denseRange_lift {X : Type w} [Nonempty I]
98 (ρ : ∀ i, X → S.X i) (hρ : S.CompatibleMaps ρ)
99 (hsurj : ∀ i, Function.Surjective (ρ i)) (hdir : Directed (· ≤ ·) (id : I → I)) :
100 DenseRange (S.inverseLimitLift ρ hρ) := by
101 rw [DenseRange, dense_iff_inter_open]
102 intro U hU hUne
103 rcases hUne with ⟨y, hyU⟩
104 rcases S.exists_projection_preimage_subset hdir hU hyU with ⟨i, V, hVopen, hyV, hVU⟩
105 rcases hsurj i (S.projection i y) with ⟨x, hx⟩
106 refine ⟨S.inverseLimitLift ρ hρ x, hVU ?_, ⟨x, rfl⟩⟩
107 change ρ i x ∈ V
108 rw [hx]
109 exact hyV
111/-- Reindexing an inverse system along a monotone map. -/
112def reindex {K : Type w} [Preorder K] (σ : K → I) (hσ : Monotone σ) :
113 InverseSystem (I := K) where
114 X := fun k => S.X (σ k)
115 topologicalSpace := fun k => inferInstance
116 map := fun {i j} hij => S.map (hσ hij)
117 continuous_map := fun {i j} hij => S.continuous_map (hσ hij)
118 map_id := fun k => by
119 simpa using S.map_id (σ k)
120 map_comp := fun {i j k} hij hjk => by
121 simpa using S.map_comp (hσ hij) (hσ hjk)
123/-- The inverse system obtained by restricting the index preorder to a subset. -/
124def restrict (J : Set I) : InverseSystem (I := J) :=
125 S.reindex (fun j : J => j.1) (fun {_ _} hij => hij)
127/-- The inverse limit is unchanged after reindexing along a monotone cofinal
128map. -/
129noncomputable def homeomorph_reindex_cofinal {K : Type w} [Preorder K]
130 (σ : K → I) (hσ : Monotone σ) (hdirK : Directed (· ≤ ·) (id : K → K))
131 (hcofinal : ∀ i : I, ∃ k : K, i ≤ σ k) :
132 S.inverseLimit ≃ₜ (S.reindex σ hσ).inverseLimit := by
133 classical
134 let R := S.reindex σ hσ
135 have hcompatR : R.CompatibleMaps (fun k => S.projection (σ k)) := by
136 intro i j hij
137 funext x
138 exact S.projection_compatible x (σ i) (σ j) (hσ hij)
139 let r : S.inverseLimit → R.inverseLimit := R.inverseLimitLift (fun k => S.projection (σ k)) hcompatR
140 choose τ hτ using hcofinal
141 let ψ : ∀ i, R.inverseLimit → S.X i := fun i => S.map (hτ i) ∘ R.projection (τ i)
142 have hψ_eq :
143 ∀ {i : I} (k : K) (hik : i ≤ σ k) (x : R.inverseLimit),
144 ψ i x = S.map hik (R.projection k x) := by
145 intro i k hik x
146 rcases hdirK (τ i) k with ⟨ℓ, hτℓ, hkℓ⟩
147 calc
148 ψ i x = S.map (hτ i) (R.projection (τ i) x) := rfl
149 _ = S.map (hτ i) (S.map (hσ hτℓ) (R.projection ℓ x)) := by
150 simpa [R, reindex] using congrArg (S.map (hτ i)) ((R.projection_compatible x (τ i) ℓ hτℓ).symm)
151 _ = S.map ((hτ i).trans (hσ hτℓ)) (R.projection ℓ x) := by
152 rw [S.map_comp_apply (hτ i) (hσ hτℓ)]
153 _ = S.map (hik.trans (hσ hkℓ)) (R.projection ℓ x) := by
154 have hproof : (hτ i).trans (hσ hτℓ) = hik.trans (hσ hkℓ) := Subsingleton.elim _ _
155 rw [hproof]
156 _ = S.map hik (S.map (hσ hkℓ) (R.projection ℓ x)) := by
157 rw [S.map_comp_apply hik (hσ hkℓ)]
158 _ = S.map hik (R.projection k x) := by
159 simpa [R, reindex] using congrArg (S.map hik) (R.projection_compatible x k ℓ hkℓ)
160 have hcompatψ : S.CompatibleMaps ψ := by
161 intro i j hij
162 funext x
163 calc
164 S.map hij (ψ j x) = S.map hij (S.map (hτ j) (R.projection (τ j) x)) := rfl
165 _ = S.map (hij.trans (hτ j)) (R.projection (τ j) x) := by
166 rw [S.map_comp_apply hij (hτ j)]
167 _ = ψ i x := by
168 symm
169 exact hψ_eq (k := τ j) (hik := hij.trans (hτ j)) x
170 let s : R.inverseLimit → S.inverseLimit := S.inverseLimitLift ψ hcompatψ
171 refine
172 { toFun := r
173 invFun := s
174 left_inv := ?_
175 right_inv := ?_
176 continuous_toFun := R.continuous_inverseLimitLift (fun k => S.projection (σ k))
177 (fun k => S.continuous_projection (σ k)) hcompatR
178 continuous_invFun := S.continuous_inverseLimitLift ψ
179 (fun i => (S.continuous_map (hτ i)).comp (R.continuous_projection (τ i))) hcompatψ } <;>
180 intro x
181 · apply S.ext
182 intro i
183 calc
184 S.projection i (s (r x)) = ψ i (r x) := by
185 rfl
186 _ = S.map (hτ i) (R.projection (τ i) (r x)) := rfl
187 _ = S.map (hτ i) (S.projection (σ (τ i)) x) := by
188 exact congrArg (S.map (hτ i))
189 (by simpa [r, Function.comp] using
190 congrFun (R.projection_comp_inverseLimitLift (fun k => S.projection (σ k)) hcompatR (τ i)) x)
191 _ = S.projection i x := S.projection_compatible x i (σ (τ i)) (hτ i)
192 · apply R.ext
193 intro k
194 calc
195 R.projection k (r (s x)) = S.projection (σ k) (s x) := by
196 simpa [r, Function.comp] using
197 congrFun (R.projection_comp_inverseLimitLift (fun k => S.projection (σ k)) hcompatR k) (s x)
198 _ = ψ (σ k) x := by
199 rfl
200 _ = S.map (le_rfl : σ k ≤ σ k) (R.projection k x) := by
201 exact hψ_eq (k := k) (hik := le_rfl) x
202 _ = R.projection k x := by
203 exact S.map_id_apply (σ k) (R.projection k x)
205/-- The cofinal reindexing homeomorphism is characterized by its projections. -/
206@[simp 900] theorem π_comp_homeomorph_reindex_cofinal {K : Type w} [Preorder K]
207 (σ : K → I) (hσ : Monotone σ) (hdirK : Directed (· ≤ ·) (id : K → K))
208 (hcofinal : ∀ i : I, ∃ k : K, i ≤ σ k) (k : K) :
209 (S.reindex σ hσ).projection k ∘ S.homeomorph_reindex_cofinal σ hσ hdirK hcofinal = S.projection (σ k) := by
210 classical
211 let R := S.reindex σ hσ
212 have hcompatR : R.CompatibleMaps (fun k => S.projection (σ k)) := by
213 intro i j hij
214 funext x
215 exact S.projection_compatible x (σ i) (σ j) (hσ hij)
216 funext x
217 simpa [R, homeomorph_reindex_cofinal, Function.comp] using
218 congrFun (R.projection_comp_inverseLimitLift (fun k => S.projection (σ k)) hcompatR k) x
220/-- The inverse limit is unchanged after passing to a cofinal subsystem. -/
221noncomputable def homeomorph_restrict_cofinal (J : Set I)
222 (hdirJ : Directed (· ≤ ·) (id : J → J)) (hcofinal : ∀ i, ∃ j : J, i ≤ j.1) :
223 S.inverseLimit ≃ₜ (S.restrict J).inverseLimit :=
224 S.homeomorph_reindex_cofinal (fun j : J => j.1) (fun {_ _} hij => hij) hdirJ hcofinal
226/-- The cofinal restriction homeomorphism is characterized by its projections. -/
227@[simp 900] theorem π_comp_homeomorph_restrict_cofinal (J : Set I)
228 (hdirJ : Directed (· ≤ ·) (id : J → J)) (hcofinal : ∀ i, ∃ j : J, i ≤ j.1) (j : J) :
229 (S.restrict J).projection j ∘ S.homeomorph_restrict_cofinal J hdirJ hcofinal = S.projection j.1 := by
230 exact
231 (S.π_comp_homeomorph_reindex_cofinal (σ := fun j : J => j.1)
232 (hσ := fun {_ _} hij => hij) hdirJ hcofinal j)
234/-- In a surjective inverse system of compact Hausdorff nonempty spaces,
235each projection from the inverse limit is surjective. -/
236theorem surjective_π [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
237 (hdir : Directed (· ≤ ·) (id : I → I))
238 (hsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (S.map hij)) (j : I) :
239 Function.Surjective (S.projection j) := by
240 let J : Set I := Set.Ici j
241 have hdirJ : Directed (· ≤ ·) (id : J → J) := by
242 intro a b
243 rcases hdir a.1 b.1 with ⟨k, hak, hbk⟩
244 refine ⟨⟨k, a.2.trans hak⟩, hak, hbk⟩
245 have hcofinal : ∀ i, ∃ k : J, i ≤ k.1 := by
246 intro i
247 rcases hdir i j with ⟨k, hik, hjk⟩
248 exact ⟨⟨k, hjk⟩, hik⟩
249 let e := S.homeomorph_restrict_cofinal J hdirJ hcofinal
250 let j0 : J := ⟨j, le_rfl⟩
251 intro xj
252 let T : InverseSystem (I := J) := {
253 X := fun k => {x : S.X k.1 // S.map k.2 x = xj}
254 topologicalSpace := fun _ => inferInstance
255 map := fun {a b} hab x =>
256 ⟨S.map hab x.1, by
257 have hproof : a.2.trans hab = b.2 := Subsingleton.elim _ _
258 calc
259 S.map a.2 (S.map hab x.1) = S.map (a.2.trans hab) x.1 := by rw [S.map_comp_apply a.2 hab]
260 _ = S.map b.2 x.1 := by rw [hproof]
261 _ = xj := x.2⟩
262 continuous_map := fun {a b} hab =>
263 Continuous.subtype_mk ((S.continuous_map hab).comp continuous_subtype_val) fun x => by
264 have hproof : a.2.trans hab = b.2 := Subsingleton.elim _ _
265 calc
266 S.map a.2 (S.map hab x.1) = S.map (a.2.trans hab) x.1 := by rw [S.map_comp_apply a.2 hab]
267 _ = S.map b.2 x.1 := by rw [hproof]
268 _ = xj := x.2
269 map_id := fun a => by
270 funext x
271 apply Subtype.ext
272 simp only [map_id_apply, id_eq]
273 map_comp := fun {a b c} hab hbc => by
274 funext x
275 apply Subtype.ext
276 simp only [Function.comp_apply, S.map_comp_apply hab hbc]}
277 letI : ∀ k, Nonempty (T.X k) := fun k => by
278 rcases hsurj k.2 xj with ⟨x, hx⟩
279 exact ⟨⟨x, hx⟩⟩
280 letI : ∀ k, T2Space (T.X k) := fun _ => inferInstance
281 letI : ∀ k, CompactSpace (T.X k) := fun k => by
282 let hs : IsClosed {x : S.X k.1 | S.map k.2 x = xj} :=
283 isClosed_eq (S.continuous_map k.2) continuous_const
284 simpa [T] using hs.isClosedEmbedding_subtypeVal.compactSpace
285 rcases InverseSystem.nonempty_inverseLimit (S := T) hdirJ with ⟨y⟩
286 let xlimJ : (S.restrict J).inverseLimit := ⟨fun k => (y.1 k).1, by
287 intro a b hab
288 exact congrArg Subtype.val (y.2 a b hab)⟩
289 have hj0 : (S.restrict J).projection j0 xlimJ = xj := by
290 simpa [xlimJ, j0] using (y.1 j0).2
291 have hstep : S.projection j (e.symm xlimJ) = (S.restrict J).projection j0 xlimJ := by
292 simpa [Function.comp, e] using
293 (congrFun (S.π_comp_homeomorph_restrict_cofinal J hdirJ hcofinal j0) (e.symm xlimJ)).symm
294 refine ⟨e.symm xlimJ, ?_⟩
295 calc
296 S.projection j (e.symm xlimJ) = (S.restrict J).projection j0 xlimJ := hstep
297 _ = xj := hj0
299end InverseSystem
300end
302/-- If each component has a chosen basis, then the inverse images of basis
303elements under the projection maps form a basis of the inverse limit. -/
304theorem InverseSystem.isTopologicalBasis_projection_preimages {I : Type u} [Preorder I]
305 (S : InverseSystem (I := I)) [Nonempty I] (hdir : Directed (· ≤ ·) (id : I → I))
306 (B : ∀ i, Set (Set (S.X i))) (hB : ∀ i, TopologicalSpace.IsTopologicalBasis (B i)) :
307 TopologicalSpace.IsTopologicalBasis
308 {W : Set S.inverseLimit | ∃ i, ∃ V ∈ B i, W = S.projection i ⁻¹' V} := by
309 classical
310 refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
311 · rintro W ⟨i, V, hV, rfl⟩
313 · intro x U hx hU
314 rcases S.exists_projection_preimage_subset hdir hU hx with ⟨i, V, hVopen, hxV, hVU⟩
315 rcases (hB i).exists_subset_of_mem_open hxV hVopen with ⟨W, hW, hxW, hWV⟩
316 refine ⟨S.projection i ⁻¹' W, ⟨i, W, hW, rfl⟩, hxW, ?_⟩
317 exact (Set.preimage_mono hWV).trans hVU
319end ProCGroups.InverseSystems