CompletedGroupAlgebra/Separation.lean
1import CompletedGroupAlgebra.AllFiniteFunctoriality.GroupLike
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Separation.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed group algebras
14The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.
15-/
16open scoped Topology
18namespace CompletedGroupAlgebra
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
24open ProCGroups.InverseSystems
25open ProCGroups.Completion
27universe u v w
29variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/-- A finite set of nontrivial elements in a profinite group can be avoided by one open normal
36 (hG : ProCGroups.IsProfiniteGroup G) (s : Finset G)
37 (hs : ∀ x ∈ s, x ≠ 1) :
38 ∃ U : CompletedGroupAlgebraIndex G,
39 ∀ x ∈ s, x ∉ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
40 classical
41 let hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
42 (isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
43 revert hs
44 refine Finset.induction_on s ?_ ?_
45 · intro _hs
46 letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
47 IsProCGroup.openNormalSubgroupInClass_nonempty hProC
48 letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
49 exact ⟨Classical.choice inferInstance, by simp only [Finset.notMem_empty, OpenSubgroup.mem_toSubgroup, IsEmpty.forall_iff, implies_true]⟩
50 · intro a s has ih hs
51 have ha : a ≠ 1 := hs a (by simp only [Finset.mem_insert, true_or])
52 rcases hProC.exists_openNormalSubgroupInClass_not_mem ha with ⟨A, hA⟩
53 have hs' : ∀ x ∈ s, x ≠ 1 := by
54 intro x hx
55 exact hs x (by simp only [Finset.mem_insert, hx, or_true])
56 rcases ih hs' with ⟨U, hU⟩
57 let Aidx : CompletedGroupAlgebraIndex G := OrderDual.toDual A
59 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) ProCGroups.FiniteGroupClass.allFinite_formation
60 Aidx U with
61 ⟨W, hAW, hUW⟩
62 refine ⟨W, ?_⟩
63 intro x hx hxW
64 rw [Finset.mem_insert] at hx
65 rcases hx with rfl | hx
66 · exact hA (hAW hxW)
67 · exact hU x hx (hUW hxW)
69omit [TopologicalSpace R] [IsTopologicalRing R]
70 H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
71/-- For a finite-support group-algebra element and a chosen basis element `g`, one finite
72quotient separates the image of `g` from all other support points. -/
74 (hG : ProCGroups.IsProfiniteGroup G) (x : MonoidAlgebra R G) (g : G) :
75 ∃ U : CompletedGroupAlgebraIndex G,
76 ∀ h ∈ x.support, h ≠ g →
77 openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h ≠
78 openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g := by
79 classical
80 let bad : Finset G := (x.support.erase g).image fun h => h⁻¹ * g
81 have hbad : ∀ y ∈ bad, y ≠ 1 := by
82 intro y hy
83 rcases Finset.mem_image.mp hy with ⟨h, hh, rfl⟩
84 intro h1
85 have hg : h = g := by
86 have hmul := congrArg (fun t : G => h * t) h1
87 have hg' : g = h := by
88 simpa [mul_assoc] using hmul
89 exact hg'.symm
90 exact (Finset.mem_erase.mp hh).1 hg
91 rcases exists_completedGroupAlgebraIndex_avoids_finset (G := G) hG bad hbad with
92 ⟨U, hU⟩
93 refine ⟨U, ?_⟩
94 intro h hh hne heq
95 have hbadmem : h⁻¹ * g ∈ bad := by
96 exact Finset.mem_image.mpr ⟨h, Finset.mem_erase.mpr ⟨hne, hh⟩, rfl⟩
97 have hmem :
98 h⁻¹ * g ∈ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
99 exact QuotientGroup.eq.1 heq
100 exact hU (h⁻¹ * g) hbadmem hmem
102omit [TopologicalSpace R] [IsTopologicalRing R]
103 H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
104/-- If a finite quotient separates `g` from the other support points of `x`, then the coefficient
105of the image of `g` in the quotient group algebra is exactly the original coefficient of `g`. -/
107 (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) (g : G)
108 (hsep : ∀ h ∈ x.support, h ≠ g →
109 openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h ≠
110 openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) :
111 completedGroupAlgebraStageMap R G U x
112 (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) =
113 x g := by
114 classical
116 change (Finsupp.mapDomain
117 (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U) x)
118 (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) =
119 x g
120 rw [Finsupp.mapDomain, Finsupp.sum_apply]
121 rw [Finsupp.sum_eq_single g]
122 · simp only [Finsupp.single_eq_same]
123 · intro h hh hne
124 exact Finsupp.single_eq_of_ne fun heq =>
125 hsep h (Finsupp.mem_support_iff.mpr hh) hne heq.symm
126 · intro _hg
127 simp only [Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]
129omit R [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
130 [IsTopologicalGroup G] H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
131/-- A finite set of nontrivial elements in a pro-`C` group can be avoided by one open normal
134 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
135 (hG : IsProCGroup C G) (s : Finset G) (hs : ∀ x ∈ s, x ≠ 1) :
136 ∃ U : CompletedGroupAlgebraIndexInClass G C,
137 ∀ x ∈ s, x ∉ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
138 classical
139 revert hs
140 refine Finset.induction_on s ?_ ?_
141 · intro _hs
142 letI : Nonempty (OpenNormalSubgroupInClass C G) :=
143 IsProCGroup.openNormalSubgroupInClass_nonempty hG
144 letI : Nonempty (CompletedGroupAlgebraIndexInClass G C) := inferInstance
145 exact ⟨Classical.choice inferInstance, by simp only [Finset.notMem_empty, OpenSubgroup.mem_toSubgroup, IsEmpty.forall_iff, implies_true]⟩
146 · intro a s has ih hs
147 have ha : a ≠ 1 := hs a (by simp only [Finset.mem_insert, true_or])
148 rcases hG.exists_openNormalSubgroupInClass_not_mem ha with ⟨A, hA⟩
149 have hs' : ∀ x ∈ s, x ≠ 1 := by
150 intro x hx
151 exact hs x (by simp only [Finset.mem_insert, hx, or_true])
152 rcases ih hs' with ⟨U, hU⟩
153 let Aidx : CompletedGroupAlgebraIndexInClass G C := OrderDual.toDual A
154 rcases directed_openNormalSubgroupInClass (C := C) (G := G) hForm Aidx U with
155 ⟨W, hAW, hUW⟩
156 refine ⟨W, ?_⟩
157 intro x hx hxW
158 rw [Finset.mem_insert] at hx
159 rcases hx with rfl | hx
160 · exact hA (hAW hxW)
161 · exact hU x hx (hUW hxW)
163omit R [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
164 [IsTopologicalGroup G] H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
165/-- For any finitely supported family on a pro-`C` group and a chosen basis point `g`, one
166`C`-quotient separates the image of `g` from all other support points. -/
168 {M : Type w} [Zero M]
169 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
170 (hG : IsProCGroup C G) (x : G →₀ M) (g : G) :
171 ∃ U : CompletedGroupAlgebraIndexInClass G C,
172 ∀ h ∈ x.support, h ≠ g →
173 openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
174 openNormalSubgroupInClassProj (C := C) (G := G) U g := by
175 classical
176 let bad : Finset G := (x.support.erase g).image fun h => h⁻¹ * g
177 have hbad : ∀ y ∈ bad, y ≠ 1 := by
178 intro y hy
179 rcases Finset.mem_image.mp hy with ⟨h, hh, rfl⟩
180 intro h1
181 have hg : h = g := by
182 have hmul := congrArg (fun t : G => h * t) h1
183 have hg' : g = h := by
184 simpa [mul_assoc] using hmul
185 exact hg'.symm
186 exact (Finset.mem_erase.mp hh).1 hg
188 (G := G) C hForm hG bad hbad with
189 ⟨U, hU⟩
190 refine ⟨U, ?_⟩
191 intro h hh hne heq
192 have hbadmem : h⁻¹ * g ∈ bad := by
193 exact Finset.mem_image.mpr ⟨h, Finset.mem_erase.mpr ⟨hne, hh⟩, rfl⟩
194 have hmem :
195 h⁻¹ * g ∈ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
196 exact QuotientGroup.eq.1 heq
197 exact hU (h⁻¹ * g) hbadmem hmem
199omit [TopologicalSpace R] [IsTopologicalRing R]
200 [IsTopologicalGroup G] H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
201/-- For a finite-support group-algebra element and a chosen basis element `g`, one `C`-quotient
202separates the image of `g` from all other support points. -/
204 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
205 (hG : IsProCGroup C G) (x : MonoidAlgebra R G) (g : G) :
206 ∃ U : CompletedGroupAlgebraIndexInClass G C,
207 ∀ h ∈ x.support, h ≠ g →
208 openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
209 openNormalSubgroupInClassProj (C := C) (G := G) U g :=
211 (G := G) C hForm hG x g
213omit [TopologicalSpace R] [IsTopologicalRing R]
214 H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in
215/-- If a `C`-quotient separates `g` from the other support points of `x`, then the coefficient of
216the image of `g` in the quotient group algebra is exactly the original coefficient of `g`. -/
218 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
219 (x : MonoidAlgebra R G) (g : G)
220 (hsep : ∀ h ∈ x.support, h ≠ g →
221 openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
222 openNormalSubgroupInClassProj (C := C) (G := G) U g) :
223 completedGroupAlgebraStageMapInClass C R G U x
224 (openNormalSubgroupInClassProj (C := C) (G := G) U g) =
225 x g := by
226 classical
227 rw [completedGroupAlgebraStageMapInClass]
228 change (Finsupp.mapDomain
229 (openNormalSubgroupInClassProj (C := C) (G := G) U) x)
230 (openNormalSubgroupInClassProj (C := C) (G := G) U g) =
231 x g
232 rw [Finsupp.mapDomain, Finsupp.sum_apply]
233 rw [Finsupp.sum_eq_single g]
234 · simp only [Finsupp.single_eq_same]
235 · intro h hh hne
236 exact Finsupp.single_eq_of_ne fun heq =>
237 hsep h (Finsupp.mem_support_iff.mpr hh) hne heq.symm
238 · intro _hg
239 simp only [Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]
241/-- Lemma 5.3.5(a), fixed-coefficient form: the canonical map from the abstract group algebra
242to the completed group algebra is injective for profinite `G`. Equivalently, the kernels of the
245 (hG : ProCGroups.IsProfiniteGroup G) :
246 Function.Injective (toCompletedGroupAlgebraRingHom R G) := by
247 intro x y hxy
248 apply Finsupp.ext
249 intro g
250 have hcoeff : (x - y) g = 0 := by
251 rcases exists_completedGroupAlgebraIndex_separating_support (R := R) (G := G)
252 hG (x - y) g with
253 ⟨U, hsep⟩
254 have hstage_eq : completedGroupAlgebraStageMap R G U x =
255 completedGroupAlgebraStageMap R G U y := by
256 have hp := congrArg (fun z : Carrier R G =>
257 completedGroupAlgebraProjection R G U z) hxy
258 change completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
259 completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G y) at hp
260 simpa [completedGroupAlgebraProjection_toCompletedGroupAlgebra] using hp
261 have hstage : completedGroupAlgebraStageMap R G U (x - y) = 0 := by
262 rw [map_sub, hstage_eq, sub_self]
263 have hstage_coeff :
264 completedGroupAlgebraStageMap R G U (x - y)
265 (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = 0 := by
266 simpa using congrArg
267 (fun z : CompletedGroupAlgebraStage R G U =>
268 z (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g))
269 hstage
271 (R := R) (G := G) U (x - y) g hsep] at hstage_coeff
272 simpa using hstage_coeff
273 exact sub_eq_zero.mp hcoeff
275/-- Kernel form of Lemma 5.3.5(a). -/
277 (hG : ProCGroups.IsProfiniteGroup G) :
278 RingHom.ker (toCompletedGroupAlgebraRingHom R G) = ⊥ :=
279 (RingHom.injective_iff_ker_eq_bot (toCompletedGroupAlgebraRingHom R G)).mp
280 (injective_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG)
282/-- The kernel of the map to `[[R G]]` is the intersection of the finite-stage kernels. -/
284 RingHom.ker (toCompletedGroupAlgebraRingHom R G) =
285 ⨅ U : CompletedGroupAlgebraIndex G, RingHom.ker (completedGroupAlgebraStageMap R G U) := by
286 ext x
287 constructor
288 · intro hx
289 rw [RingHom.mem_ker] at hx
290 rw [Submodule.mem_iInf]
291 intro U
292 rw [RingHom.mem_ker]
293 have hU := congrArg (fun y : Carrier R G =>
294 completedGroupAlgebraProjection R G U y) hx
295 change completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
296 completedGroupAlgebraProjection R G U (0 : Carrier R G) at hU
297 simpa [completedGroupAlgebraProjection_toCompletedGroupAlgebra] using hU
298 · intro hx
299 rw [RingHom.mem_ker]
300 apply (completedGroupAlgebraSystem R G).ext
301 intro U
302 change completedGroupAlgebraStageMap R G U x = 0
303 exact (Submodule.mem_iInf
304 (p := fun U : CompletedGroupAlgebraIndex G =>
305 RingHom.ker (completedGroupAlgebraStageMap R G U))).1 hx U
307/-- Fixed-coefficient finite-stage kernel-family form of Lemma 5.3.5(a). -/
309 (hG : ProCGroups.IsProfiniteGroup G) :
310 (⨅ U : CompletedGroupAlgebraIndex G,
311 RingHom.ker (completedGroupAlgebraStageMap R G U)) = ⊥ := by
312 rw [← toCompletedGroupAlgebraRingHom_ker_eq_iInf_stageMap_ker (R := R) (G := G),
313 toCompletedGroupAlgebraRingHom_ker_eq_bot (R := R) (G := G) hG]
315/-- `C`-indexed form of Lemma 5.3.5(a): for a pro-`C` group, the canonical map from
316the abstract group algebra to `[[R G]]_C` is injective. -/
318 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
319 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
320 Function.Injective (toCompletedGroupAlgebraInClassRingHom C hC R G) := by
321 intro x y hxy
322 apply injective_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG.1
323 have h := congrArg
324 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG) hxy
325 simpa [RingHom.congr_fun
327 (R := R) (G := G) C hC hForm hG)] using h
329/-- Kernel form of the `C`-indexed injectivity statement. -/
331 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
332 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
333 RingHom.ker (toCompletedGroupAlgebraInClassRingHom C hC R G) = ⊥ :=
334 (RingHom.injective_iff_ker_eq_bot (toCompletedGroupAlgebraInClassRingHom C hC R G)).mp
335 (injective_toCompletedGroupAlgebraInClassRingHom (R := R) (G := G) C hC hForm hG)
337/-- The kernel of the map to `[[R G]]_C` is the intersection of the `C`-indexed finite-stage
338kernels. -/
340 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
341 RingHom.ker (toCompletedGroupAlgebraInClassRingHom C hC R G) =
342 ⨅ U : CompletedGroupAlgebraIndexInClass G C,
343 RingHom.ker (completedGroupAlgebraStageMapInClass C R G U) := by
344 ext x
345 constructor
346 · intro hx
347 rw [RingHom.mem_ker] at hx
348 rw [Submodule.mem_iInf]
349 intro U
350 rw [RingHom.mem_ker]
351 have hU := congrArg (fun y : CompletedGroupAlgebraInClass C hC R G =>
352 completedGroupAlgebraProjectionInClass C hC R G U y) hx
353 change completedGroupAlgebraProjectionInClass C hC R G U
354 (toCompletedGroupAlgebraInClass C hC R G x) =
355 completedGroupAlgebraProjectionInClass C hC R G U
356 (0 : CompletedGroupAlgebraInClass C hC R G) at hU
357 simpa [completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass] using hU
358 · intro hx
359 rw [RingHom.mem_ker]
360 apply (completedGroupAlgebraSystemInClass C hC R G).ext
361 intro U
362 change completedGroupAlgebraStageMapInClass C R G U x = 0
363 exact (Submodule.mem_iInf
364 (p := fun U : CompletedGroupAlgebraIndexInClass G C =>
365 RingHom.ker (completedGroupAlgebraStageMapInClass C R G U))).1 hx U
367/-- `C`-indexed finite-stage kernel-family form of Lemma 5.3.5(a). -/
369 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
370 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
371 (⨅ U : CompletedGroupAlgebraIndexInClass G C,
372 RingHom.ker (completedGroupAlgebraStageMapInClass C R G U)) = ⊥ := by
374 (R := R) (G := G) C hC,
375 toCompletedGroupAlgebraInClassRingHom_ker_eq_bot (R := R) (G := G) C hC hForm hG]
377/-- Lemma 5.3.5(a), book kernel-family form: the intersection of the kernels of
380 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
381 (⨅ K : CompletedGroupAlgebraOpenQuotientIndex R G,
382 groupAlgebraOpenFiniteQuotientKernel R G K) = ⊥ := by
383 apply le_antisymm
384 · intro x hx
385 rw [Ideal.mem_bot]
386 have hxall :
387 ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
388 x ∈ groupAlgebraOpenFiniteQuotientKernel R G K := by
389 simpa using (Submodule.mem_iInf
390 (p := fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
391 groupAlgebraOpenFiniteQuotientKernel R G K)).1 hx
392 have hxlimit :
393 toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G x = 0 := by
394 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
395 intro K
396 change groupAlgebraOpenFiniteQuotientMap R G K x = 0
397 exact (mem_groupAlgebraOpenFiniteQuotientKernel_iff R G K x).1 (hxall K)
398 have hcompleted :
399 toCompletedGroupAlgebraRingHom R G x = 0 := by
400 apply injective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G) hR
402 (toCompletedGroupAlgebra R G x) =
404 (0 : Carrier R G)
405 simpa [toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom] using hxlimit
406 exact (injective_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG) (by
407 simpa using hcompleted)
408 · exact bot_le
410/-- Lemma 5.3.5(b/c), concrete completion form: with the book kernel-neighborhood topology on
411`R[G]`, the canonical map into `[[RG]]` is an injective dense continuous map into a profinite ring,
414 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
415 letI : TopologicalSpace (MonoidAlgebra R G) :=
417 IsProfiniteRing (Carrier R G) ∧
418 Function.Injective (toCompletedGroupAlgebraRingHom R G) ∧
419 DenseRange (toCompletedGroupAlgebraRingHom R G) ∧
420 Continuous (toCompletedGroupAlgebraRingHom R G) ∧
422 TopologicalSpace.induced (toCompletedGroupAlgebra R G) inferInstance := by
423 have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
424 (isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
425 letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
426 IsProCGroup.openNormalSubgroupInClass_nonempty hProC
427 letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
428 letI : Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G) := inferInstance
429 refine ⟨completedGroupAlgebra_isProfiniteRing (R := R) (G := G) hR,
430 injective_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG,
431 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG,
432 continuous_toCompletedGroupAlgebraRingHom_kernelTopology (R := R) (G := G) hR, ?_⟩
433 have hτ :=
435 (R := R) (G := G) hR
436 simpa [completedGroupAlgebraNaturalTopology] using hτ.symm
438/-- Continuous ring homomorphisms out of `[[R G]]` into another completed group algebra are
439determined by their values on the dense abstract group algebra. -/
441 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
442 {f g : Carrier R G →+* Carrier R H}
443 (hf : Continuous f) (hg : Continuous g)
444 (hfg : f.comp (toCompletedGroupAlgebraRingHom R G) =
445 g.comp (toCompletedGroupAlgebraRingHom R G)) :
446 f = g := by
447 letI : T2Space (Carrier R H) :=
448 completedGroupAlgebra_t2Space (R := R) (G := H) hR
449 have hdense : DenseRange (toCompletedGroupAlgebraRingHom R G) :=
450 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG
451 have hcomp : (f : Carrier R G → Carrier R H) ∘
452 (toCompletedGroupAlgebraRingHom R G) =
453 (g : Carrier R G → Carrier R H) ∘
454 (toCompletedGroupAlgebraRingHom R G) := by
455 funext x
456 exact congrFun (congrArg DFunLike.coe hfg) x
457 have hfun : (f : Carrier R G → Carrier R H) = g :=
458 DenseRange.equalizer hdense hf hg hcomp
459 exact RingHom.ext fun x => congrFun hfun x
461/-- Lemma 5.3.5(e), identity law for the completed-group-algebra functor. -/
462theorem completedGroupAlgebraMap_id
463 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
464 completedGroupAlgebraMap (G := G) (H := G) R hG (MonoidHom.id G) continuous_id =
465 RingHom.id (Carrier R G) := by
466 apply completedGroupAlgebraRingHom_ext_of_comp_toCompleted (R := R) (G := G) (H := G)
467 hR hG
468 · exact continuous_completedGroupAlgebraMap (R := R) (G := G) (H := G)
469 hG (MonoidHom.id G) continuous_id
470 · exact continuous_id
473 rfl
475/-- Lemma 5.3.5(e), identity law for the completed-group-algebra functor, as an `R`-algebra
476homomorphism. -/
478 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
479 completedGroupAlgebraMapAlgHom (G := G) (H := G) R hG (MonoidHom.id G) continuous_id =
480 AlgHom.id R (Carrier R G) := by
481 apply AlgHom.ext
482 intro x
483 have h := congrFun
484 (congrArg DFunLike.coe
485 (completedGroupAlgebraMap_id (R := R) (G := G) hR hG))
486 x
487 simpa using h
489end