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

ProCGroups/InverseSystems/FiniteStageFactorization.lean

1import ProCGroups.InverseSystems.ProfiniteSpace
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/InverseSystems/FiniteStageFactorization.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
21namespace ProCGroups.InverseSystems
23universe u v w
25private def additiveMultiplicativeHomeomorph (A : Type*) [TopologicalSpace A] :
26 A ≃ₜ Multiplicative A where
27 toEquiv := Multiplicative.ofAdd
28 continuous_toFun := continuous_id
29 continuous_invFun := continuous_id
31/-- The inverse system whose `F`-th stage is the finite
32subproduct over a finite subset `F`. -/
33def finiteSubsetProductSystem {α : Type u} (X : α → Type v)
34 [∀ a, TopologicalSpace (X a)] : InverseSystem.{u, max u v} (I := Finset α) where
35 X := fun F => ∀ a : F, X a.1
36 topologicalSpace := fun _ => inferInstance
37 map := fun {F G} hFG x a => x ⟨a.1, hFG a.2⟩
38 continuous_map := fun {F G} hFG => by
39 exact continuous_pi fun a => continuous_apply (⟨a.1, hFG a.2⟩ : G)
40 map_id := fun F => by
41 funext x a
42 rfl
43 map_comp := fun {F G H} hFG hGH => by
44 funext x a
45 rfl
47/-- An arbitrary product is homeomorphic to the inverse limit of its finite subproducts. -/
48def homeomorph_inverseLimit_finiteSubsetProductSystem {α : Type u} (X : α → Type v)
49 [∀ a, TopologicalSpace (X a)] :
50 (∀ a, X a) ≃ₜ (finiteSubsetProductSystem X).inverseLimit := by
51 let S : InverseSystem.{u, max u v} (I := Finset α) := finiteSubsetProductSystem X
52 let toS : (∀ a, X a) → S.inverseLimit := fun x =>
53 ⟨fun F a => x a.1, by
54 intro F G hFG
55 funext a
56 rfl⟩
57 let fromS : S.inverseLimit → (∀ a, X a) :=
58 fun y a => S.projection ({a} : Finset α) y ⟨a, by simp only [Finset.mem_singleton]⟩
59 have hleft : Function.LeftInverse fromS toS := by
60 intro x
61 funext a
62 rfl
63 have hright : Function.RightInverse fromS toS := by
64 intro y
65 apply S.ext
66 intro F
67 funext a
68 change fromS y a.1 = S.projection F y a
69 have hs : ({a.1} : Finset α) ≤ F := by
70 intro b hb
71 have hb' : b = a.1 := by simpa using hb
72 exact hb' ▸ a.2
73 have hcompat := congrFun (y.2 ({a.1} : Finset α) F hs) ⟨a.1, by simp only [Finset.mem_singleton]⟩
74 simpa [fromS, S, finiteSubsetProductSystem] using hcompat.symm
75 have hcontinuous_toS : Continuous toS := by
76 exact Continuous.subtype_mk
77 (by
78 refine continuous_pi fun F => ?_
79 refine continuous_pi fun a => ?_
80 exact continuous_apply a.1)
81 (fun x F G hFG => by
82 funext a
83 rfl)
84 have hcontinuous_fromS : Continuous fromS := by
85 refine continuous_pi fun a => ?_
86 exact (continuous_apply ⟨a, by simp only [Finset.mem_singleton]⟩).comp (S.continuous_projection ({a} : Finset α))
87 exact
88 { toFun := toS
89 invFun := fromS
90 left_inv := hleft
91 right_inv := hright
92 continuous_toFun := hcontinuous_toS
93 continuous_invFun := hcontinuous_fromS }
95/-- A continuous map from a profinite inverse limit to a finite discrete
96space factors through one projection. -/
97theorem InverseSystem.factors_through_projection_finite
98 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
99 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
100 [∀ i, TotallyDisconnectedSpace (S.X i)] (hdir : Directed (· ≤ ·) (id : I → I))
101 {Y : Type w} [TopologicalSpace Y] [Finite Y] [Nonempty Y] [DiscreteTopology Y]
102 (ρ : S.inverseLimit → Y) (hρ : Continuous ρ) :
103 ∃ k : I, ∃ ρ' : S.X k → Y, Continuous ρ' ∧ ρ = ρ' ∘ S.projection k := by
104 classical
105 letI : Fintype Y := Fintype.ofFinite Y
106 letI : CompactSpace S.inverseLimit := inferInstance
107 let Uy : Y → Set S.inverseLimit := fun y => ρ ⁻¹' ({y} : Set Y)
108 have hUy_clopen : ∀ y, IsClopen (Uy y) := by
109 intro y
110 refine ⟨?_, ?_⟩
111 · simpa [Uy] using (isClosed_discrete ({y} : Set Y)).preimage hρ
112 · simpa [Uy] using (isOpen_discrete ({y} : Set Y)).preimage hρ
113 have hlocal :
114 ∀ y (x : S.inverseLimit), x ∈ Uy y →
115 ∃ i, ∃ V : Set (S.X i), IsClopen V ∧ S.projection i x ∈ V ∧ S.projection i ⁻¹' V ⊆ Uy y := by
116 intro y x hx
117 rcases S.exists_projection_preimage_subset hdir (hUy_clopen y).2 hx with
118 ⟨i, W, hWopen, hxW, hWU⟩
119 rcases exists_clopen_subset_of_mem_open (X := S.X i) hWopen hxW with ⟨V, hVclopen, hxV, hVW⟩
120 exact ⟨i, V, hVclopen, hxV, (Set.preimage_mono hVW).trans hWU⟩
121 choose ix V hVclopen hxV hVsub using hlocal
122 have hsubcover :
123 ∀ y, ∃ t : Finset ↥(Uy y), Uy y ⊆ ⋃ x ∈ t, S.projection (ix y x.1 x.2) ⁻¹' V y x.1 x.2 := by
124 intro y
125 have hcompactUy : IsCompact (Uy y) := (hUy_clopen y).1.isCompact
126 simpa using hcompactUy.elim_nhds_subcover'
127 (U := fun x hx => S.projection (ix y x hx) ⁻¹' V y x hx)
128 (hU := fun x hx =>
129 ((hVclopen y x hx).2.preimage (S.continuous_projection (ix y x hx))).mem_nhds (hxV y x hx))
130 choose t htcover using hsubcover
131 let i0 : I := Classical.choice ‹Nonempty I›
132 let used : Finset I :=
133 (Finset.univ.biUnion fun y : Y => (t y).image (fun x => ix y x.1 x.2)) ∪ {i0}
134 have hused_nonempty : used.Nonempty := ⟨i0, by simp only [Finset.union_singleton, Finset.mem_insert, Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image,
135 Subtype.exists, true_and, true_or, used]⟩
136 rcases exists_upperBound_finset (I := I) hdir used hused_nonempty with ⟨k, hk⟩
137 have hix_le_k : ∀ y (x : ↥(Uy y)) (hx : x ∈ t y), ix y x.1 x.2 ≤ k := by
138 intro y x hx
139 apply hk
140 apply Finset.mem_union.mpr
141 left
142 apply Finset.mem_biUnion.mpr
143 refine ⟨y, Finset.mem_univ y, ?_⟩
144 apply Finset.mem_image.mpr
145 exact ⟨x, hx, rfl⟩
146 let B : Y → Set (S.X k) := fun y =>
147 ⋃ x ∈ (Finset.univ : Finset ↥(t y)),
148 S.map (hix_le_k y x.1 x.2) ⁻¹' V y x.1.1 x.1.2
149 have hBclopen : ∀ y, IsClopen (B y) := by
150 intro y
151 refine ⟨?_, ?_⟩
152 · simpa [B] using
153 isClosed_biUnion_finset (s := (Finset.univ : Finset ↥(t y))) fun x hx =>
154 (hVclopen y x.1.1 x.1.2).1.preimage (S.continuous_map (hix_le_k y x.1 x.2))
155 · simpa [B] using
156 isOpen_biUnion (s := (((Finset.univ : Finset ↥(t y)) : Set ↥(t y)))) fun x hx =>
157 (hVclopen y x.1.1 x.1.2).2.preimage (S.continuous_map (hix_le_k y x.1 x.2))
158 have hUy_eq : ∀ y, Uy y = S.projection k ⁻¹' B y := by
159 intro y
160 ext z
161 constructor
162 · intro hz
163 have hzcover := htcover y hz
164 rcases mem_iUnion.1 hzcover with ⟨x, hxcover⟩
165 rcases mem_iUnion.1 hxcover with ⟨hx, hzV⟩
166 change S.projection k z ∈ B y
167 refine mem_iUnion.2 ⟨⟨x, hx⟩, ?_⟩
168 refine mem_iUnion.2 ⟨Finset.mem_univ _, ?_⟩
169 change S.map (hix_le_k y x hx) (S.projection k z) ∈ V y x.1 x.2
170 rw [S.projection_compatible z (ix y x.1 x.2) k (hix_le_k y x hx)]
171 exact hzV
172 · intro hz
173 have hzB : S.projection k z ∈ B y := hz
174 rcases mem_iUnion.1 hzB with ⟨x, hxB⟩
175 rcases mem_iUnion.1 hxB with ⟨_hxuniv, hzV⟩
176 have hzV' : S.projection (ix y x.1.1 x.1.2) z ∈ V y x.1.1 x.1.2 := by
177 change S.map (hix_le_k y x.1 x.2) (S.projection k z) ∈ V y x.1.1 x.1.2 at hzV
178 rw [S.projection_compatible z (ix y x.1.1 x.1.2) k (hix_le_k y x.1 x.2)] at hzV
179 exact hzV
180 exact hVsub y x.1.1 x.1.2 (by simpa using hzV')
181 have hRangeClosed : IsClosed (Set.range (S.projection k)) := by
182 exact (isCompact_range (S.continuous_projection k)).isClosed
183 let Z : Y → Set (S.X k) := fun y => B y ∩ Set.range (S.projection k)
184 have hZclosed : ∀ y, IsClosed (Z y) := by
185 intro y
186 exact (hBclopen y).1.inter hRangeClosed
187 have hZdisj : Set.univ.PairwiseDisjoint Z := by
188 intro y _ y' _ hyy'
189 change Disjoint (Z y) (Z y')
190 rw [Set.disjoint_left]
191 intro z hz hz'
192 rcases hz.2 with ⟨x, rfl⟩
193 have hx : x ∈ Uy y := by
194 rw [hUy_eq y]
195 exact hz.1
196 have hx' : x ∈ Uy y' := by
197 rw [hUy_eq y']
198 exact hz'.1
199 have hxy : ρ x = y := by simpa [Uy] using hx
200 have hxy' : ρ x = y' := by simpa [Uy] using hx'
201 exact hyy' (hxy.symm.trans hxy')
202 rcases exists_clopen_partition_of_clopen_cover
203 (X := S.X k) (I := Y)
204 (Z_closed := fun y => hZclosed y)
205 (D_clopen := fun _ => isClopen_univ)
206 (Z_subset_D := fun _ => by simp only [subset_univ, Z])
207 (Z_disj := hZdisj) with ⟨C, hCclopen, hZsubsetC, _hCsubsetD, hcoverC, hCdisj⟩
208 have hcoverC' : (Set.univ : Set (S.X k)) ⊆ ⋃ y, C y := by
209 simpa using hcoverC
210 have huniqC : ∀ z : S.X k, ∃! y, z ∈ C y := by
211 intro z
212 have hz : z ∈ ⋃ y, C y := hcoverC' (by simp only [mem_univ])
213 rcases mem_iUnion.1 hz with ⟨y, hy⟩
214 refine ⟨y, hy, ?_⟩
215 intro y' hy'
216 by_contra hne
217 have hne' : y ≠ y' := by simpa [eq_comm] using hne
218 have hdisj : Disjoint (C y) (C y') := hCdisj (by simp only [mem_univ]) (by simp only [mem_univ]) hne'
219 exact (Set.disjoint_left.1 hdisj) hy hy'
220 let ρ' : S.X k → Y := fun z => Classical.choose (huniqC z)
221 have hρ' : Continuous ρ' := by
222 rw [continuous_discrete_rng]
223 intro y
224 have hpre : ρ' ⁻¹' ({y} : Set Y) = C y := by
225 ext z
226 constructor
227 · intro hz
228 have hz' : z ∈ C (ρ' z) := (Classical.choose_spec (huniqC z)).1
229 simpa [Set.mem_preimage, Set.mem_singleton_iff.mp hz] using hz'
230 · intro hz
231 have hchoose_eq : y = ρ' z := (Classical.choose_spec (huniqC z)).2 y hz
232 simp only [hchoose_eq, mem_preimage, mem_singleton_iff]
233 simpa [hpre] using (hCclopen y).2
234 refine ⟨k, ρ', hρ', ?_⟩
235 funext x
236 change ρ x = ρ' (S.projection k x)
237 have hxUy : x ∈ Uy (ρ x) := by
238 simp only [mem_preimage, mem_singleton_iff, Uy]
239 have hxB : S.projection k x ∈ B (ρ x) := by
240 have : x ∈ S.projection k ⁻¹' B (ρ x) := by
241 rw [← hUy_eq (ρ x)]
242 exact hxUy
243 exact this
244 have hxZ : S.projection k x ∈ Z (ρ x) := ⟨hxB, ⟨x, rfl⟩⟩
245 have hxC : S.projection k x ∈ C (ρ x) := hZsubsetC (ρ x) hxZ
246 have hchoose_eq : ∀ y, S.projection k x ∈ C y → y = ρ' (S.projection k x) :=
247 (Classical.choose_spec (huniqC (S.projection k x))).2
248 exact hchoose_eq (ρ x) hxC
252section
254variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
256/-- Finite-subset product stages inherit their product group structures. -/
257instance finiteSubsetProductSystem_instGroup {α : Type u} (X : α → Type v)
258 [∀ a, TopologicalSpace (X a)] [∀ a, Group (X a)] :
259 ∀ s, Group ((finiteSubsetProductSystem X).X s) := by
260 intro s
261 classical
263 infer_instance
265/-- Finite-subset product stages inherit their product topological group structures. -/
266instance finiteSubsetProductSystem_instIsTopologicalGroup {α : Type u} (X : α → Type v)
267 [∀ a, TopologicalSpace (X a)] [∀ a, Group (X a)] [∀ a, IsTopologicalGroup (X a)] :
268 ∀ s, IsTopologicalGroup ((finiteSubsetProductSystem X).X s) := by
269 intro s
270 classical
272 infer_instance
274/-- The finite-subset product system is a group-valued inverse system. -/
275instance finiteSubsetProductSystem_instIsGroupSystem {α : Type u} (X : α → Type v)
276 [∀ a, TopologicalSpace (X a)] [∀ a, Group (X a)] :
278 map_one := by
279 intro i j hij
280 funext a
281 rfl
282 map_mul := by
283 intro i j hij x y
284 funext a
285 rfl
286 map_inv := by
287 intro i j hij x
288 funext a
289 rfl
291/-- A continuous homomorphism from an inverse limit of profinite groups to a
292finite discrete group factors through one of the projections. -/
293theorem InverseSystem.factors_through_projection_finite_group_hom [Nonempty I]
294 [∀ i, Group (S.X i)] [IsGroupSystem S] [∀ i, IsTopologicalGroup (S.X i)]
295 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
296 [∀ i, TotallyDisconnectedSpace (S.X i)]
297 (hdir : Directed (· ≤ ·) (id : I → I))
298 {H : Type w} [Group H] [TopologicalSpace H] [Finite H] [DiscreteTopology H]
299 (β : S.inverseLimit →* H) (_hβ : Continuous β) :
300 ∃ k : I, ∃ βk : S.X k →* H, Continuous βk ∧ β = βk ∘ S.projection k := by
301 classical
302 let rangeβ : S.inverseLimit → Set.range β := fun x => ⟨β x, ⟨x, rfl⟩⟩
303 letI : Nonempty (Set.range β) := ⟨⟨β 1, ⟨1, rfl⟩⟩⟩
304 have hrangeβ_continuous : Continuous rangeβ := by
305 exact Continuous.subtype_mk _hβ fun x => ⟨x, rfl⟩
306 rcases S.factors_through_projection_finite hdir rangeβ hrangeβ_continuous with
307 ⟨i0, β0range, hβ0range_continuous, hβ0range_fac⟩
308 let β0 : S.X i0 → H := fun x => (β0range x).1
309 have hβ0_continuous : Continuous β0 := continuous_subtype_val.comp hβ0range_continuous
310 have hβ0_fac : β = β0 ∘ S.projection i0 := by
311 funext x
312 exact congrArg Subtype.val (congrFun hβ0range_fac x)
313 let J : Set I := {i | i0 ≤ i}
314 have hdirJ : Directed (· ≤ ·) (id : J → J) := by
315 intro i j
316 rcases hdir i.1 j.1 with ⟨k, hik, hjk⟩
317 exact ⟨⟨k, i.2.trans hik⟩, hik, hjk⟩
318 have hcofinal : ∀ i : I, ∃ j : J, i ≤ j.1 := by
319 intro i
320 rcases hdir i i0 with ⟨k, hik, hi0k⟩
321 exact ⟨⟨k, hi0k⟩, hik⟩
322 let βJ : ∀ j : J, S.X j.1 → H := fun j => β0 ∘ S.map j.2
323 have hβJ_continuous : ∀ j : J, Continuous (βJ j) := by
324 intro j
325 dsimp [βJ]
326 exact hβ0_continuous.comp (S.continuous_map j.2)
327 have hβJ_map : ∀ {i j : J} (hij : i ≤ j) (x : S.X j.1), βJ i (S.map hij x) = βJ j x := by
328 intro i j hij x
329 dsimp [βJ, β0]
330 calc
331 (β0range (S.map i.2 (S.map hij x))).1 = (β0range (S.map (i.2.trans hij) x)).1 := by
332 rw [S.map_comp_apply i.2 hij]
333 _ = (β0range (S.map j.2 x)).1 := by
334 have hproof : i.2.trans hij = j.2 := Subsingleton.elim _ _
335 rw [hproof]
336 have hβJ_fac : ∀ j : J, β = βJ j ∘ S.projection j.1 := by
337 intro j
338 funext x
339 calc
340 β x = β0 (S.projection i0 x) := by
341 simpa [β0] using congrArg Subtype.val (congrFun hβ0range_fac x)
342 _ = β0 (S.map j.2 (S.projection j.1 x)) := by rw [S.projection_compatible x i0 j.1 j.2]
343 _ = βJ j (S.projection j.1 x) := rfl
344 let η : S.inverseLimit × S.inverseLimit → H × H := fun xy =>
345 (β xy.1 * β xy.2, β (xy.1 * xy.2))
346 let Δ : Set (H × H) := {z | z.1 = z.2}
347 have hη_delta : Set.range η ⊆ Δ := by
348 intro z hz
349 rcases hz with ⟨xy, rfl⟩
350 exact (β.map_mul xy.1 xy.2).symm
351 let E : J → Set (H × H) := fun j =>
352 Set.range fun xy : S.X j.1 × S.X j.1 => (βJ j xy.1 * βJ j xy.2, βJ j (xy.1 * xy.2))
353 have hE_mono : ∀ {i j : J}, i ≤ j → E j ⊆ E i := by
354 intro i j hij z hz
355 rcases hz with ⟨xy, rfl⟩
356 refine ⟨(S.map hij xy.1, S.map hij xy.2), ?_⟩
357 have h1 : βJ i (S.map hij xy.1) = βJ j xy.1 := hβJ_map hij xy.1
358 have h2 : βJ i (S.map hij xy.2) = βJ j xy.2 := hβJ_map hij xy.2
359 have h3 : βJ i (S.map hij xy.1 * S.map hij xy.2) = βJ j (xy.1 * xy.2) := by
360 calc
361 βJ i (S.map hij xy.1 * S.map hij xy.2)
362 = βJ i (S.map hij (xy.1 * xy.2)) := by
363 rw [IsGroupSystem.map_mul (S := S) hij xy.1 xy.2]
364 _ = βJ j (xy.1 * xy.2) := hβJ_map hij (xy.1 * xy.2)
365 apply Prod.ext
366 · change βJ i (S.map hij xy.1) * βJ i (S.map hij xy.2) =
367 βJ j xy.1 * βJ j xy.2
368 rw [h1, h2]
369 · exact h3
370 have hrange_eta_subset_iInter : Set.range η ⊆ ⋂ j, E j := by
371 intro z hz
372 rcases hz with ⟨xy, rfl⟩
373 rw [Set.mem_iInter]
374 intro j
375 refine ⟨(S.projection j.1 xy.1, S.projection j.1 xy.2), ?_⟩
376 apply Prod.ext
377 · have hx : β xy.1 = βJ j (S.projection j.1 xy.1) :=
378 congrFun (hβJ_fac j) xy.1
379 have hy : β xy.2 = βJ j (S.projection j.1 xy.2) :=
380 congrFun (hβJ_fac j) xy.2
381 change βJ j (S.projection j.1 xy.1) * βJ j (S.projection j.1 xy.2) =
382 β xy.1 * β xy.2
383 rw [← hx, ← hy]
384 · calc
385 βJ j (S.projection j.1 xy.1 * S.projection j.1 xy.2)
386 = βJ j (S.projection j.1 (xy.1 * xy.2)) := by
387 rw [projection_mul (S := S) j.1 xy.1 xy.2]
388 _ = β (xy.1 * xy.2) := by
389 simpa [Function.comp] using (congrFun (hβJ_fac j) (xy.1 * xy.2)).symm
390 have hiInter_E_subset_range : (⋂ j, E j) ⊆ Set.range η := by
391 intro z hz
392 let Yset : ∀ j : J, Set (S.X j.1 × S.X j.1) := fun j =>
393 {xy | (βJ j xy.1 * βJ j xy.2, βJ j (xy.1 * xy.2)) = z}
394 have hYclosed : ∀ j : J, IsClosed (Yset j) := by
395 intro j
396 have hleft :
397 Continuous fun xy : S.X j.1 × S.X j.1 => βJ j xy.1 * βJ j xy.2 :=
398 ((hβJ_continuous j).comp continuous_fst).mul ((hβJ_continuous j).comp continuous_snd)
399 have hright :
400 Continuous fun xy : S.X j.1 × S.X j.1 => βJ j (xy.1 * xy.2) :=
401 (hβJ_continuous j).comp continuous_mul
402 exact isClosed_singleton.preimage (hleft.prodMk hright)
403 let T : InverseSystem (I := J) := {
404 X := fun j => Yset j
405 topologicalSpace := fun _ => inferInstance
406 map := fun {i j} hij xy =>
407 ⟨(S.map hij xy.1.1, S.map hij xy.1.2), by
408 have h1 : βJ i (S.map hij xy.1.1) = βJ j xy.1.1 := hβJ_map hij xy.1.1
409 have h2 : βJ i (S.map hij xy.1.2) = βJ j xy.1.2 := hβJ_map hij xy.1.2
410 have h3 : βJ i (S.map hij xy.1.1 * S.map hij xy.1.2) = βJ j (xy.1.1 * xy.1.2) := by
411 calc
412 βJ i (S.map hij xy.1.1 * S.map hij xy.1.2)
413 = βJ i (S.map hij (xy.1.1 * xy.1.2)) := by
414 rw [IsGroupSystem.map_mul (S := S) hij xy.1.1 xy.1.2]
415 _ = βJ j (xy.1.1 * xy.1.2) := hβJ_map hij (xy.1.1 * xy.1.2)
416 have hxy : (βJ j xy.1.1 * βJ j xy.1.2, βJ j (xy.1.1 * xy.1.2)) = z := by
417 change (βJ j xy.1.1 * βJ j xy.1.2, βJ j (xy.1.1 * xy.1.2)) = z
418 exact xy.2
419 change
420 (βJ i (S.map hij xy.1.1) * βJ i (S.map hij xy.1.2),
421 βJ i (S.map hij xy.1.1 * S.map hij xy.1.2)) = z
422 rw [h1, h2, h3]
423 exact hxy⟩
424 continuous_map := fun {i j} hij =>
425 Continuous.subtype_mk
426 (((S.continuous_map hij).comp (continuous_fst.comp continuous_subtype_val)).prodMk
427 ((S.continuous_map hij).comp (continuous_snd.comp continuous_subtype_val)))
428 (fun xy => by
429 have h1 : βJ i (S.map hij xy.1.1) = βJ j xy.1.1 := hβJ_map hij xy.1.1
430 have h2 : βJ i (S.map hij xy.1.2) = βJ j xy.1.2 := hβJ_map hij xy.1.2
431 have h3 : βJ i (S.map hij xy.1.1 * S.map hij xy.1.2) = βJ j (xy.1.1 * xy.1.2) := by
432 calc
433 βJ i (S.map hij xy.1.1 * S.map hij xy.1.2)
434 = βJ i (S.map hij (xy.1.1 * xy.1.2)) := by
435 rw [IsGroupSystem.map_mul (S := S) hij xy.1.1 xy.1.2]
436 _ = βJ j (xy.1.1 * xy.1.2) := hβJ_map hij (xy.1.1 * xy.1.2)
437 have hxy : (βJ j xy.1.1 * βJ j xy.1.2, βJ j (xy.1.1 * xy.1.2)) = z := by
438 change (βJ j xy.1.1 * βJ j xy.1.2, βJ j (xy.1.1 * xy.1.2)) = z
439 exact xy.2
440 change
441 (βJ i (S.map hij xy.1.1) * βJ i (S.map hij xy.1.2),
442 βJ i (S.map hij xy.1.1 * S.map hij xy.1.2)) = z
443 rw [h1, h2, h3]
444 exact hxy)
445 map_id := fun j => by
446 funext xy
447 apply Subtype.ext
448 apply Prod.ext
449 · exact S.map_id_apply j.1 xy.1.1
450 · exact S.map_id_apply j.1 xy.1.2
451 map_comp := fun {i j k} hij hjk => by
452 funext xy
453 apply Subtype.ext
454 apply Prod.ext
455 · exact S.map_comp_apply hij hjk xy.1.1
456 · exact S.map_comp_apply hij hjk xy.1.2 }
457 have hzall : ∀ j : J, z ∈ E j := by
458 rw [Set.mem_iInter] at hz
459 exact hz
460 have hnonemptyT : ∀ j : J, Nonempty (T.X j) := by
461 intro j
462 rcases hzall j with ⟨xy, hxy⟩
463 exact ⟨⟨xy, hxy⟩⟩
464 letI : ∀ j : J, Nonempty (T.X j) := hnonemptyT
465 letI : ∀ j : J, CompactSpace (T.X j) := fun j => by
466 simpa [T] using (isCompact_iff_compactSpace.mp (hYclosed j).isCompact)
467 letI : ∀ j : J, T2Space (T.X j) := fun _ => inferInstance
468 rcases T.nonempty_inverseLimit hdirJ with ⟨u⟩
469 let xlim : (S.restrict J).inverseLimit := by
470 refine ⟨fun j => (u.1 j).1.1, ?_⟩
471 intro i j hij
472 exact congrArg Prod.fst (congrArg Subtype.val (u.2 i j hij))
473 let ylim : (S.restrict J).inverseLimit := by
474 refine ⟨fun j => (u.1 j).1.2, ?_⟩
475 intro i j hij
476 exact congrArg Prod.snd (congrArg Subtype.val (u.2 i j hij))
477 letI : ∀ j : J, Group ((S.restrict J).X j) := fun j => by
478 change Group (S.X j.1)
479 infer_instance
480 let e := S.homeomorph_restrict_cofinal J hdirJ hcofinal
481 let j0 : J := ⟨i0, le_rfl⟩
482 have hu0 :
483 (βJ j0 ((u.1 j0).1.1) * βJ j0 ((u.1 j0).1.2),
484 βJ j0 (((u.1 j0).1.1) * ((u.1 j0).1.2))) = z := by
485 exact (u.1 j0).2
486 have hπx : (S.restrict J).projection j0 xlim = S.projection j0.1 (e.symm xlim) := by
487 simpa [e, xlim] using
488 congrFun (S.π_comp_homeomorph_restrict_cofinal J hdirJ hcofinal j0) (e.symm xlim)
489 have hπy : (S.restrict J).projection j0 ylim = S.projection j0.1 (e.symm ylim) := by
490 simpa [e, ylim] using
491 congrFun (S.π_comp_homeomorph_restrict_cofinal J hdirJ hcofinal j0) (e.symm ylim)
492 refine ⟨(e.symm xlim, e.symm ylim), ?_⟩
493 apply Prod.ext
494 · calc
495 β (e.symm xlim) * β (e.symm ylim)
496 = βJ j0 ((S.restrict J).projection j0 xlim) * βJ j0 ((S.restrict J).projection j0 ylim) := by
497 have hxβ : β (e.symm xlim) = βJ j0 ((S.restrict J).projection j0 xlim) := by
498 calc
499 β (e.symm xlim) = βJ j0 (S.projection j0.1 (e.symm xlim)) := by
500 simpa [Function.comp] using congrFun (hβJ_fac j0) (e.symm xlim)
501 _ = βJ j0 ((S.restrict J).projection j0 xlim) := by rw [← hπx]
502 have hyβ : β (e.symm ylim) = βJ j0 ((S.restrict J).projection j0 ylim) := by
503 calc
504 β (e.symm ylim) = βJ j0 (S.projection j0.1 (e.symm ylim)) := by
505 simpa [Function.comp] using congrFun (hβJ_fac j0) (e.symm ylim)
506 _ = βJ j0 ((S.restrict J).projection j0 ylim) := by rw [← hπy]
507 rw [hxβ, hyβ]
508 _ = z.1 := by simpa [xlim, ylim] using congrArg Prod.fst hu0
509 · calc
510 β (e.symm xlim * e.symm ylim)
511 = βJ j0 (S.projection j0.1 (e.symm xlim * e.symm ylim)) := by
512 simpa [Function.comp] using congrFun (hβJ_fac j0) (e.symm xlim * e.symm ylim)
513 _ = βJ j0 (S.projection j0.1 (e.symm xlim) * S.projection j0.1 (e.symm ylim)) := by
514 rw [projection_mul (S := S) j0.1 (e.symm xlim) (e.symm ylim)]
515 _ = βJ j0 ((S.restrict J).projection j0 xlim * (S.restrict J).projection j0 ylim) := by
516 rw [← hπx, ← hπy]
517 _ = z.2 := by simpa [xlim, ylim] using congrArg Prod.snd hu0
518 have hnot_iInter : ∀ {t : H × H}, t ∉ Set.range η → ∃ j : J, t ∉ E j := by
519 intro t ht
520 by_contra hno
521 apply ht
522 apply hiInter_E_subset_range
523 rw [Set.mem_iInter]
524 intro j
525 by_contra htj
526 exact hno ⟨j, htj⟩
527 let j0 : J := ⟨i0, le_rfl⟩
528 let jchoose : ∀ t : H × H, t ∉ Set.range η → J := fun t ht => Classical.choose (hnot_iInter ht)
529 have hjchoose : ∀ t ht, t ∉ E (jchoose t ht) := by
530 intro t ht
531 exact Classical.choose_spec (hnot_iInter ht)
532 letI : Fintype H := Fintype.ofFinite H
533 letI : Fintype (H × H) := Fintype.ofFinite (H × H)
534 let used : Finset J := Finset.univ.image fun t : H × H =>
535 if ht : t ∈ Set.range η then j0 else jchoose t ht
536 have hused_nonempty : used.Nonempty := by
537 refine ⟨if h : ((1 : H), (1 : H)) ∈ Set.range η then j0 else jchoose ((1 : H), (1 : H)) h, ?_⟩
538 refine Finset.mem_image.mpr ?_
539 exact ⟨((1 : H), (1 : H)), Finset.mem_univ _, by split_ifs <;> rfl⟩
540 rcases exists_upperBound_finset (I := J) hdirJ used hused_nonempty with ⟨k, hk⟩
541 have hrange_eta_subset_Ek : Set.range η ⊆ E k := by
542 intro t ht
543 have hmem : t ∈ ⋂ j, E j := hrange_eta_subset_iInter ht
544 rw [Set.mem_iInter] at hmem
545 exact hmem k
546 have hEk_subset_range_eta : E k ⊆ Set.range η := by
547 intro t ht
548 by_cases htr : t ∈ Set.range η
549 · exact htr
550 · have hmem_used : (if ht' : t ∈ Set.range η then j0 else jchoose t ht') ∈ used := by
551 refine Finset.mem_image.mpr ?_
552 exact ⟨t, Finset.mem_univ _, by split_ifs; rfl⟩
553 have hle : (if ht' : t ∈ Set.range η then j0 else jchoose t ht') ≤ k := hk _ hmem_used
554 have ht' : t ∈ E (if ht' : t ∈ Set.range η then j0 else jchoose t ht') := hE_mono hle ht
555 simp only [htr, ↓reduceDIte, hjchoose] at ht'
556 have hEk_subset_delta : E k ⊆ Δ := by
557 intro t ht
558 exact hη_delta (hEk_subset_range_eta ht)
559 let βkFun : S.X k.1 → H := βJ k
560 have hβk_mul : ∀ x y : S.X k.1, βkFun (x * y) = βkFun x * βkFun y := by
561 intro x y
562 have hxy : (βkFun x * βkFun y, βkFun (x * y)) ∈ E k := ⟨(x, y), rfl⟩
563 have hxyΔ : (βkFun x * βkFun y, βkFun (x * y)) ∈ Δ := hEk_subset_delta hxy
564 simpa [Δ] using hxyΔ.symm
565 have hβk_one : βkFun 1 = 1 := by
566 have h := hβk_mul 1 1
567 have h' := congrArg (fun t : H => t * (βkFun 1)⁻¹) h
568 simpa [mul_assoc] using h'.symm
569 let βk : S.X k.1 →* H :=
570 { toFun := βkFun
571 map_one' := hβk_one
572 map_mul' := hβk_mul }
573 have hβk_continuous : Continuous βk := by
574 change Continuous βkFun
575 exact hβJ_continuous k
576 refine ⟨k.1, βk, hβk_continuous, ?_⟩
577 exact hβJ_fac k
579/-- A continuous additive homomorphism from an inverse limit of profinite additive groups to a
580finite discrete additive group factors through one finite stage. -/
581theorem InverseSystem.factors_through_projection_finite_addMonoidHom [Nonempty I]
582 [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S] [∀ i, IsTopologicalAddGroup (S.X i)]
583 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
584 [∀ i, TotallyDisconnectedSpace (S.X i)]
585 (hdir : Directed (· ≤ ·) (id : I → I))
586 {H : Type w} [AddCommGroup H] [TopologicalSpace H] [Finite H] [DiscreteTopology H]
587 (β : S.inverseLimit →+ H) (hβ : Continuous β) :
588 ∃ k : I, ∃ βk : S.X k →+ H, Continuous βk ∧ β = βk ∘ S.projection k := by
589 classical
590 let T : InverseSystem (I := I) :=
591 { X := fun i => Multiplicative (S.X i)
592 topologicalSpace := fun _ => inferInstance
593 map := fun {i j} hij x => Multiplicative.ofAdd (S.map hij x.toAdd)
594 continuous_map := fun {i j} hij => by
597 exact ei.continuous_toFun.comp ((S.continuous_map hij).comp ej.continuous_invFun)
598 map_id := fun i => by
599 funext x
600 apply Multiplicative.ext
601 change S.map (le_rfl : i ≤ i) x.toAdd = x.toAdd
602 exact S.map_id_apply i x.toAdd
603 map_comp := fun {i j k} hij hjk => by
604 funext x
605 apply Multiplicative.ext
606 change S.map hij (S.map hjk x.toAdd) = S.map (hij.trans hjk) x.toAdd
607 exact S.map_comp_apply hij hjk x.toAdd }
608 letI : ∀ i, Group (T.X i) := fun _ => inferInstance
609 letI : IsGroupSystem T :=
610 { map_one := by
611 intro i j hij
612 apply Multiplicative.ext
613 exact IsAddGroupSystem.map_zero (S := S) hij
614 map_mul := by
615 intro i j hij x y
616 apply Multiplicative.ext
617 exact IsAddGroupSystem.map_add (S := S) hij x.toAdd y.toAdd
618 map_inv := by
619 intro i j hij x
620 apply Multiplicative.ext
621 exact IsAddGroupSystem.map_neg (S := S) hij x.toAdd }
622 letI : ∀ i, IsTopologicalGroup (T.X i) := fun _ => inferInstance
623 letI : ∀ i, CompactSpace (T.X i) := fun _ => inferInstance
624 letI : ∀ i, T2Space (T.X i) := fun i =>
626 letI : ∀ i, TotallyDisconnectedSpace (T.X i) := fun i =>
627 (additiveMultiplicativeHomeomorph (S.X i)).totallyDisconnectedSpace
628 let toAddLimit : T.inverseLimit → S.inverseLimit := fun x =>
629 ⟨fun i => (T.projection i x).toAdd, by
630 intro i j hij
631 change S.map hij ((T.projection j x).toAdd) = (T.projection i x).toAdd
632 exact congrArg Multiplicative.toAdd (T.projection_compatible x i j hij)⟩
633 let toMulLimit : S.inverseLimit → T.inverseLimit := fun x =>
634 ⟨fun i => Multiplicative.ofAdd (S.projection i x), by
635 intro i j hij
636 apply Multiplicative.ext
637 change S.map hij (S.projection j x) = S.projection i x
638 exact S.projection_compatible x i j hij⟩
639 let toAddLimitMulHom : T.inverseLimit →* Multiplicative S.inverseLimit :=
640 { toFun := fun x => Multiplicative.ofAdd (toAddLimit x)
641 map_one' := by
642 apply Multiplicative.ext
643 apply S.ext
644 intro i
645 rfl
646 map_mul' := by
647 intro x y
648 apply Multiplicative.ext
649 apply S.ext
650 intro i
651 rfl }
652 let βMul : T.inverseLimit →* Multiplicative H :=
653 (AddMonoidHom.toMultiplicative β).comp toAddLimitMulHom
654 have htoAddLimit_continuous : Continuous toAddLimit := by
655 exact Continuous.subtype_mk
656 (continuous_pi fun i =>
657 (additiveMultiplicativeHomeomorph (S.X i)).continuous_invFun.comp
658 (T.continuous_projection i))
659 (fun x => (toAddLimit x).2)
660 have hβMul_continuous : Continuous βMul := by
661 change Continuous fun x => Multiplicative.ofAdd (β (toAddLimit x))
662 exact (additiveMultiplicativeHomeomorph H).continuous_toFun.comp
663 (hβ.comp htoAddLimit_continuous)
664 letI : Finite (Multiplicative H) := Finite.of_equiv H Multiplicative.ofAdd
665 rcases T.factors_through_projection_finite_group_hom hdir βMul hβMul_continuous with
666 ⟨k, γk, hγk_continuous, hγk_fac⟩
667 let βk : S.X k →+ H :=
668 { toFun := fun x => (γk (Multiplicative.ofAdd x)).toAdd
669 map_zero' := by
670 exact congrArg Multiplicative.toAdd γk.map_one
671 map_add' := by
672 intro x y
673 exact congrArg Multiplicative.toAdd
674 (γk.map_mul (Multiplicative.ofAdd x) (Multiplicative.ofAdd y)) }
675 have hβk_continuous : Continuous βk := by
676 change Continuous fun x : S.X k => (γk (Multiplicative.ofAdd x)).toAdd
677 exact (additiveMultiplicativeHomeomorph H).continuous_invFun.comp
678 (hγk_continuous.comp (additiveMultiplicativeHomeomorph (S.X k)).continuous_toFun)
679 refine ⟨k, βk, hβk_continuous, ?_⟩
680 funext x
681 have hlim : toAddLimit (toMulLimit x) = x := by
682 apply S.ext
683 intro i
684 rfl
685 have hpoint := congrArg Multiplicative.toAdd (congrFun hγk_fac (toMulLimit x))
686 have hleft : (βMul (toMulLimit x)).toAdd = β x := by
687 simp only [MonoidHom.coe_comp, AddMonoidHom.coe_toMultiplicative, MonoidHom.coe_mk, OneHom.coe_mk,
688 Function.comp_apply, hlim, toAdd_ofAdd, βMul, toAddLimitMulHom]
689 have hright :
690 (γk (T.projection k (toMulLimit x))).toAdd = βk (S.projection k x) := by
691 rfl
692 exact hleft.symm.trans (hpoint.trans hright)
694end
696end ProCGroups.InverseSystems