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