Source: ProCGroups.CompletedGroupAlgebra.Separation
1import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.GroupLike
2import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison
4/-!
5# Completed Group Algebra / Separation
7This module contains separation lemmas for completed group algebras using finite quotients.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
19open ProCGroups.Completion
21universe u v w
23variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
24variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
26variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
28omit [T2Space G] in
29/--
30A finite set of nontrivial elements in a profinite group can be avoided by one open-normal
31finite quotient. This is the finite-support separation input in Lemma 5.3.5(a).
32-/
33theorem exists_completedGroupAlgebraIndex_avoids_finset
34 (s : Finset G)
35 (hs : ∀ x ∈ s, x ≠ 1) :
36 ∃ U : CompletedGroupAlgebraIndex G,
37 ∀ x ∈ s, x ∉ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
38 classical
39 revert hs
40 refine Finset.induction_on s ?_ ?_
41 · intro _hs
42 exact ⟨terminalCompletedGroupAlgebraIndex G,
43 by simp only [Finset.notMem_empty, OpenSubgroup.mem_toSubgroup, IsEmpty.forall_iff,
44 implies_true]⟩
45 · intro a s has ih hs
46 have ha : a ≠ 1 := hs a (by simp only [Finset.mem_insert, true_or])
47 rcases ProCGroups.ProC.exists_openNormalSubgroup_not_mem (G := G) ha with ⟨A, hA⟩
48 have hs' : ∀ x ∈ s, x ≠ 1 := by
49 intro x hx
50 exact hs x (by simp only [Finset.mem_insert, hx, or_true])
51 rcases ih hs' with ⟨U, hU⟩
52 let U0 : OpenNormalSubgroup G := (OrderDual.ofDual U).1
53 let W0 : OpenNormalSubgroup G := A ⊓ U0
54 let W : CompletedGroupAlgebraIndex G := OrderDual.toDual
55 ⟨W0, ProCGroups.openNormalSubgroup_finiteQuotient (G := G) W0⟩
56 refine ⟨W, ?_⟩
57 intro x hx hxW
58 change x ∈ A ⊓ U0 at hxW
59 rw [Finset.mem_insert] at hx
60 rcases hx with rfl | hx
61 · exact hA hxW.1
62 · exact hU x hx hxW.2
64omit [TopologicalSpace R] [IsTopologicalRing R]
65 [T2Space G]
66 H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
67/--
68For a finite-support group-algebra element and a chosen basis element \(g\), one finite quotient
69separates the image of \(g\) from all other support points.
70-/
71theorem exists_completedGroupAlgebraIndex_separating_support
72 (x : MonoidAlgebra R G) (g : G) :
73 ∃ U : CompletedGroupAlgebraIndex G,
74 ∀ h ∈ x.coeff.support, h ≠ g →
75 openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h ≠
76 openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U
77 g := by
78 classical
79 let bad : Finset G := (x.coeff.support.erase g).image fun h => h⁻¹ * g
80 have hbad : ∀ y ∈ bad, y ≠ 1 := by
81 intro y hy
82 rcases Finset.mem_image.mp hy with ⟨h, hh, rfl⟩
83 intro h1
84 have hg : h = g := by
85 have hmul := congrArg (fun t : G => h * t) h1
86 have hg' : g = h := by
87 simpa [mul_assoc] using hmul
88 exact hg'.symm
89 exact (Finset.mem_erase.mp hh).1 hg
90 rcases exists_completedGroupAlgebraIndex_avoids_finset (G := G) bad hbad with
91 ⟨U, hU⟩
92 refine ⟨U, ?_⟩
93 intro h hh hne heq
94 have hbadmem : h⁻¹ * g ∈ bad := by
95 exact Finset.mem_image.mpr ⟨h, Finset.mem_erase.mpr ⟨hne, hh⟩, rfl⟩
96 have hmem :
97 h⁻¹ * g ∈ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
98 exact QuotientGroup.eq.1 heq
99 exact hU (h⁻¹ * g) hbadmem hmem
101omit [TopologicalSpace R] [IsTopologicalRing R]
102 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
103 H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
104/--
105If a finite quotient separates \(g\) from the other support points of \(x\), then the
106coefficient of the image of \(g\) in the quotient group algebra is exactly the original
107coefficient of \(g\).
108-/
109theorem completedGroupAlgebraStageMap_coeff_of_support_separated
110 (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) (g : G)
111 (hsep : ∀ h ∈ x.coeff.support, h ≠ g →
112 openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h ≠
113 openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) :
114 (completedGroupAlgebraStageMap R G U x).coeff
115 (openNormalSubgroupInClassProj
116 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) =
117 x.coeff g := by
118 classical
119 change (Finsupp.mapDomain
120 (openNormalSubgroupInClassProj
121 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U) x.coeff)
122 (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) =
123 x.coeff g
124 rw [Finsupp.mapDomain, Finsupp.sum_apply]
125 rw [Finsupp.sum_eq_single g]
126 · simp only [Finsupp.single_eq_same]
127 · intro h hh hne
128 exact Finsupp.single_eq_of_ne fun heq =>
129 hsep h (Finsupp.mem_support_iff.mpr hh) hne heq.symm
130 · intro _hg
131 simp only [Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]
133omit R [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
134 [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
135 H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
136/--
137A finite set of nontrivial elements in a pro-\(C\) group can be avoided by one open normal
138\(C\)-quotient. This is the \(C\)-indexed finite-support separation input in Lemma 5.3.5(a).
139-/
140theorem exists_completedGroupAlgebraIndexInClass_avoids_finset
141 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
142 (hG : HasOpenNormalBasisInClass C G) (s : Finset G) (hs : ∀ x ∈ s, x ≠ 1) :
143 ∃ U : CompletedGroupAlgebraIndexInClass G C,
144 ∀ x ∈ s, x ∉ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
145 classical
146 revert hs
147 refine Finset.induction_on s ?_ ?_
148 · intro _hs
149 letI : Nonempty (OpenNormalSubgroupInClass C G) :=
150 HasOpenNormalBasisInClass.openNormalSubgroupInClass_nonempty hG
151 letI : Nonempty (CompletedGroupAlgebraIndexInClass G C) := inferInstance
152 exact ⟨Classical.choice inferInstance, by simp only [Finset.notMem_empty,
153 OpenSubgroup.mem_toSubgroup, IsEmpty.forall_iff, implies_true]⟩
154 · intro a s has ih hs
155 have ha : a ≠ 1 := hs a (by simp only [Finset.mem_insert, true_or])
156 rcases hG.exists_openNormalSubgroupInClass_not_mem ha with ⟨A, hA⟩
157 have hs' : ∀ x ∈ s, x ≠ 1 := by
158 intro x hx
159 exact hs x (by simp only [Finset.mem_insert, hx, or_true])
160 rcases ih hs' with ⟨U, hU⟩
161 let Aidx : CompletedGroupAlgebraIndexInClass G C := OrderDual.toDual A
162 rcases directed_openNormalSubgroupInClass (C := C) (G := G) hForm Aidx U with
163 ⟨W, hAW, hUW⟩
164 refine ⟨W, ?_⟩
165 intro x hx hxW
166 rw [Finset.mem_insert] at hx
167 rcases hx with rfl | hx
168 · exact hA (hAW hxW)
169 · exact hU x hx (hUW hxW)
171omit R [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
172 [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
173 H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
174/--
175For any finitely supported family on a pro-\(C\) group and a chosen basis point \(g\), one
176\(C\)-quotient separates the image of \(g\) from all other support points.
177-/
178theorem exists_completedGroupAlgebraIndexInClass_separating_finsupp_support
179 {M : Type w} [Zero M]
180 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
181 (hG : HasOpenNormalBasisInClass C G) (x : G →₀ M) (g : G) :
182 ∃ U : CompletedGroupAlgebraIndexInClass G C,
183 ∀ h ∈ x.support, h ≠ g →
184 openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
185 openNormalSubgroupInClassProj (C := C) (G := G) U g := by
186 classical
187 let bad : Finset G := (x.support.erase g).image fun h => h⁻¹ * g
188 have hbad : ∀ y ∈ bad, y ≠ 1 := by
189 intro y hy
190 rcases Finset.mem_image.mp hy with ⟨h, hh, rfl⟩
191 intro h1
192 have hg : h = g := by
193 have hmul := congrArg (fun t : G => h * t) h1
194 have hg' : g = h := by
195 simpa [mul_assoc] using hmul
196 exact hg'.symm
197 exact (Finset.mem_erase.mp hh).1 hg
198 rcases exists_completedGroupAlgebraIndexInClass_avoids_finset
199 (G := G) C hForm hG bad hbad with
200 ⟨U, hU⟩
201 refine ⟨U, ?_⟩
202 intro h hh hne heq
203 have hbadmem : h⁻¹ * g ∈ bad := by
204 exact Finset.mem_image.mpr ⟨h, Finset.mem_erase.mpr ⟨hne, hh⟩, rfl⟩
205 have hmem :
206 h⁻¹ * g ∈ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
207 exact QuotientGroup.eq.1 heq
208 exact hU (h⁻¹ * g) hbadmem hmem
210omit [TopologicalSpace R] [IsTopologicalRing R]
211 [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
212 H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
213/--
214For a finite-support group-algebra element and a chosen basis element \(g\), one \(C\)-quotient
215separates the image of \(g\) from all other support points.
216-/
217theorem exists_completedGroupAlgebraIndexInClass_separating_support
218 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
219 (hG : HasOpenNormalBasisInClass C G) (x : MonoidAlgebra R G) (g : G) :
220 ∃ U : CompletedGroupAlgebraIndexInClass G C,
221 ∀ h ∈ x.coeff.support, h ≠ g →
222 openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
223 openNormalSubgroupInClassProj (C := C) (G := G) U g :=
224 exists_completedGroupAlgebraIndexInClass_separating_finsupp_support
225 (G := G) C hForm hG x.coeff g
227omit [TopologicalSpace R] [IsTopologicalRing R]
228 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
229 H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
230/--
231If a \(C\)-quotient separates \(g\) from the other support points of \(x\), then the coefficient
232of the image of \(g\) in the quotient group algebra is exactly the original coefficient of
233\(g\).
234-/
235theorem completedGroupAlgebraStageMapInClass_coeff_of_support_separated
236 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
237 (x : MonoidAlgebra R G) (g : G)
238 (hsep : ∀ h ∈ x.coeff.support, h ≠ g →
239 openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
240 openNormalSubgroupInClassProj (C := C) (G := G) U g) :
241 (completedGroupAlgebraStageMapInClass C R G U x).coeff
242 (openNormalSubgroupInClassProj (C := C) (G := G) U g) =
243 x.coeff g := by
244 classical
245 change (Finsupp.mapDomain
246 (openNormalSubgroupInClassProj (C := C) (G := G) U) x.coeff)
247 (openNormalSubgroupInClassProj (C := C) (G := G) U g) =
248 x.coeff g
249 rw [Finsupp.mapDomain, Finsupp.sum_apply]
250 rw [Finsupp.sum_eq_single g]
251 · simp only [Finsupp.single_eq_same]
252 · intro h hh hne
253 exact Finsupp.single_eq_of_ne fun heq =>
254 hsep h (Finsupp.mem_support_iff.mpr hh) hne heq.symm
255 · intro _hg
256 simp only [Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]
258omit [T2Space G] in
259/--
260In Lemma 5.3.5(a), fixed-coefficient form, the canonical map from the abstract group algebra to
261the completed group algebra is injective for profinite G. Equivalently, the kernels of the
262finite group-quotient maps have trivial intersection.
263-/
264theorem injective_toCompletedGroupAlgebraRingHom
265 : Function.Injective (toCompletedGroupAlgebraRingHom R G) := by
266 intro x y hxy
267 apply MonoidAlgebra.ext
268 apply Finsupp.ext
269 intro g
270 have hcoeff : (x - y).coeff g = 0 := by
271 rcases exists_completedGroupAlgebraIndex_separating_support (R := R) (G := G)
272 (x - y) g with
273 ⟨U, hsep⟩
274 have hstage_eq : completedGroupAlgebraStageMap R G U x =
275 completedGroupAlgebraStageMap R G U y := by
276 have hp := congrArg (fun z : CompletedGroupAlgebraCarrier R G =>
277 completedGroupAlgebraProjection R G U z) hxy
278 change completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
279 completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G y) at hp
280 simpa [completedGroupAlgebraProjection_toCompletedGroupAlgebra] using hp
281 have hstage : completedGroupAlgebraStageMap R G U (x - y) = 0 := by
282 rw [map_sub, hstage_eq, sub_self]
283 have hstage_coeff :
284 (completedGroupAlgebraStageMap R G U (x - y)).coeff
285 (openNormalSubgroupInClassProj
286 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = 0 := by
287 simpa only [MonoidAlgebra.coeff_zero, Finsupp.zero_apply] using congrArg
288 (fun z : CompletedGroupAlgebraStage R G U =>
289 z.coeff (openNormalSubgroupInClassProj
290 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g))
291 hstage
292 rw [completedGroupAlgebraStageMap_coeff_of_support_separated
293 (R := R) (G := G) U (x - y) g hsep] at hstage_coeff
294 simpa using hstage_coeff
295 exact sub_eq_zero.mp (by simpa using hcoeff)
297omit [T2Space G] in
298/--
299The dense map from the ordinary group algebra into the completed group algebra has trivial
300kernel after separation by all finite quotient stages.
301-/
302theorem toCompletedGroupAlgebraRingHom_ker_eq_bot
303 : RingHom.ker (toCompletedGroupAlgebraRingHom R G) = ⊥ :=
304 (RingHom.injective_iff_ker_eq_bot (toCompletedGroupAlgebraRingHom R G)).mp
305 (injective_toCompletedGroupAlgebraRingHom (R := R) (G := G))
307omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
308/-- The kernel of the map to \(\widehat{R[G]}\) is the intersection of the finite-stage kernels. -/
309theorem toCompletedGroupAlgebraRingHom_ker_eq_iInf_stageMap_ker :
310 RingHom.ker (toCompletedGroupAlgebraRingHom R G) =
311 ⨅ U : CompletedGroupAlgebraIndex G, RingHom.ker (completedGroupAlgebraStageMap R G U) := by
312 ext x
313 constructor
314 · intro hx
315 rw [RingHom.mem_ker] at hx
316 rw [Submodule.mem_iInf]
317 intro U
318 rw [RingHom.mem_ker]
319 have hU := congrArg (fun y : CompletedGroupAlgebraCarrier R G =>
320 completedGroupAlgebraProjection R G U y) hx
321 change completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
322 completedGroupAlgebraProjection R G U (0 : CompletedGroupAlgebraCarrier R G) at hU
323 simpa [completedGroupAlgebraProjection_toCompletedGroupAlgebra] using hU
324 · intro hx
325 rw [RingHom.mem_ker]
326 apply completedGroupAlgebra_ext (R := R) (G := G)
327 intro U
328 change completedGroupAlgebraStageMap R G U x = 0
329 exact (Submodule.mem_iInf
330 (p := fun U : CompletedGroupAlgebraIndex G =>
331 RingHom.ker (completedGroupAlgebraStageMap R G U))).1 hx U
333omit [T2Space G] in
334/-- Fixed-coefficient finite-stage kernel-family form of Lemma 5.3.5(a). -/
335theorem iInf_completedGroupAlgebraStageMap_ker_eq_bot
336 : (⨅ U : CompletedGroupAlgebraIndex G,
337 RingHom.ker (completedGroupAlgebraStageMap R G U)) = ⊥ := by
338 rw [← toCompletedGroupAlgebraRingHom_ker_eq_iInf_stageMap_ker (R := R) (G := G),
339 toCompletedGroupAlgebraRingHom_ker_eq_bot (R := R) (G := G)]
341omit [CompactSpace G] [TotallyDisconnectedSpace G] in
342/--
343\(C\)-indexed form of Lemma 5.3.5(a): for a pro-\(C\) group, the canonical map from the abstract
344group algebra to \(\widehat{R[G]}_{C}\) is injective.
345-/
346theorem injective_toCompletedGroupAlgebraInClassRingHom
347 (C : ProCGroups.FiniteGroupClass.{v})
348 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
349 Function.Injective (toCompletedGroupAlgebraInClassRingHom C R G) := by
350 intro x y hxy
351 apply MonoidAlgebra.ext
352 apply Finsupp.ext
353 intro g
354 have hcoeff : (x - y).coeff g = 0 := by
355 rcases exists_completedGroupAlgebraIndexInClass_separating_support
356 (R := R) (G := G) C hForm hG (x - y) g with
357 ⟨U, hsep⟩
358 have hstage_eq : completedGroupAlgebraStageMapInClass C R G U x =
359 completedGroupAlgebraStageMapInClass C R G U y := by
360 have hp := congrArg (fun z : CompletedGroupAlgebraInClass C R G =>
361 completedGroupAlgebraProjectionInClass C R G U z) hxy
362 change completedGroupAlgebraProjectionInClass C R G U
363 (toCompletedGroupAlgebraInClass C R G x) =
364 completedGroupAlgebraProjectionInClass C R G U
365 (toCompletedGroupAlgebraInClass C R G y) at hp
366 simpa [completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass] using hp
367 have hstage : completedGroupAlgebraStageMapInClass C R G U (x - y) = 0 := by
368 rw [map_sub, hstage_eq, sub_self]
369 have hstage_coeff :
370 (completedGroupAlgebraStageMapInClass C R G U (x - y)).coeff
371 (openNormalSubgroupInClassProj (C := C) (G := G) U g) = 0 := by
372 simpa only [MonoidAlgebra.coeff_zero, Finsupp.zero_apply] using congrArg
373 (fun z : CompletedGroupAlgebraStageInClass C R G U =>
374 z.coeff (openNormalSubgroupInClassProj (C := C) (G := G) U g))
375 hstage
376 rw [completedGroupAlgebraStageMapInClass_coeff_of_support_separated
377 (R := R) (G := G) C U (x - y) g hsep] at hstage_coeff
378 simpa using hstage_coeff
379 exact sub_eq_zero.mp (by simpa using hcoeff)
381omit [CompactSpace G] [TotallyDisconnectedSpace G] in
382/-- Kernel form of the \(C\)-indexed injectivity statement. -/
383theorem toCompletedGroupAlgebraInClassRingHom_ker_eq_bot
384 (C : ProCGroups.FiniteGroupClass.{v})
385 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
386 RingHom.ker (toCompletedGroupAlgebraInClassRingHom C R G) = ⊥ :=
387 (RingHom.injective_iff_ker_eq_bot (toCompletedGroupAlgebraInClassRingHom C R G)).mp
388 (injective_toCompletedGroupAlgebraInClassRingHom (R := R) (G := G) C hForm hG)
390omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
391/--
392The kernel of the map to \(\widehat{R[G]}_{C}\) is the intersection of the \(C\)-indexed
393finite-stage kernels.
394-/
395theorem toCompletedGroupAlgebraInClassRingHom_ker_eq_iInf_stageMapInClass_ker
396 (C : ProCGroups.FiniteGroupClass.{v}) :
397 RingHom.ker (toCompletedGroupAlgebraInClassRingHom C R G) =
398 ⨅ U : CompletedGroupAlgebraIndexInClass G C,
399 RingHom.ker (completedGroupAlgebraStageMapInClass C R G U) := by
400 ext x
401 constructor
402 · intro hx
403 rw [RingHom.mem_ker] at hx
404 rw [Submodule.mem_iInf]
405 intro U
406 rw [RingHom.mem_ker]
407 have hU := congrArg (fun y : CompletedGroupAlgebraInClass C R G =>
408 completedGroupAlgebraProjectionInClass C R G U y) hx
409 change completedGroupAlgebraProjectionInClass C R G U
410 (toCompletedGroupAlgebraInClass C R G x) =
411 completedGroupAlgebraProjectionInClass C R G U
412 (0 : CompletedGroupAlgebraInClass C R G) at hU
413 simpa [completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass] using hU
414 · intro hx
415 rw [RingHom.mem_ker]
416 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
417 intro U
418 change completedGroupAlgebraStageMapInClass C R G U x = 0
419 exact (Submodule.mem_iInf
420 (p := fun U : CompletedGroupAlgebraIndexInClass G C =>
421 RingHom.ker (completedGroupAlgebraStageMapInClass C R G U))).1 hx U
423omit [CompactSpace G] [TotallyDisconnectedSpace G] in
424/-- \(C\)-indexed finite-stage kernel-family form of Lemma 5.3.5(a). -/
425theorem iInf_completedGroupAlgebraStageMapInClass_ker_eq_bot
426 (C : ProCGroups.FiniteGroupClass.{v})
427 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
428 (⨅ U : CompletedGroupAlgebraIndexInClass G C,
429 RingHom.ker (completedGroupAlgebraStageMapInClass C R G U)) = ⊥ := by
430 rw [← toCompletedGroupAlgebraInClassRingHom_ker_eq_iInf_stageMapInClass_ker
431 (R := R) (G := G) C ,
432 toCompletedGroupAlgebraInClassRingHom_ker_eq_bot (R := R) (G := G) C hForm hG]
434omit [T2Space G] in
435/--
436In Lemma 5.3.5(a), book kernel-family form, the intersection of the kernels of \(R[G] \to
437(R/I)[G/U]\), over open coefficient ideals and finite group quotients, is zero.
438-/
439theorem iInf_groupAlgebraOpenFiniteQuotientKernel_eq_bot
440 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] :
441 (⨅ K : CompletedGroupAlgebraOpenQuotientIndex R G,
442 groupAlgebraOpenFiniteQuotientKernel R G K) = ⊥ := by
443 apply le_antisymm
444 · intro x hx
445 rw [Ideal.mem_bot]
446 have hxall :
447 ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
448 x ∈ groupAlgebraOpenFiniteQuotientKernel R G K := by
449 simpa using (Submodule.mem_iInf
450 (p := fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
451 groupAlgebraOpenFiniteQuotientKernel R G K)).1 hx
452 have hxlimit :
453 toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G x = 0 := by
454 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
455 intro K
456 change groupAlgebraOpenFiniteQuotientMap R G K x = 0
457 exact (mem_groupAlgebraOpenFiniteQuotientKernel_iff
458 (R := R) (G := G) (K := K) (x := x)).1 (hxall K)
459 have hcompleted :
460 toCompletedGroupAlgebraRingHom R G x = 0 := by
461 apply injective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G)
462 change completedGroupAlgebraToOpenFiniteQuotientLimit R G
463 (toCompletedGroupAlgebra R G x) =
464 completedGroupAlgebraToOpenFiniteQuotientLimit R G
465 (0 : CompletedGroupAlgebraCarrier R G)
466 calc
467 completedGroupAlgebraToOpenFiniteQuotientLimit R G
468 (toCompletedGroupAlgebra R G x) =
469 toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x :=
470 completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra
471 (R := R) (G := G) x
472 _ = 0 := hxlimit
473 _ = completedGroupAlgebraToOpenFiniteQuotientLimit R G
474 (0 : CompletedGroupAlgebraCarrier R G) := by
475 symm
476 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
477 intro K
478 exact map_zero (completedGroupAlgebraOpenFiniteQuotientProjection R G K)
479 exact (injective_toCompletedGroupAlgebraRingHom (R := R) (G := G)) (by
480 simpa using hcompleted)
481 · exact bot_le
483omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
484/--
485Continuous ring homomorphisms out of \(\widehat{R[G]}\) into another completed group algebra are
486determined by their values on the dense abstract group algebra.
487-/
488theorem completedGroupAlgebraRingHom_ext_of_comp_toCompleted
489 [T2Space R]
490 {f g : CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraCarrier R H}
491 (hf : Continuous f) (hg : Continuous g)
492 (hfg : f.comp (toCompletedGroupAlgebraRingHom R G) =
493 g.comp (toCompletedGroupAlgebraRingHom R G)) :
494 f = g := by
495 letI : T2Space (CompletedGroupAlgebraCarrier R H) :=
496 completedGroupAlgebra_t2Space (R := R) (G := H)
497 have hdense : DenseRange (toCompletedGroupAlgebraRingHom R G) :=
498 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G)
499 have hcomp : (f : CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraCarrier R H) ∘
500 (toCompletedGroupAlgebraRingHom R G) =
501 (g : CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraCarrier R H) ∘
502 (toCompletedGroupAlgebraRingHom R G) := by
503 funext x
504 exact congrFun (congrArg DFunLike.coe hfg) x
505 have hfun : (f : CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraCarrier R H) = g :=
506 DenseRange.equalizer hdense hf hg hcomp
507 exact RingHom.ext fun x => congrFun hfun x
509omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
510/-- Lemma 5.3.5(e), identity law for the completed-group-algebra functor. -/
511theorem completedGroupAlgebraMap_id
512 [T2Space R] :
513 completedGroupAlgebraMap (G := G) (H := G) R (MonoidHom.id G) continuous_id =
514 RingHom.id (CompletedGroupAlgebraCarrier R G) := by
515 apply completedGroupAlgebraRingHom_ext_of_comp_toCompleted (R := R) (G := G) (H := G)
516 · exact continuous_completedGroupAlgebraMap (R := R) (G := G) (H := G)
517 (MonoidHom.id G) continuous_id
518 · exact continuous_id
519 · rw [completedGroupAlgebraMap_comp_toCompletedGroupAlgebra,
520 finiteGroupAlgebra_mapDomainRingHom_id]
521 rfl
523omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
524/--
525Lemma 5.3.5(e), identity law for the completed-group-algebra functor, as an \(R\)-algebra
526homomorphism.
527-/
528theorem completedGroupAlgebraMapAlgHom_id
529 [T2Space R] :
530 completedGroupAlgebraMapAlgHom (G := G) (H := G) R (MonoidHom.id G) continuous_id =
531 AlgHom.id R (CompletedGroupAlgebraCarrier R G) := by
532 apply AlgHom.ext
533 intro x
534 have h := congrFun
535 (congrArg DFunLike.coe
536 (completedGroupAlgebraMap_id (R := R) (G := G)))
537 x
538 simpa using h
540end
542end CompletedGroupAlgebra