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

ProCGroups/InverseSystems/CompatibilityAndSurjectivity.lean

1import ProCGroups.InverseSystems.Basic
2import ProCGroups.InverseSystems.Utilities
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/InverseSystems/CompatibilityAndSurjectivity.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Inverse systems and inverse limits
15Defines inverse systems of topological groups and proves lift, projection, exactness, quotient, stagewise isomorphism, and finite-stage factorization results.
16-/
18open Set
19open scoped Topology
21namespace ProCGroups.InverseSystems
23universe u v w
25section
27variable {I : Type u} [Preorder I]
29attribute [instance] InverseSystem.topologicalSpace
31namespace InverseSystem
33variable (S : InverseSystem (I := I))
35/-- Compatibility restricted to indices below a fixed stage. This is only used to prove
36nonemptiness of the inverse limit. -/
37private def CompatibleUpTo (j : I) (x : ∀ i, S.X i) : Prop :=
38 ∀ k, ∀ hkj : k ≤ j, S.map hkj (x j) = x k
40private theorem isClosed_setOf_compatibleUpTo [∀ i, T2Space (S.X i)] (j : I) :
41 IsClosed {x : ∀ i, S.X i | S.CompatibleUpTo j x} := by
42 simp only [CompatibleUpTo, setOf_forall]
43 refine isClosed_iInter fun k => isClosed_iInter fun hkj => ?_
44 exact isClosed_eq ((S.continuous_map hkj).comp (continuous_apply j)) (continuous_apply k)
46private theorem compatibleUpTo_nonempty (j : I) [∀ i, Nonempty (S.X i)] :
47 ({x : ∀ i, S.X i | S.CompatibleUpTo j x} : Set (∀ i, S.X i)).Nonempty := by
48 classical
49 let xj : S.X j := Classical.choice (inferInstance : Nonempty (S.X j))
50 let x : ∀ i, S.X i := fun i =>
51 if hij : i ≤ j then S.map hij xj else Classical.choice (inferInstance : Nonempty (S.X i))
52 refine ⟨x, ?_⟩
53 intro k hkj
54 simp only [le_refl, ↓reduceDIte, map_id_apply, hkj, x]
56private theorem compatibleUpTo_mono {j j' : I} (hjj' : j ≤ j') :
57 {x : ∀ i, S.X i | S.CompatibleUpTo j' x} ⊆ {x : ∀ i, S.X i | S.CompatibleUpTo j x} := by
58 intro x hx k hkj
59 calc
60 S.map hkj (x j) = S.map hkj (S.map hjj' (x j')) := by rw [hx j hjj']
61 _ = S.map (hkj.trans hjj') (x j') := by rw [S.map_comp_apply hkj hjj']
62 _ = x k := hx k (hkj.trans hjj')
64/-- The inverse limit of nonempty compact Hausdorff spaces is nonempty. -/
65theorem nonempty_inverseLimit [∀ i, Nonempty (S.X i)] [∀ i, CompactSpace (S.X i)]
66 [∀ i, T2Space (S.X i)] (hdir : Directed (· ≤ ·) (id : I → I)) :
67 Nonempty S.inverseLimit := by
68 classical
69 let Y : I → Set (∀ i, S.X i) := fun j => {x | S.CompatibleUpTo j x}
70 have hclosed : ∀ j, IsClosed (Y j) := fun j => S.isClosed_setOf_compatibleUpTo j
71 have hfinite : ∀ s : Finset I, (⋂ i ∈ s, Y i).Nonempty := by
72 intro s
73 by_cases hs : s.Nonempty
74 · rcases exists_upperBound_finset (I := I) hdir s hs with ⟨j, hj⟩
75 rcases S.compatibleUpTo_nonempty j with ⟨x, hx⟩
76 refine ⟨x, ?_⟩
77 simp only [Y, mem_iInter]
78 intro i hi
79 exact S.compatibleUpTo_mono (hj i hi) hx
80 · have hs' : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs
81 subst hs'
82 refine ⟨fun i => Classical.choice (inferInstance : Nonempty (S.X i)), ?_⟩
83 simp only [Finset.notMem_empty, iInter_of_empty, iInter_univ, mem_univ]
84 rcases CompactSpace.iInter_nonempty hclosed hfinite with ⟨x, hx⟩
85 refine ⟨⟨x, ?_⟩⟩
86 intro i j hij
87 exact (mem_iInter.mp hx j) i hij
89/-- Special case for inverse systems of nonempty finite discrete spaces. -/
90theorem nonempty_inverseLimit_of_finite [∀ i, Finite (S.X i)] [∀ i, Nonempty (S.X i)]
91 [∀ i, DiscreteTopology (S.X i)] (hdir : Directed (· ≤ ·) (id : I → I)) :
92 Nonempty S.inverseLimit := by
93 letI : ∀ i, CompactSpace (S.X i) := fun _ => inferInstance
94 letI : ∀ i, T2Space (S.X i) := fun _ => inferInstance
95 exact S.nonempty_inverseLimit hdir
97/-- A morphism of inverse systems over the same directed preorder. -/
98structure Morphism (T : InverseSystem (I := I)) where
99 map : ∀ i, S.X i → T.X i
100 continuous_map : ∀ i, Continuous (map i)
101 comm : ∀ {i j : I} (hij : i ≤ j), T.map hij ∘ map j = map i ∘ S.map hij
103namespace Morphism
105variable {S}
106variable {T U : InverseSystem (I := I)}
108/-- A morphism of inverse systems commutes with transition maps pointwise. -/
109@[simp] theorem comm_apply (Θ : S.Morphism T) {i j : I} (hij : i ≤ j) (x : S.X j) :
110 T.map hij (Θ.map j x) = Θ.map i (S.map hij x) := by
111 simpa [Function.comp] using congrFun (Θ.comm hij) x
113/-- The identity morphism of an inverse system. -/
114def id (S : InverseSystem (I := I)) : S.Morphism S where
115 map := fun _ => fun x => x
116 continuous_map := fun _ => continuous_id
117 comm := fun _ => by
118 funext x
119 rfl
121/-- The identity morphism of an inverse system acts as the identity at each stage. -/
122@[simp] theorem id_apply (i : I) (x : S.X i) :
123 (id S).map i x = x := rfl
125/-- Composition of morphisms of inverse systems. -/
126def comp (Φ : T.Morphism U) (Θ : S.Morphism T) : S.Morphism U where
127 map := fun i => Φ.map i ∘ Θ.map i
128 continuous_map := fun i => (Φ.continuous_map i).comp (Θ.continuous_map i)
129 comm := fun {i j} hij => by
130 funext x
131 calc
132 U.map hij ((Φ.map j ∘ Θ.map j) x) = U.map hij (Φ.map j (Θ.map j x)) := rfl
133 _ = Φ.map i (T.map hij (Θ.map j x)) := by
134 exact congrFun (Φ.comm hij) (Θ.map j x)
135 _ = Φ.map i (Θ.map i (S.map hij x)) := by
136 rw [Θ.comm_apply hij x]
137 _ = ((Φ.map i ∘ Θ.map i) ∘ S.map hij) x := by
138 rfl
140/-- Composition of morphisms of inverse systems is computed stagewise. -/
141@[simp] theorem comp_apply (Φ : T.Morphism U) (Θ : S.Morphism T) (i : I) (x : S.X i) :
142 (comp Φ Θ).map i x = Φ.map i (Θ.map i x) := rfl
146/-- A morphism of inverse systems sends inverse-limit projections to a compatible family. -/
147theorem compatibleMaps_morphism {T : InverseSystem (I := I)} (Θ : S.Morphism T) :
148 T.CompatibleMaps (fun i => Θ.map i ∘ S.projection i) := by
149 intro i j hij
150 funext x
151 calc
152 T.map hij (Θ.map j (S.projection j x)) = Θ.map i (S.map hij (S.projection j x)) := by
153 exact Θ.comm_apply hij (S.projection j x)
154 _ = Θ.map i (S.projection i x) := by rw [S.projection_compatible x i j hij]
156/-- The induced map on inverse limits of a morphism of inverse systems. -/
157def limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T) :
158 S.inverseLimit → T.inverseLimit :=
159 T.inverseLimitLift (fun i => Θ.map i ∘ S.projection i) (S.compatibleMaps_morphism Θ)
161/-- A projection after the induced map on inverse limits is the corresponding stage map after projection. -/
162@[simp] theorem π_comp_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T) (i : I) :
163 T.projection i ∘ S.limMap Θ = Θ.map i ∘ S.projection i := by
166/-- Pointwise form of the projection formula for the induced map on inverse limits. -/
167@[simp] theorem π_limMap_apply {T : InverseSystem (I := I)} (Θ : S.Morphism T)
168 (i : I) (x : S.inverseLimit) :
169 T.projection i (S.limMap Θ x) = Θ.map i (S.projection i x) := by
170 simpa [Function.comp] using congrFun (S.π_comp_limMap (Θ := Θ) i) x
172/-- The map induced on inverse limits by a morphism of inverse systems is continuous. -/
173theorem continuous_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T) :
174 Continuous (S.limMap Θ) := by
175 refine T.continuous_inverseLimitLift (fun i => Θ.map i ∘ S.projection i) ?_ (S.compatibleMaps_morphism Θ)
176 intro i
177 exact (Θ.continuous_map i).comp (S.continuous_projection i)
179/-- The inverse-limit map induced by the identity morphism is the identity. -/
180@[simp] theorem limMap_id :
181 S.limMap (Morphism.id S) = id := by
182 funext x
183 apply S.ext
184 intro i
185 change S.projection i (S.limMap (Morphism.id S) x) = S.projection i x
186 rw [S.π_limMap_apply (Θ := Morphism.id S)]
187 rfl
189/-- The inverse-limit map induced by a composite morphism is the composite of the induced maps. -/
190@[simp] theorem limMap_comp {T U : InverseSystem (I := I)} (Φ : T.Morphism U) (Θ : S.Morphism T) :
191 S.limMap (Morphism.comp Φ Θ) = T.limMap Φ ∘ S.limMap Θ := by
192 funext x
193 apply U.ext
194 intro i
195 change U.projection i (S.limMap (Morphism.comp Φ Θ) x) = U.projection i ((T.limMap Φ ∘ S.limMap Θ) x)
196 calc
197 U.projection i (S.limMap (Morphism.comp Φ Θ) x) = (Morphism.comp Φ Θ).map i (S.projection i x) := by
198 rw [S.π_limMap_apply (Θ := Morphism.comp Φ Θ)]
199 _ = Φ.map i (Θ.map i (S.projection i x)) := rfl
200 _ = U.projection i ((T.limMap Φ ∘ S.limMap Θ) x) := by
201 rw [Function.comp, T.π_limMap_apply (Θ := Φ), S.π_limMap_apply (Θ := Θ)]
203/-- The induced map on inverse limits is injective when all stage maps are injective. -/
204theorem injective_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T)
205 (hinj : ∀ i, Function.Injective (Θ.map i)) :
206 Function.Injective (S.limMap Θ) := by
207 intro x y hxy
208 apply S.ext
209 intro i
210 apply hinj i
211 simpa using congrArg (T.projection i) hxy
213/-- If all components of a morphism of inverse systems are embeddings, then the induced map on
214inverse limits is an embedding. -/
215theorem embedding_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T)
216 (hemb : ∀ i, Topology.IsEmbedding (Θ.map i)) :
217 Topology.IsEmbedding (S.limMap Θ) := by
218 let hsubS : Topology.IsEmbedding (Subtype.val : S.inverseLimit → ∀ i, S.X i) :=
219 Topology.IsEmbedding.subtypeVal
220 let hpi : Topology.IsEmbedding (Pi.map fun i => Θ.map i : (∀ i, S.X i) → ∀ i, T.X i) :=
221 Topology.IsEmbedding.piMap fun i => hemb i
222 have hcomp :
223 Topology.IsEmbedding
224 (((Subtype.val : T.inverseLimit → ∀ i, T.X i) ∘ S.limMap Θ) : S.inverseLimit → ∀ i, T.X i) := by
225 simpa [Function.comp] using (hpi.comp hsubS)
226 exact Topology.IsEmbedding.of_comp (S.continuous_limMap Θ) continuous_subtype_val hcomp
228/-- If all components of a morphism of inverse systems are surjective,
229then the induced map on inverse limits is surjective. -/
230theorem surjective_limMap {T : InverseSystem (I := I)} [∀ i, CompactSpace (S.X i)]
231 [∀ i, T2Space (S.X i)] [∀ i, T2Space (T.X i)] (hdir : Directed (· ≤ ·) (id : I → I))
232 (Θ : S.Morphism T) (hsurj : ∀ i, Function.Surjective (Θ.map i)) :
233 Function.Surjective (S.limMap Θ) := by
234 intro xlim
235 let F : InverseSystem (I := I) := {
236 X := fun i => {x : S.X i // Θ.map i x = T.projection i xlim}
237 topologicalSpace := fun _ => inferInstance
238 map := fun {i j} hij x =>
239 ⟨S.map hij x.1, by
240 calc
241 Θ.map i (S.map hij x.1) = T.map hij (Θ.map j x.1) := by
242 symm
243 exact Θ.comm_apply hij x.1
244 _ = T.map hij (T.projection j xlim) := by rw [x.2]
245 _ = T.projection i xlim := T.projection_compatible xlim i j hij⟩
246 continuous_map := fun {i j} hij =>
247 Continuous.subtype_mk ((S.continuous_map hij).comp continuous_subtype_val) fun x => by
248 calc
249 Θ.map i (S.map hij x.1) = T.map hij (Θ.map j x.1) := by
250 symm
251 exact Θ.comm_apply hij x.1
252 _ = T.map hij (T.projection j xlim) := by rw [x.2]
253 _ = T.projection i xlim := T.projection_compatible xlim i j hij
254 map_id := fun i => by
255 funext x
256 apply Subtype.ext
257 simp only [projection_apply, map_id_apply, id_eq]
258 map_comp := fun {i j k} hij hjk => by
259 funext x
260 apply Subtype.ext
261 simp only [projection_apply, Function.comp_apply, S.map_comp_apply hij hjk]}
262 letI : ∀ i, Nonempty (F.X i) := fun i => by
263 rcases hsurj i (T.projection i xlim) with ⟨x, hx⟩
264 exact ⟨⟨x, hx⟩⟩
265 letI : ∀ i, T2Space (F.X i) := fun _ => inferInstance
266 letI : ∀ i, CompactSpace (F.X i) := fun i => by
267 let hs : IsClosed {x : S.X i | Θ.map i x = T.projection i xlim} :=
268 isClosed_eq (Θ.continuous_map i) continuous_const
269 simpa [F] using hs.isClosedEmbedding_subtypeVal.compactSpace
270 rcases InverseSystem.nonempty_inverseLimit (S := F) hdir with ⟨y⟩
271 refine ⟨⟨fun i => (y.1 i).1, ?_⟩, ?_⟩
272 · intro i j hij
273 exact congrArg Subtype.val (y.2 i j hij)
274 · apply T.ext
275 intro i
276 simpa using (y.1 i).2
278/-- Compatible surjections from a compact space induce a surjection
279onto the inverse limit. -/
280theorem surjective_inverseLimitLift {X : Type w} [TopologicalSpace X] [CompactSpace X]
281 [Nonempty I]
282 (ψ : ∀ i, X → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
283 (hsurj : ∀ i, Function.Surjective (ψ i)) (hdir : Directed (· ≤ ·) (id : I → I))
284 [∀ i, T2Space (S.X i)] :
285 Function.Surjective (S.inverseLimitLift ψ hcompat) := by
286 intro xlim
287 let Z : I → Set X := fun i => {x | ψ i x = S.projection i xlim}
288 have hclosed : ∀ i, IsClosed (Z i) := fun i => isClosed_eq (hψ i) continuous_const
289 have hfinite : ∀ s : Finset I, (⋂ i ∈ s, Z i).Nonempty := by
290 intro s
291 by_cases hs : s.Nonempty
292 · rcases exists_upperBound_finset (I := I) hdir s hs with ⟨j, hj⟩
293 rcases hsurj j (S.projection j xlim) with ⟨x, hx⟩
294 refine ⟨x, ?_⟩
295 simp only [Z, mem_iInter]
296 intro i hi
297 have hfac : S.map (hj i hi) (ψ j x) = ψ i x := by
298 simpa [Function.comp] using congrFun (hcompat i j (hj i hi)) x
299 calc
300 ψ i x = S.map (hj i hi) (ψ j x) := hfac.symm
301 _ = S.map (hj i hi) (S.projection j xlim) := by rw [hx]
302 _ = S.projection i xlim := S.projection_compatible xlim i j (hj i hi)
303 · have hs' : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs
304 subst hs'
305 let j : I := Classical.choice ‹Nonempty I›
306 rcases hsurj j (S.projection j xlim) with ⟨x, hx⟩
307 exact ⟨x, by simp only [Finset.notMem_empty, iInter_of_empty, iInter_univ, mem_univ]⟩
308 rcases CompactSpace.iInter_nonempty hclosed hfinite with ⟨x, hx⟩
309 refine ⟨x, ?_⟩
310 apply S.ext
311 intro i
312 calc
313 S.projection i (S.inverseLimitLift ψ hcompat x) = ψ i x := by
314 rfl
315 _ = S.projection i xlim := mem_iInter.mp hx i
317/-- If an inverse limit over a directed index set is finite, one projection separates all points. -/
319 (hdir : Directed (· ≤ ·) (id : I → I)) [Finite S.inverseLimit] :
320 ∃ k, Function.Injective (S.projection k) := by
321 classical
322 letI : Fintype S.inverseLimit := Fintype.ofFinite S.inverseLimit
323 let pairs : Finset (S.inverseLimit × S.inverseLimit) :=
324 Finset.univ.filter fun p => p.1 ≠ p.2
325 have hseparate :
326 ∀ p : S.inverseLimit × S.inverseLimit, p ∈ pairs →
327 ∃ i, S.projection i p.1 ≠ S.projection i p.2 := by
328 intro p hp
329 have hpne : p.1 ≠ p.2 := by
330 exact (Finset.mem_filter.mp hp).2
331 by_contra h
332 apply hpne
333 apply S.ext
334 intro i
335 by_contra hneq
336 exact h ⟨i, hneq⟩
337 have hfinset :
338 ∀ t : Finset (S.inverseLimit × S.inverseLimit),
339 (∀ p, p ∈ t → ∃ i, S.projection i p.1 ≠ S.projection i p.2) →
340 ∃ k, ∀ p, p ∈ t → S.projection k p.1 ≠ S.projection k p.2 := by
341 intro t
342 induction t using Finset.induction_on with
343 | empty =>
344 intro _
345 exact ⟨Classical.choice ‹Nonempty I›, by simp only [Finset.notMem_empty, projection_apply, ne_eq, IsEmpty.forall_iff, implies_true]⟩
346 | insert p t hpt ih =>
347 intro ht
348 rcases ht p (by simp only [Finset.mem_insert, true_or]) with ⟨j, hj⟩
349 have ht_rest : ∀ q, q ∈ t → ∃ i, S.projection i q.1 ≠ S.projection i q.2 := by
350 intro q hq
351 exact ht q (by simp only [Finset.mem_insert, hq, or_true])
352 rcases ih ht_rest with ⟨i, hi⟩
353 rcases hdir i j with ⟨k, hik, hjk⟩
354 refine ⟨k, ?_⟩
355 intro q hq
356 rw [Finset.mem_insert] at hq
357 rcases hq with rfl | hq
358 · intro heq
359 apply hj
360 calc
361 S.projection j q.1 = S.map hjk (S.projection k q.1) := by
362 exact (S.projection_compatible q.1 j k hjk).symm
363 _ = S.map hjk (S.projection k q.2) := by rw [heq]
364 _ = S.projection j q.2 := S.projection_compatible q.2 j k hjk
365 · intro heq
366 apply hi q hq
367 calc
368 S.projection i q.1 = S.map hik (S.projection k q.1) := by
369 exact (S.projection_compatible q.1 i k hik).symm
370 _ = S.map hik (S.projection k q.2) := by rw [heq]
371 _ = S.projection i q.2 := S.projection_compatible q.2 i k hik
372 rcases hfinset pairs hseparate with ⟨k, hk⟩
373 refine ⟨k, ?_⟩
374 intro x y hxy
375 by_contra hne
376 exact hk (x, y) (by simp only [ne_eq, Finset.mem_filter, Finset.mem_univ, hne, not_false_eq_true, and_self, pairs]) hxy
379end
380end ProCGroups.InverseSystems