Yamaguchi Lean 4 Library
ProCGroups/InverseSystems/ProjectionImageSystems.lean
ProCGroups/InverseSystems/ProjectionImageSystems/Source

ProCGroups/InverseSystems/ProjectionImageSystems.lean

1import ProCGroups.InverseSystems.CofinalityAndDensity
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/InverseSystems/ProjectionImageSystems.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
24/-- The inverse system formed by the projection images of a subset of an inverse limit. -/
25def InverseSystem.projectionImageSystem {I : Type u} [Preorder I]
26 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
27 InverseSystem (I := I) where
28 X := fun i => S.projection i '' Y
29 topologicalSpace := fun _ => inferInstance
30 map := fun {i j} hij x => ⟨S.map hij x.1, by
31 rcases x.2 with ⟨y, hy, hxy⟩
32 refine ⟨y, hy, ?_⟩
33 simpa [← hxy] using (S.projection_compatible y i j hij).symm⟩
34 continuous_map := fun {i j} hij =>
35 Continuous.subtype_mk
36 ((S.continuous_map hij).comp continuous_subtype_val) (fun x => by
37 rcases x.2 with ⟨y, hy, hxy⟩
38 refine ⟨y, hy, ?_⟩
39 simpa [Function.comp, ← hxy] using (S.projection_compatible y i j hij).symm)
40 map_id := fun i => by
41 funext x
42 apply Subtype.ext
43 simp only [map_id_apply, id_eq]
44 map_comp := fun {i j k} hij hjk => by
45 funext x
46 apply Subtype.ext
47 simp only [Function.comp_apply, S.map_comp_apply hij hjk]
49/-- The canonical morphism from the projection-image system into the ambient
50inverse system. -/
51def projectionImageInclusion {I : Type u} [Preorder I]
52 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
53 (S.projectionImageSystem Y).Morphism S where
54 map := fun _ => Subtype.val
55 continuous_map := fun _ => continuous_subtype_val
56 comm := fun {i j} hij => by
57 funext x
58 rfl
60/-- The coordinatewise section map from a subset of an inverse limit to its
61projection-image system. -/
62def projectionImageSectionMap {I : Type u} [Preorder I]
63 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :
64 Y → (S.projectionImageSystem Y).X i :=
65 fun y => ⟨S.projection i y.1, ⟨y.1, y.2, rfl⟩⟩
67/-- The projection-image section map is continuous. -/
68theorem continuous_projectionImageSectionMap {I : Type u} [Preorder I]
69 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :
70 Continuous (projectionImageSectionMap S Y i) := by
71 exact Continuous.subtype_mk ((S.continuous_projection i).comp continuous_subtype_val)
72 (fun y => ⟨y.1, y.2, rfl⟩)
74/-- The projection-image section maps are compatible with the inverse-system
75transition maps. -/
76theorem compatible_projectionImageSectionMap {I : Type u} [Preorder I]
77 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
78 (S.projectionImageSystem Y).CompatibleMaps (projectionImageSectionMap S Y) := by
79 intro i j hij
80 funext y
81 apply Subtype.ext
82 exact S.projection_compatible y.1 i j hij
84/-- Each coordinate section map onto a projection image is surjective. -/
85theorem surjective_projectionImageSectionMap {I : Type u} [Preorder I]
86 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :
87 Function.Surjective (projectionImageSectionMap S Y i) := by
88 intro x
89 rcases x.2 with ⟨y, hy, hxy⟩
90 refine ⟨⟨y, hy⟩, ?_⟩
91 apply Subtype.ext
92 simpa using hxy
94/-- The canonical lift from a subset of an inverse limit to the inverse limit of
95its projection-image system. -/
96def projectionImageLift {I : Type u} [Preorder I]
97 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
98 Y → (S.projectionImageSystem Y).inverseLimit :=
99 (S.projectionImageSystem Y).inverseLimitLift (projectionImageSectionMap S Y)
102/-- The canonical projection-image lift is continuous. -/
103theorem continuous_projectionImageLift {I : Type u} [Preorder I]
104 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
105 Continuous (projectionImageLift S Y) := by
106 exact (S.projectionImageSystem Y).continuous_inverseLimitLift (projectionImageSectionMap S Y)
109/-- For a closed subset of a compact Hausdorff inverse limit, the canonical
110projection-image lift is surjective. -/
111theorem surjective_projectionImageLift {I : Type u} [Preorder I] [Nonempty I]
112 (S : InverseSystem (I := I)) [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
113 (hdir : Directed (· ≤ ·) (id : I → I)) (Y : Set S.inverseLimit) (hY : IsClosed Y) :
114 Function.Surjective (projectionImageLift S Y) := by
115 let T := S.projectionImageSystem Y
116 letI : CompactSpace Y := by
117 simpa using hY.isClosedEmbedding_subtypeVal.compactSpace
118 letI : ∀ i, T2Space (T.X i) := fun i => by
119 change T2Space (S.projection i '' Y)
120 infer_instance
121 exact T.surjective_inverseLimitLift (projectionImageSectionMap S Y) (continuous_projectionImageSectionMap S Y)
124/-- Composing the projection-image lift with the inclusion morphism recovers the
125underlying point of the original inverse limit. -/
126theorem projectionImageLift_comp_subtype {I : Type u} [Preorder I]
127 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :
128 (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) ∘
129 projectionImageLift S Y = Subtype.val := by
130 funext y
131 apply S.ext
132 intro i
133 have hpi :
134 (S.projectionImageSystem Y).projection i (projectionImageLift S Y y) =
136 simpa [Function.comp, projectionImageLift] using
137 congrFun
140 calc
141 S.projection i ((S.projectionImageSystem Y).limMap (projectionImageInclusion S Y)
144 ((S.projectionImageSystem Y).projection i (projectionImageLift S Y y)) := by
145 simpa [Function.comp] using
146 congrFun
147 ((S.projectionImageSystem Y).π_comp_limMap
149 _ = ((S.projectionImageSystem Y).projection i (projectionImageLift S Y y)).1 := rfl
150 _ = (projectionImageSectionMap S Y i y).1 := by rw [hpi]
151 _ = S.projection i y.1 := rfl
153/-- The transition maps in the projection-image system are always surjective. -/
154theorem InverseSystem.surjective_projectionImageSystem_map
155 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) (Y : Set S.inverseLimit)
156 {i j : I} (hij : i ≤ j) :
157 Function.Surjective ((S.projectionImageSystem Y).map hij) := by
158 intro x
159 rcases x.2 with ⟨y, hy, hxy⟩
160 refine ⟨⟨S.projection j y, ⟨y, hy, rfl⟩⟩, ?_⟩
161 apply Subtype.ext
162 change S.map hij (S.projection j y) = x.1
163 rw [S.projection_compatible y i j hij]
164 exact hxy
166/-- A closed subset of an inverse limit is homeomorphic to the inverse limit of its
167projection-image system. -/
168noncomputable def InverseSystem.homeomorph_projectionImageSystem_of_isClosed
169 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
170 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
171 (hdir : Directed (· ≤ ·) (id : I → I))
172 (Y : Set S.inverseLimit) (hY : IsClosed Y) :
173 Y ≃ₜ (S.projectionImageSystem Y).inverseLimit := by
174 classical
175 letI : CompactSpace Y := by
176 simpa using hY.isClosedEmbedding_subtypeVal.compactSpace
177 letI : ∀ i, T2Space ((S.projectionImageSystem Y).X i) := fun i => by
178 change T2Space (S.projection i '' Y)
179 infer_instance
181 have he_inj : Function.Injective e := by
182 intro y y' hyy
183 have hy : y.1 = y'.1 := by
184 calc
185 y.1 = (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) (e y) := by
186 simpa [Function.comp] using (congrFun (projectionImageLift_comp_subtype S Y) y).symm
187 _ = (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) (e y') := by
188 rw [hyy]
189 _ = y'.1 := by
190 simpa [Function.comp] using congrFun (projectionImageLift_comp_subtype S Y) y'
191 exact Subtype.ext hy
193 ⟨he_inj, surjective_projectionImageLift S hdir Y hY⟩
195/-- The image-system embedding identifies the inverse limit with the
196closed subset. -/
198 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
199 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
200 (hdir : Directed (· ≤ ·) (id : I → I))
201 (Y : Set S.inverseLimit) (hY : IsClosed Y) :
202 Set.range ((S.projectionImageSystem Y).limMap (projectionImageInclusion S Y)) = Y := by
203 classical
204 apply le_antisymm
205 · rintro x ⟨z, rfl⟩
206 rcases surjective_projectionImageLift S hdir Y hY z with ⟨y, hy⟩
207 have hx :
208 (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) z = y.1 := by
209 calc
210 (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) z
211 = (S.projectionImageSystem Y).limMap
213 rw [hy]
214 _ = y.1 := by
215 simpa [Function.comp] using congrFun (projectionImageLift_comp_subtype S Y) y
216 exact hx ▸ y.2
217 · intro y hy
218 refine ⟨projectionImageLift S Y ⟨y, hy⟩, ?_⟩
219 simpa [Function.comp] using congrFun (projectionImageLift_comp_subtype S Y) ⟨y, hy⟩
221/-- Membership in the projected image system can be checked coordinatewise. -/
222theorem InverseSystem.mem_isClosed_iff_forall_projection_mem
223 {I : Type u} [Preorder I] {S : InverseSystem (I := I)} [Nonempty I]
224 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
225 (hdir : Directed (· ≤ ·) (id : I → I))
226 {Y : Set S.inverseLimit} (hY : IsClosed Y) {x : S.inverseLimit} :
227 x ∈ Y ↔ ∀ i, S.projection i x ∈ S.projection i '' Y := by
228 classical
229 constructor
230 · intro hx i
231 exact ⟨x, hx, rfl⟩
232 · intro hx
233 let T := S.projectionImageSystem Y
234 let incl : T.Morphism S := projectionImageInclusion S Y
235 have hcompat :
236 T.CompatibleMaps (fun (i : I) (_ : Unit) => (⟨S.projection i x, hx i⟩ : T.X i)) := by
237 intro i j hij
238 funext _
239 apply Subtype.ext
240 exact S.projection_compatible x i j hij
241 let z : T.inverseLimit :=
242 T.inverseLimitLift (fun (i : I) (_ : Unit) => (⟨S.projection i x, hx i⟩ : T.X i)) hcompat ()
243 have hz : T.limMap incl z = x := by
244 apply S.ext
245 intro i
246 have hpi : T.projection i z = (⟨S.projection i x, hx i⟩ : T.X i) := by
247 simpa [Function.comp, z] using
248 congrFun
249 (T.projection_comp_inverseLimitLift (fun (i : I) (_ : Unit) => (⟨S.projection i x, hx i⟩ : T.X i)) hcompat i) ()
250 calc
251 S.projection i (T.limMap incl z) = incl.map i (T.projection i z) := by
252 simpa [Function.comp] using congrFun (T.π_comp_limMap (Θ := incl) i) z
253 _ = (T.projection i z).1 := rfl
254 _ = S.projection i x := by rw [hpi]
255 have hxrange : x ∈ Set.range (T.limMap incl) := ⟨z, hz⟩
256 rw [range_limMap_projectionImageInclusion_eq S hdir Y hY] at hxrange
257 exact hxrange
259/-- A closed subspace of an inverse limit is again an inverse limit of its projection images. -/
260theorem InverseSystem.exists_homeomorph_closed_subspace_projection_images
261 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
262 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
263 (hdir : Directed (· ≤ ·) (id : I → I))
264 (Y : Set S.inverseLimit) (hY : IsClosed Y) :
265 (∀ i, Nonempty (((S.projectionImageSystem Y).X i) ≃ₜ (S.projection i '' Y))) ∧
266 Nonempty (Y ≃ₜ (S.projectionImageSystem Y).inverseLimit) := by
267 constructor
268 · intro i
269 exact ⟨Homeomorph.refl _⟩
270 · exact ⟨S.homeomorph_projectionImageSystem_of_isClosed hdir Y hY⟩
272/-- The projection of the closure of a subset equals the closure of the projection image. -/
273theorem InverseSystem.projection_image_closure_eq_closure_projection_image
274 {I : Type u} [Preorder I] (S : InverseSystem (I := I))
275 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
276 (i : I) (Y : Set S.inverseLimit) :
277 S.projection i '' closure Y = closure (S.projection i '' Y) := by
278 let hclosed : IsClosedMap (S.projection i) := (S.continuous_projection i).isClosedMap
279 simpa using (hclosed.closure_image_eq_of_continuous (S.continuous_projection i) Y).symm
281/-
282Textual note: the printed PDF on p. 7 states these results without closures on the projection
283images. As written, that is false already for a one-point index set. The proof works after
284inserting closures on the projection images, equivalently by replacing `Y` with `closure Y`
285inside the projection-image system.
286-/
287/-- The closure of a subset of an inverse limit is homeomorphic to the inverse limit of the
288projection-image system of that closure. -/
289theorem InverseSystem.exists_homeomorph_closure_projection_images
290 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
291 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
292 (hdir : Directed (· ≤ ·) (id : I → I))
293 (Y : Set S.inverseLimit) :
294 (∀ i, Nonempty (((S.projectionImageSystem (closure Y)).X i) ≃ₜ (S.projection i '' closure Y))) ∧
295 Nonempty (closure Y ≃ₜ (S.projectionImageSystem (closure Y)).inverseLimit) := by
296 simpa using S.exists_homeomorph_closed_subspace_projection_images hdir (Y := closure Y)
297 isClosed_closure
299/-- Equal projection images of the closures force the closures themselves to be equal. -/
300theorem InverseSystem.closure_eq_of_projection_images_eq
301 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
302 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
303 (hdir : Directed (· ≤ ·) (id : I → I))
304 (Y Y' : Set S.inverseLimit)
305 (hproj : ∀ i, S.projection i '' closure Y = S.projection i '' closure Y') :
306 closure Y = closure Y' := by
307 ext x
308 constructor
309 · intro hx
310 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure] at hx
311 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
312 intro i
313 rw [← hproj i]
314 exact hx i
315 · intro hx
316 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure] at hx
317 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
318 intro i
319 rw [hproj i]
320 exact hx i
322/-- Equal raw projection images of two subsets force their closures in the inverse limit to be
323equal. -/
324theorem InverseSystem.closure_eq_of_projection_images_eq_of_subsets
325 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
326 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
327 (hdir : Directed (· ≤ ·) (id : I → I))
328 (Y Y' : Set S.inverseLimit)
329 (hproj : ∀ i, S.projection i '' Y = S.projection i '' Y') :
330 closure Y = closure Y' := by
331 apply S.closure_eq_of_projection_images_eq hdir Y Y'
332 intro i
333 calc
334 S.projection i '' closure Y = closure (S.projection i '' Y) := by
335 exact S.projection_image_closure_eq_closure_projection_image i Y
336 _ = closure (S.projection i '' Y') := by rw [hproj i]
337 _ = S.projection i '' closure Y' := by
338 symm
339 exact S.projection_image_closure_eq_closure_projection_image i Y'
341/-- Any inverse system of compact Hausdorff spaces admits a surjective projection-image system
342with the same inverse limit. -/
343noncomputable def InverseSystem.homeomorph_surjectiveProjectionImageSystem
344 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
345 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
346 (hdir : Directed (· ≤ ·) (id : I → I)) :
347 S.inverseLimit ≃ₜ (S.projectionImageSystem (Set.univ : Set S.inverseLimit)).inverseLimit :=
348 (Homeomorph.Set.univ S.inverseLimit).symm.trans
349 (S.homeomorph_projectionImageSystem_of_isClosed hdir Set.univ isClosed_univ)
351/-- The projection-image system of the full inverse limit is surjective and has the same inverse
352limit as the original system. -/
353theorem InverseSystem.exists_homeomorph_surjectiveProjectionImageSystem
354 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
355 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
356 (hdir : Directed (· ≤ ·) (id : I → I)) :
357 (∀ {i j : I} (hij : i ≤ j),
358 Function.Surjective ((S.projectionImageSystem (Set.univ : Set S.inverseLimit)).map hij)) ∧
359 Nonempty (S.inverseLimit ≃ₜ
360 (S.projectionImageSystem (Set.univ : Set S.inverseLimit)).inverseLimit) := by
361 constructor
362 · intro i j hij
363 exact S.surjective_projectionImageSystem_map (Y := (Set.univ : Set S.inverseLimit)) hij
364 · exact ⟨S.homeomorph_surjectiveProjectionImageSystem hdir⟩
366end ProCGroups.InverseSystems