Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison
ProCGroups/CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteComparison/Source

Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison

1import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap
2import Mathlib.Algebra.Ring.TransferInstance
3import Mathlib.Topology.Homeomorph.TransferInstance
5/-!
6# Completed Group Algebra / Open Finite Quotient Topology / Open Finite Comparison
8This module compares the named fixed-coefficient completion with the named two-parameter
9open-finite quotient completion and studies the induced topology, injectivity, density, and
10coefficient-quotient kernels.
11-/
13open scoped Topology
15namespace CompletedGroupAlgebra
17noncomputable section
19open ProCGroups
20open ProCGroups.ProC
21open ProCGroups.InverseSystems
22open ProCGroups.Completion
24universe u v w
26variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
27variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30/--
31The canonical map from the fixed-coefficient completed group algebra \(\widehat{R[G]}\) to the
32two-parameter limit \(\varprojlim_{I,U} (R/I)[G/U]\).
33-/
34def completedGroupAlgebraToOpenFiniteQuotientLimit
35 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
36 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
37 (x : CompletedGroupAlgebraCarrier R G) :
38 CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
39 (completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv
40 (R := R) (G := G)).symm
41 ((completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimitLift
42 (fun K => completedGroupAlgebraOpenFiniteQuotientProjection R G K)
43 (by
44 intro K L hKL
45 funext x
46 exact congrFun
47 (congrArg DFunLike.coe
48 (completedGroupAlgebraOpenFiniteQuotientTransition_comp_projection
49 R G hKL))
50 x) x)
52/--
53The open-finite-limit projection after the comparison from the completed group algebra is the
54original finite-stage projection.
55-/
56@[simp]
57theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_fromCompleted
58 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
59 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
60 (K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : CompletedGroupAlgebraCarrier R G) :
61 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
62 (completedGroupAlgebraToOpenFiniteQuotientLimit R G x) =
63 completedGroupAlgebraOpenFiniteQuotientProjection R G K x :=
64 rfl
66/--
67The comparison from the completed group algebra to the open-finite quotient limit agrees with
68the canonical dense map on abstract group-algebra elements.
69-/
70@[simp]
71theorem completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra
72 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
73 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
74 (x : MonoidAlgebra R G) :
75 completedGroupAlgebraToOpenFiniteQuotientLimit R G (toCompletedGroupAlgebra R G x) =
76 toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x := by
77 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
78 intro K
79 rfl
81/--
82The canonical map \(\widehat{R[G]} \to \varprojlim_{I,U} (R/I)[G/U]\) is bundled as a ring
83homomorphism.
84-/
85def completedGroupAlgebraToOpenFiniteQuotientLimitRingHom
86 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
87 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
88 CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G where
89 toFun := completedGroupAlgebraToOpenFiniteQuotientLimit R G
90 map_zero' := by
91 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
92 intro K
93 exact map_zero (completedGroupAlgebraOpenFiniteQuotientProjection R G K)
94 map_one' := by
95 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
96 intro K
97 exact map_one (completedGroupAlgebraOpenFiniteQuotientProjection R G K)
98 map_add' x y := by
99 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
100 intro K
101 exact map_add (completedGroupAlgebraOpenFiniteQuotientProjection R G K) x y
102 map_mul' x y := by
103 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
104 intro K
105 exact map_mul (completedGroupAlgebraOpenFiniteQuotientProjection R G K) x y
107/-- Projection from the open-finite quotient limit, composed with the comparison from the
108completion, recovers the corresponding completed projection. -/
109@[simp]
110theorem openFiniteLimitProjection_comp_fromCompleted
111 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
112 (completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K).comp
113 (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G) =
114 completedGroupAlgebraOpenFiniteQuotientProjection R G K := by
115 apply RingHom.ext
116 intro x
117 rfl
119/--
120Composing the comparison map with the dense map from the abstract group algebra recovers the
121canonical completed group-algebra map.
122-/
123@[simp]
124theorem completedGAToOpenFiniteQuotientLimitRingHom_comp_toCompletedGA :
125 (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G).comp
126 (toCompletedGroupAlgebraRingHom R G) =
127 toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G := by
128 apply RingHom.ext
129 intro x
130 exact completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra (R := R) (G := G) x
132/-- The comparison map \(\widehat{R[G]} \to \varprojlim_{I,U} (R/I)[G/U]\) is continuous. -/
133theorem continuous_completedGroupAlgebraToOpenFiniteQuotientLimit :
134 Continuous (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
135 let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
136 letI : ∀ K, TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
137 fun K => (completedGroupAlgebraOpenFiniteQuotientSystem R G).topologicalSpace K
138 let π : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
139 CompletedGroupAlgebraCarrier R G →
140 CompletedGroupAlgebraOpenQuotientStage R G K :=
141 fun K => completedGroupAlgebraOpenFiniteQuotientProjection R G K
142 have hπ : ∀ K, Continuous (π K) := by
143 intro K
144 exact continuous_completedGroupAlgebraOpenFiniteQuotientProjection (R := R) (G := G) K
145 have hcompat : S.CompatibleMaps π := by
146 intro K L hKL
147 funext x
148 exact congrFun
149 (congrArg DFunLike.coe
150 (completedGroupAlgebraOpenFiniteQuotientTransition_comp_projection
151 R G hKL))
152 x
153 change Continuous (S.inverseLimitLift π hcompat)
154 exact S.continuous_inverseLimitLift π hπ hcompat
156/--
157The image of the map from the completed group algebra to the open-finite quotient limit is dense
158in the target completed group-algebra object.
159-/
160theorem denseRange_completedGroupAlgebraToOpenFiniteQuotientLimit
161 [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
162 DenseRange (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
163 have hdense :
164 DenseRange
165 ((completedGroupAlgebraToOpenFiniteQuotientLimit R G) ∘
166 (toCompletedGroupAlgebra R G)) := by
167 have hcomp :
168 (completedGroupAlgebraToOpenFiniteQuotientLimit R G) ∘
169 (toCompletedGroupAlgebra R G) =
170 toCompletedGroupAlgebraOpenFiniteQuotientLimit R G := by
171 funext x
172 exact completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra
173 (R := R) (G := G) x
174 rw [hcomp]
175 exact denseRange_toCompletedGroupAlgebraOpenFiniteQuotientLimit
176 (R := R) (G := G)
177 exact DenseRange.of_comp hdense
179/--
180The comparison map to the two-parameter kernel-neighborhood limit is injective when the
181coefficient ring is profinite. This is the completed-stage form of the kernel-intersection claim
182in Lemma 5.3.5(a).
183-/
184theorem injective_completedGroupAlgebraToOpenFiniteQuotientLimit
185 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] :
186 Function.Injective (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
187 intro x y hxy
188 apply completedGroupAlgebra_ext (R := R) (G := G)
189 intro U
190 apply MonoidAlgebra.ext
191 apply Finsupp.ext
192 intro q
193 have hzero : (completedGroupAlgebraProjection R G U x -
194 completedGroupAlgebraProjection R G U y).coeff q = 0 := by
195 apply profiniteRing_eq_zero_of_forall_openIdeal_quotient_eq_zero (R := R)
196 intro Iopen
197 let K : CompletedGroupAlgebraOpenQuotientIndex R G := (OrderDual.toDual Iopen, U)
198 have hcoord := congrArg
199 (fun z : CompletedGroupAlgebraOpenFiniteQuotientLimit R G =>
200 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K z) hxy
201 change completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 U
202 (completedGroupAlgebraProjection R G U x) =
203 completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 U
204 (completedGroupAlgebraProjection R G U y) at hcoord
205 have hdiff : completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 U
206 (completedGroupAlgebraProjection R G U x -
207 completedGroupAlgebraProjection R G U y) = 0 := by
208 rw [map_sub, hcoord, sub_self]
209 have hq := congrArg
210 (fun z : CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 U => z.coeff q) hdiff
211 simpa [completedGroupAlgebraStageCoeffQuotientMap,
212 MonoidAlgebra.coeff_mapRingHom] using hq
213 have hsub : (completedGroupAlgebraProjection R G U x).coeff q -
214 (completedGroupAlgebraProjection R G U y).coeff q = 0 := by
215 exact hzero
216 exact sub_eq_zero.mp hsub
218/--
219For profinite coefficients, the comparison map to the Hausdorff two-parameter
220kernel-neighborhood limit has compact closed dense image and is surjective.
221-/
222theorem surjective_completedGroupAlgebraToOpenFiniteQuotientLimit
223 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
224 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
225 Function.Surjective (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
226 letI : CompactSpace (CompletedGroupAlgebraCarrier R G) :=
227 completedGroupAlgebra_compactSpace (R := R) (G := G)
228 letI : T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
229 completedGroupAlgebraOpenFiniteQuotientLimit_t2Space (R := R) (G := G)
230 have hclosed : IsClosed (Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G)) := by
231 exact (isCompact_range
232 (continuous_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G))).isClosed
233 have hdense :
234 closure (Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G)) = Set.univ :=
235 (denseRange_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G)).closure_range
236 have hrange : Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G) = Set.univ := by
237 rwa [hclosed.closure_eq] at hdense
238 intro y
239 have hy : y ∈ Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
240 rw [hrange]
241 exact Set.mem_univ y
242 simpa using hy
244/--
245The comparison map \(\widehat{R[G]} \to \varprojlim_{I,U} (R/I)[G/U]\) is a bijection under the
246profinite coefficient hypothesis.
247-/
248theorem bijective_completedGroupAlgebraToOpenFiniteQuotientLimit
249 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
250 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
251 Function.Bijective (completedGroupAlgebraToOpenFiniteQuotientLimit R G) :=
252 ⟨injective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G),
253 surjective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G)⟩
255/--
256Ribes--Zalesskii Section \(5.3\) comparison: the fixed-coefficient inverse-limit model
257\(\widehat{R[G]}\) is ring-isomorphic to the two-parameter kernel-neighborhood limit
258\(\varprojlim_{I,U} (R/I)[G/U]\) for profinite coefficient rings.
259-/
260def completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv
261 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
262 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
263 CompletedGroupAlgebraCarrier R G ≃+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
264 RingEquiv.ofBijective (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G)
265 (bijective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G))
267/--
268The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison
269map.
270-/
271@[simp]
272theorem completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv_apply
273 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
274 (CompletedGroupAlgebraOpenQuotientIndex R G)]
275 (x : CompletedGroupAlgebraCarrier R G) :
276 completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv (R := R) (G := G) x =
277 completedGroupAlgebraToOpenFiniteQuotientLimit R G x :=
278 rfl
280/--
281The fixed-coefficient completed group algebra is homeomorphic to the two-parameter open finite
282quotient inverse limit.
283-/
284def completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph
285 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
286 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
287 CompletedGroupAlgebraCarrier R G ≃ₜ CompletedGroupAlgebraOpenFiniteQuotientLimit R G := by
288 letI : CompactSpace (CompletedGroupAlgebraCarrier R G) :=
289 completedGroupAlgebra_compactSpace (R := R) (G := G)
290 letI : T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
291 completedGroupAlgebraOpenFiniteQuotientLimit_t2Space (R := R) (G := G)
292 let e : CompletedGroupAlgebraCarrier R G ≃ CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
293 (completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv (R := R) (G := G)).toEquiv
294 exact Continuous.homeoOfEquivCompactToT2 (f := e) (by
295 change Continuous (completedGroupAlgebraToOpenFiniteQuotientLimit R G)
296 exact continuous_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G))
298/--
299In Lemma 5.3.5(c), fixed-coefficient inverse-limit form, the abstract group algebra maps dense
300into the completed group algebra.
301-/
302theorem denseRange_toCompletedGroupAlgebra :
303 DenseRange (toCompletedGroupAlgebra R G) := by
304 let S := completedGroupAlgebraSystem R G
305 letI : TopologicalSpace (MonoidAlgebra R G) := ⊥
306 letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
307 have hdir : Directed (α := CompletedGroupAlgebraIndex G) (· ≤ ·) fun U => U :=
308 directed_openNormalSubgroupInClass
311 have hdense :
312 DenseRange
313 (S.inverseLimitLift (fun U : CompletedGroupAlgebraIndex G =>
314 completedGroupAlgebraStageMap R G U)
315 (completedGroupAlgebraStageMap_compatibleMaps (R := R) (G := G))) :=
316 S.denseRange_lift
317 (fun U : CompletedGroupAlgebraIndex G => completedGroupAlgebraStageMap R G U)
318 (completedGroupAlgebraStageMap_compatibleMaps (R := R) (G := G))
319 (fun U => completedGroupAlgebraStageMap_surjective (R := R) (G := G) U)
320 hdir
321 change DenseRange
322 (S.inverseLimitLift
323 (fun U : CompletedGroupAlgebraIndex G => completedGroupAlgebraStageMap R G U)
324 (completedGroupAlgebraStageMap_compatibleMaps (R := R) (G := G)))
325 exact hdense
327/-- The image of the canonical ring homomorphism into the completed group algebra is dense. -/
328theorem denseRange_toCompletedGroupAlgebraRingHom :
329 DenseRange (toCompletedGroupAlgebraRingHom R G) := by
330 simpa [toCompletedGroupAlgebraRingHom] using
331 denseRange_toCompletedGroupAlgebra (R := R) (G := G)
333/--
334The completion topology on the abstract group algebra, induced by the canonical map into
335\(\widehat{R[G]}\); below it is identified with the kernel-neighborhood topology generated by
336the maps \(R[G] \to (R/I)[G/U]\).
337-/
338@[reducible]
339def completedGroupAlgebraNaturalTopology (R : Type u) (G : Type v) [CommRing R]
340 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
341 [IsTopologicalGroup G] :
342 TopologicalSpace (MonoidAlgebra R G) :=
343 TopologicalSpace.induced (toCompletedGroupAlgebra R G) inferInstance
345/-- A genuine copy of the abstract group algebra reserved for the topology induced by the
346canonical map into `[[R G]]`.
348This is deliberately a structure, not a reducible type synonym: the natural and
349kernel-neighborhood topologies therefore cannot compete as instances on the same type. -/
350@[ext]
351structure CompletedGroupAlgebraNaturalSource (R : Type u) (G : Type v) [CommRing R]
352 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
353 [IsTopologicalGroup G] where
354 /-- The group-algebra element carried by the natural-topology wrapper. -/
355 toMonoidAlgebra : MonoidAlgebra R G
357/-- Forget the natural-topology wrapper. -/
358def completedGroupAlgebraNaturalSourceEquiv :
359 CompletedGroupAlgebraNaturalSource R G ≃ MonoidAlgebra R G where
360 toFun := CompletedGroupAlgebraNaturalSource.toMonoidAlgebra
361 invFun := fun x => CompletedGroupAlgebraNaturalSource.mk x
362 left_inv x := by cases x; rfl
363 right_inv _ := rfl
365/-- Transport the group-algebra ring structure to its natural-topology wrapper. -/
366instance instRingCompletedGroupAlgebraNaturalSource :
367 Ring (CompletedGroupAlgebraNaturalSource R G) :=
368 (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).ring
370/-- Algebraic form of the forgetful equivalence from the natural-topology source. -/
371def completedGroupAlgebraNaturalSourceRingEquiv :
372 CompletedGroupAlgebraNaturalSource R G ≃+* MonoidAlgebra R G :=
373 (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).ringEquiv
375/-- Insert a raw group-algebra element into the natural-topology source. Keeping this as a
376bundled ring homomorphism avoids making downstream APIs unpack the topology wrapper. -/
377def completedGroupAlgebraNaturalSourceOf :
378 MonoidAlgebra R G →+* CompletedGroupAlgebraNaturalSource R G :=
379 (completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G)).symm.toRingHom
381/-- Forgetting the natural-topology wrapper after inserting a group-algebra element returns that
382element. -/
383@[simp]
384theorem completedGroupAlgebraNaturalSourceOf_toMonoidAlgebra (x : MonoidAlgebra R G) :
385 (completedGroupAlgebraNaturalSourceOf (R := R) (G := G) x).toMonoidAlgebra = x :=
386 by
387 change (completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G))
388 ((completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G)).symm x) = x
389 exact (completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G)).apply_symm_apply x
391/-- The coefficient-ring embedding into the natural-topology source. -/
392def completedGroupAlgebraNaturalSourceCoefficientRingHom :
393 R →+* CompletedGroupAlgebraNaturalSource R G :=
394 (completedGroupAlgebraNaturalSourceOf (R := R) (G := G)).comp
395 (MonoidAlgebra.singleOneRingHom (R := R) (M := G))
397/-- The group-like embedding into the natural-topology source. -/
398def completedGroupAlgebraNaturalSourceGroupMonoidHom :
399 G →* CompletedGroupAlgebraNaturalSource R G :=
400 (completedGroupAlgebraNaturalSourceOf (R := R) (G := G)).toMonoidHom.comp
401 (MonoidAlgebra.of R G)
403/-- The same group-like map with its invertibility recorded in the codomain. -/
404def completedGroupAlgebraNaturalSourceGroupUnitsHom :
405 G →* (CompletedGroupAlgebraNaturalSource R G)ˣ :=
406 (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G)).toHomUnits
408/-- Forgetting invertibility from the group-like units map gives the group-like monoid map. -/
409@[simp]
410theorem completedGroupAlgebraNaturalSourceGroupUnitsHom_coe (g : G) :
411 ((completedGroupAlgebraNaturalSourceGroupUnitsHom (R := R) (G := G) g :
412 (CompletedGroupAlgebraNaturalSource R G)ˣ) :
413 CompletedGroupAlgebraNaturalSource R G) =
414 completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g :=
415 rfl
417/-- The wrapped coefficient embedding forgets to the group algebra's scalar at the identity. -/
418@[simp]
419theorem completedGroupAlgebraNaturalSourceCoefficientRingHom_toMonoidAlgebra (r : R) :
420 (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r).toMonoidAlgebra =
421 MonoidAlgebra.single 1 r := by
422 simp [completedGroupAlgebraNaturalSourceCoefficientRingHom,
423 MonoidAlgebra.singleOneRingHom]
425/-- The wrapped group-like embedding forgets to the usual group-algebra basis element. -/
426@[simp]
427theorem completedGroupAlgebraNaturalSourceGroupMonoidHom_toMonoidAlgebra (g : G) :
428 (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g).toMonoidAlgebra =
429 MonoidAlgebra.of R G g := by
430 simp [completedGroupAlgebraNaturalSourceGroupMonoidHom]
432/-- Equip the natural-source wrapper with the topology induced by the completed group
433algebra. -/
434instance instTopologicalSpaceCompletedGroupAlgebraNaturalSource :
435 TopologicalSpace (CompletedGroupAlgebraNaturalSource R G) := by
436 letI : TopologicalSpace (MonoidAlgebra R G) :=
437 completedGroupAlgebraNaturalTopology R G
438 exact (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).topologicalSpace
440/-- The forgetful equivalence is a homeomorphism to the raw group algebra carrying the natural
441topology. -/
442def completedGroupAlgebraNaturalSourceHomeomorph :
443 letI : TopologicalSpace (MonoidAlgebra R G) :=
444 completedGroupAlgebraNaturalTopology R G
445 CompletedGroupAlgebraNaturalSource R G ≃ₜ MonoidAlgebra R G := by
446 letI : TopologicalSpace (MonoidAlgebra R G) :=
447 completedGroupAlgebraNaturalTopology R G
448 exact (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).homeomorph
450/-- A genuine copy of the abstract group algebra reserved for the open-ideal/finite-group
451kernel-neighborhood topology. -/
452@[ext]
453structure CompletedGroupAlgebraKernelSource (R : Type u) (G : Type v) [CommRing R]
454 [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
455 /-- The group-algebra element carried by the kernel-neighborhood-topology wrapper. -/
456 toMonoidAlgebra : MonoidAlgebra R G
458/-- Forget the kernel-neighborhood-topology wrapper. -/
459def completedGroupAlgebraKernelSourceEquiv :
460 CompletedGroupAlgebraKernelSource R G ≃ MonoidAlgebra R G where
461 toFun := CompletedGroupAlgebraKernelSource.toMonoidAlgebra
462 invFun := fun x => CompletedGroupAlgebraKernelSource.mk x
463 left_inv x := by cases x; rfl
464 right_inv _ := rfl
466/-- Transport the group-algebra ring structure to its kernel-neighborhood wrapper. -/
467instance instRingCompletedGroupAlgebraKernelSource :
468 Ring (CompletedGroupAlgebraKernelSource R G) :=
469 (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).ring
471/-- Algebraic form of the forgetful equivalence from the kernel-neighborhood source. -/
472def completedGroupAlgebraKernelSourceRingEquiv :
473 CompletedGroupAlgebraKernelSource R G ≃+* MonoidAlgebra R G :=
474 (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).ringEquiv
476/-- Equip the kernel-source wrapper with the open-finite-quotient kernel topology. -/
477instance instTopologicalSpaceCompletedGroupAlgebraKernelSource :
478 TopologicalSpace (CompletedGroupAlgebraKernelSource R G) := by
479 letI : TopologicalSpace (MonoidAlgebra R G) :=
480 groupAlgebraOpenFiniteQuotientKernelTopology R G
481 exact (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).topologicalSpace
483/-- The forgetful equivalence is a homeomorphism to the raw group algebra carrying the
484kernel-neighborhood topology. -/
485def completedGroupAlgebraKernelSourceHomeomorph :
486 letI : TopologicalSpace (MonoidAlgebra R G) :=
487 groupAlgebraOpenFiniteQuotientKernelTopology R G
488 CompletedGroupAlgebraKernelSource R G ≃ₜ MonoidAlgebra R G := by
489 letI : TopologicalSpace (MonoidAlgebra R G) :=
490 groupAlgebraOpenFiniteQuotientKernelTopology R G
491 exact (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).homeomorph
493/-- Canonical map from the natural-topology source wrapper. -/
494def toCompletedGroupAlgebraNaturalSourceRingHom :
495 CompletedGroupAlgebraNaturalSource R G →+* CompletedGroupAlgebraCarrier R G :=
496 (toCompletedGroupAlgebraRingHom R G).comp
497 (completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G)).toRingHom
499/-- On coefficients, the wrapped canonical map is the completed algebra's scalar map. -/
500@[simp]
501theorem toCompletedGroupAlgebraNaturalSourceRingHom_coefficient (r : R) :
502 toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)
503 (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r) =
504 algebraMap R (CompletedGroupAlgebraCarrier R G) r := by
505 change toCompletedGroupAlgebra R G
506 (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r).toMonoidAlgebra =
507 algebraMap R (CompletedGroupAlgebraCarrier R G) r
508 rw [completedGroupAlgebraNaturalSourceCoefficientRingHom_toMonoidAlgebra]
509 apply completedGroupAlgebra_ext (R := R) (G := G)
510 intro U
511 change completedGroupAlgebraStageMap R G U (MonoidAlgebra.single 1 r) =
512 algebraMap R (CompletedGroupAlgebraStage R G U) r
513 simpa only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
514 RingHom.coe_id, Function.comp_apply, id_eq] using
515 completedGroupAlgebraStageMap_algebraMap (R := R) (G := G) U r
517/-- On group-like elements, the wrapped canonical map is the usual completed group element. -/
518@[simp]
519theorem toCompletedGroupAlgebraNaturalSourceRingHom_group (g : G) :
520 toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)
521 (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g) =
522 toCompletedGroupAlgebra R G (MonoidAlgebra.of R G g) := by
523 change toCompletedGroupAlgebra R G
524 (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g).toMonoidAlgebra =
525 toCompletedGroupAlgebra R G (MonoidAlgebra.of R G g)
526 rw [completedGroupAlgebraNaturalSourceGroupMonoidHom_toMonoidAlgebra]
528/--
529The dense map from the abstract group algebra to the completed group algebra is continuous for
530the natural finite-quotient topology.
531-/
532theorem continuous_toCompletedGroupAlgebraRingHom_naturalTopology :
533 letI : TopologicalSpace (MonoidAlgebra R G) :=
534 completedGroupAlgebraNaturalTopology R G
535 Continuous (toCompletedGroupAlgebraRingHom R G) := by
536 letI : TopologicalSpace (MonoidAlgebra R G) :=
537 completedGroupAlgebraNaturalTopology R G
538 change Continuous (toCompletedGroupAlgebra R G)
539 exact (continuous_induced_dom : Continuous (toCompletedGroupAlgebra R G))
541/-- The natural-source wrapper's canonical map is continuous by construction. -/
542theorem continuous_toCompletedGroupAlgebraNaturalSourceRingHom :
543 Continuous (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)) := by
544 letI : TopologicalSpace (MonoidAlgebra R G) :=
545 completedGroupAlgebraNaturalTopology R G
546 exact
547 (continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G)).comp
548 (completedGroupAlgebraNaturalSourceHomeomorph (R := R) (G := G)).continuous
550/-- The natural-source wrapper has the same dense image as the raw algebraic group ring. -/
551theorem denseRange_toCompletedGroupAlgebraNaturalSourceRingHom
552 : DenseRange (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)) := by
553 letI : TopologicalSpace (MonoidAlgebra R G) :=
554 completedGroupAlgebraNaturalTopology R G
555 simpa [toCompletedGroupAlgebraNaturalSourceRingHom, Function.comp_def] using
556 (denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G)).comp
557 (completedGroupAlgebraNaturalSourceRingEquiv
558 (R := R) (G := G)).surjective.denseRange
559 (continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G))
561/-- A finite-stage group-algebra map with the natural-topology source kept explicit in its type. -/
562def completedGroupAlgebraNaturalSourceStageMap (U : CompletedGroupAlgebraIndex G) :
563 CompletedGroupAlgebraNaturalSource R G →+* CompletedGroupAlgebraStage R G U :=
564 (completedGroupAlgebraStageMap R G U).comp
565 (completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G)).toRingHom
567/-- The finite-stage map from the natural-source wrapper is the ordinary stage map after
568forgetting the wrapper. -/
569@[simp]
570theorem completedGroupAlgebraNaturalSourceStageMap_apply
571 (U : CompletedGroupAlgebraIndex G) (x : CompletedGroupAlgebraNaturalSource R G) :
572 completedGroupAlgebraNaturalSourceStageMap R G U x =
573 completedGroupAlgebraStageMap R G U x.toMonoidAlgebra := by
574 change completedGroupAlgebraStageMap R G U
575 ((completedGroupAlgebraNaturalSourceRingEquiv (R := R) (G := G)) x) =
576 completedGroupAlgebraStageMap R G U x.toMonoidAlgebra
577 rfl
579/--
580The canonical map as a continuous \(R\)-linear map for the topology induced from
581\(\widehat{R[G]}\).
582-/
583def toCompletedGroupAlgebraContinuousLinearMap_naturalTopology :
584 letI : TopologicalSpace (MonoidAlgebra R G) :=
585 completedGroupAlgebraNaturalTopology R G
586 MonoidAlgebra R G →L[R] CompletedGroupAlgebraCarrier R G := by
587 letI : TopologicalSpace (MonoidAlgebra R G) :=
588 completedGroupAlgebraNaturalTopology R G
589 exact
590 { toLinearMap := toCompletedGroupAlgebraLinearMap R G
591 cont := continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G) }
593omit [IsTopologicalRing R] in
594/--
595The kernel-neighborhood topology is exactly the topology induced by the canonical map from
596\(R[G]\) to the two-parameter kernel-neighborhood limit.
597-/
598theorem groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit :
599 groupAlgebraOpenFiniteQuotientKernelTopology R G =
600 TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)
601 inferInstance := by
602 let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
603 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
604 TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
605 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
606 change TopologicalSpace.induced (groupAlgebraOpenFiniteQuotientProductMap R G) inferInstance =
607 TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)
608 (TopologicalSpace.induced (fun z : S.inverseLimit => z.1) inferInstance)
609 rw [induced_compose]
610 rfl
612/--
613Under the profinite coefficient hypothesis, the topology on \(R[G]\) induced from
614\(\widehat{R[G]}\) agrees with the topology induced by the two-parameter kernel-neighborhood
615limit.
616-/
617theorem completedGroupAlgebraNaturalTopology_eq_induced_toOpenFiniteQuotientLimit
618 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
619 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
620 completedGroupAlgebraNaturalTopology R G =
621 TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)
622 inferInstance := by
623 let e := completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph (R := R) (G := G)
624 have hcomp : e ∘ toCompletedGroupAlgebra R G =
625 toCompletedGroupAlgebraOpenFiniteQuotientLimit R G := by
626 funext x
627 exact completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra
628 (R := R) (G := G) x
629 dsimp [completedGroupAlgebraNaturalTopology]
630 rw [e.isInducing.eq_induced]
631 rw [induced_compose]
632 rw [hcomp]
634/--
635Ribes--Zalesskii Section \(5.3\) natural topology comparison: the topology on the abstract group
636algebra induced from \(\widehat{R[G]}\) is the kernel-neighborhood topology generated by the
637maps \(R[G] \to (R/I)[G/U]\).
638-/
639theorem completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
640 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
641 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
642 completedGroupAlgebraNaturalTopology R G =
643 groupAlgebraOpenFiniteQuotientKernelTopology R G := by
644 rw [completedGroupAlgebraNaturalTopology_eq_induced_toOpenFiniteQuotientLimit
645 (R := R) (G := G),
646 groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit (R := R) (G := G)]
648/-- The two source wrappers are canonically homeomorphic once the coefficient ring is profinite. -/
649def completedGroupAlgebraNaturalSourceHomeomorphKernelSource
650 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
651 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
652 CompletedGroupAlgebraNaturalSource R G ≃ₜ CompletedGroupAlgebraKernelSource R G where
653 toEquiv :=
654 (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).trans
655 (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).symm
656 continuous_toFun := by
657 let τnat := completedGroupAlgebraNaturalTopology R G
658 let τker := groupAlgebraOpenFiniteQuotientKernelTopology R G
659 have hτ : τnat = τker :=
660 completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
661 (R := R) (G := G)
662 have hforget :
663 @Continuous (CompletedGroupAlgebraNaturalSource R G) (MonoidAlgebra R G)
664 inferInstance τnat
665 (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)) := by
666 letI : TopologicalSpace (MonoidAlgebra R G) := τnat
667 exact
668 (completedGroupAlgebraNaturalSourceHomeomorph (R := R) (G := G)).continuous
669 have hid : @Continuous (MonoidAlgebra R G) (MonoidAlgebra R G) τnat τker id := by
670 rw [hτ]
671 exact continuous_id
672 have hwrap :
673 @Continuous (MonoidAlgebra R G) (CompletedGroupAlgebraKernelSource R G)
674 τker inferInstance
675 (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).symm :=
676 (completedGroupAlgebraKernelSourceHomeomorph (R := R) (G := G)).symm.continuous
677 have hraw :=
678 @Continuous.comp
679 (CompletedGroupAlgebraNaturalSource R G) (MonoidAlgebra R G) (MonoidAlgebra R G)
680 inferInstance τnat τker
681 (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)) id hid hforget
682 have htotal :=
683 @Continuous.comp
684 (CompletedGroupAlgebraNaturalSource R G) (MonoidAlgebra R G)
685 (CompletedGroupAlgebraKernelSource R G)
686 inferInstance τker inferInstance
687 (id ∘ completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G))
688 (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).symm hwrap hraw
689 change Continuous
690 ((completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)).symm ∘ id ∘
691 (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)))
692 exact htotal
693 continuous_invFun := by
694 let τnat := completedGroupAlgebraNaturalTopology R G
695 let τker := groupAlgebraOpenFiniteQuotientKernelTopology R G
696 have hτ : τnat = τker :=
697 completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
698 (R := R) (G := G)
699 have hforget :
700 @Continuous (CompletedGroupAlgebraKernelSource R G) (MonoidAlgebra R G)
701 inferInstance τker
702 (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)) :=
703 (completedGroupAlgebraKernelSourceHomeomorph (R := R) (G := G)).continuous
704 have hid : @Continuous (MonoidAlgebra R G) (MonoidAlgebra R G) τker τnat id := by
705 rw [hτ]
706 exact continuous_id
707 have hwrap :
708 @Continuous (MonoidAlgebra R G) (CompletedGroupAlgebraNaturalSource R G)
709 τnat inferInstance
710 (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).symm := by
711 letI : TopologicalSpace (MonoidAlgebra R G) := τnat
712 exact
713 (completedGroupAlgebraNaturalSourceHomeomorph (R := R) (G := G)).symm.continuous
714 have hraw :=
715 @Continuous.comp
716 (CompletedGroupAlgebraKernelSource R G) (MonoidAlgebra R G) (MonoidAlgebra R G)
717 inferInstance τker τnat
718 (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)) id hid hforget
719 have htotal :=
720 @Continuous.comp
721 (CompletedGroupAlgebraKernelSource R G) (MonoidAlgebra R G)
722 (CompletedGroupAlgebraNaturalSource R G)
723 inferInstance τnat inferInstance
724 (id ∘ completedGroupAlgebraKernelSourceEquiv (R := R) (G := G))
725 (completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).symm hwrap hraw
726 change Continuous
727 ((completedGroupAlgebraNaturalSourceEquiv (R := R) (G := G)).symm ∘ id ∘
728 (completedGroupAlgebraKernelSourceEquiv (R := R) (G := G)))
729 exact htotal
731/-- Canonical map from the kernel-neighborhood source wrapper. -/
732def toCompletedGroupAlgebraKernelSourceRingHom :
733 CompletedGroupAlgebraKernelSource R G →+* CompletedGroupAlgebraCarrier R G :=
734 (toCompletedGroupAlgebraRingHom R G).comp
735 (completedGroupAlgebraKernelSourceRingEquiv (R := R) (G := G)).toRingHom
737/--
738The canonical map \(R[G] \to \widehat{R[G]}\) is continuous for the kernel-neighborhood topology
739on \(R[G]\).
740-/
741theorem continuous_toCompletedGroupAlgebraRingHom_kernelTopology
742 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
743 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
744 letI : TopologicalSpace (MonoidAlgebra R G) :=
745 groupAlgebraOpenFiniteQuotientKernelTopology R G
746 Continuous (toCompletedGroupAlgebraRingHom R G) := by
747 let τnat := completedGroupAlgebraNaturalTopology R G
748 let τker := groupAlgebraOpenFiniteQuotientKernelTopology R G
749 have hτ : τnat = τker :=
750 completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
751 (R := R) (G := G)
752 change @Continuous (MonoidAlgebra R G) (CompletedGroupAlgebraCarrier R G)
753 τker inferInstance (toCompletedGroupAlgebraRingHom R G)
754 rw [← hτ]
755 exact continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G)
757/-- The kernel-wrapper canonical map is continuous under the profinite coefficient hypothesis. -/
758theorem continuous_toCompletedGroupAlgebraKernelSourceRingHom
759 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
760 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
761 Continuous (toCompletedGroupAlgebraKernelSourceRingHom (R := R) (G := G)) := by
762 letI : TopologicalSpace (MonoidAlgebra R G) :=
763 groupAlgebraOpenFiniteQuotientKernelTopology R G
764 exact
765 (continuous_toCompletedGroupAlgebraRingHom_kernelTopology (R := R) (G := G)).comp
766 (completedGroupAlgebraKernelSourceHomeomorph (R := R) (G := G)).continuous
768/-- The canonical map as a continuous \(R\)-linear map for the kernel-neighborhood topology. -/
769def toCompletedGroupAlgebraContinuousLinearMap_kernelTopology
770 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] [Nonempty
771 (CompletedGroupAlgebraOpenQuotientIndex R G)] :
772 letI : TopologicalSpace (MonoidAlgebra R G) :=
773 groupAlgebraOpenFiniteQuotientKernelTopology R G
774 MonoidAlgebra R G →L[R] CompletedGroupAlgebraCarrier R G := by
775 letI : TopologicalSpace (MonoidAlgebra R G) :=
776 groupAlgebraOpenFiniteQuotientKernelTopology R G
777 exact
778 { toLinearMap := toCompletedGroupAlgebraLinearMap R G
779 cont := continuous_toCompletedGroupAlgebraRingHom_kernelTopology
780 (R := R) (G := G) }
782end
784end CompletedGroupAlgebra