Yamaguchi Lean 4 Library
CompletedGroupAlgebra/InClassFunctoriality/Maps.lean
CompletedGroupAlgebra/InClassFunctoriality/Maps/Source

CompletedGroupAlgebra/InClassFunctoriality/Maps.lean

1import CompletedGroupAlgebra.InClassFunctoriality.StageMaps
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/InClassFunctoriality/Maps.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Functoriality of 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
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]
33variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
35/-- A continuous homomorphism of groups induces a ring homomorphism on `C`-indexed completed
36group algebras, when `C` is hereditary. -/
38 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
40 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
41 (φ : G →* H) (hφ : Continuous φ) :
42 CompletedGroupAlgebraInClass C hC R G →+* CompletedGroupAlgebraInClass C hC R H where
43 toFun x := ⟨fun V =>
45 (G := G) (H := H) C hHer (R := R) φ hφ V
46 (completedGroupAlgebraProjectionInClass C hC R G
47 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x), by
48 intro V W hVW
49 change completedGroupAlgebraTransitionInClass C R H hVW
51 (G := G) (H := H) C hHer (R := R) φ hφ W
52 (completedGroupAlgebraProjectionInClass C hC R G
53 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W) x)) =
55 (G := G) (H := H) C hHer (R := R) φ hφ V
56 (completedGroupAlgebraProjectionInClass C hC R G
57 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
58 have hcomp := congrFun
59 (congrArg DFunLike.coe
61 (R := R) (G := G) (H := H) C hHer φ hφ hVW))
62 (completedGroupAlgebraProjectionInClass C hC R G
63 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W) x)
64 rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
66 (R := R) (G := G) C hC
67 (completedGroupAlgebraComapIndexInClass_mono
68 (G := G) (H := H) C hHer φ hφ hVW) x]
69 exact hcomp⟩
70 map_zero' := by
71 apply (completedGroupAlgebraSystemInClass C hC R H).ext
72 intro V
74 (G := G) (H := H) C hHer (R := R) φ hφ V)
75 map_one' := by
76 apply (completedGroupAlgebraSystemInClass C hC R H).ext
77 intro V
79 (G := G) (H := H) C hHer (R := R) φ hφ V)
80 map_add' x y := by
81 apply (completedGroupAlgebraSystemInClass C hC R H).ext
82 intro V
84 (G := G) (H := H) C hHer (R := R) φ hφ V)
85 (completedGroupAlgebraProjectionInClass C hC R G
86 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
87 (completedGroupAlgebraProjectionInClass C hC R G
88 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)
89 map_mul' x y := by
90 apply (completedGroupAlgebraSystemInClass C hC R H).ext
91 intro V
93 (G := G) (H := H) C hHer (R := R) φ hφ V)
94 (completedGroupAlgebraProjectionInClass C hC R G
95 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
96 (completedGroupAlgebraProjectionInClass C hC R G
97 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)
99/-- The in-class completed group-algebra map is characterized by its finite-stage projections. -/
100@[simp 900]
102 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
104 (φ : G →* H) (hφ : Continuous φ)
105 (V : CompletedGroupAlgebraIndexInClass H C) (x : CompletedGroupAlgebraInClass C hC R G) :
106 completedGroupAlgebraProjectionInClass C hC R H V
107 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x) =
109 (G := G) (H := H) C hHer (R := R) φ hφ V
110 (completedGroupAlgebraProjectionInClass C hC R G
111 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x) :=
112 rfl
114/-- Algebra form of `completedGroupAlgebraMapInClass`. -/
116 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
118 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
119 (φ : G →* H) (hφ : Continuous φ) :
120 CompletedGroupAlgebraInClass C hC R G →ₐ[R] CompletedGroupAlgebraInClass C hC R H where
121 toRingHom := completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
122 commutes' := by
123 intro r
124 apply (completedGroupAlgebraSystemInClass C hC R H).ext
125 intro V
127 (G := G) (H := H) C hHer (R := R) φ hφ V
128 (algebraMap R
129 (CompletedGroupAlgebraStageInClass C R G
130 (completedGroupAlgebraComapIndexInClass
131 (G := G) (H := H) C hHer φ hφ V)) r) =
132 algebraMap R (CompletedGroupAlgebraStageInClass C R H V) r
134 (R := R) (G := G) (H := H) C hHer φ hφ V r
136/-- The algebra-hom version of the in-class map has the same underlying function. -/
137@[simp]
139 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
141 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C hC R G) :
142 completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ x =
143 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x :=
144 rfl
146/-- The induced `C`-indexed completed-group-algebra map is continuous. -/
148 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
150 (φ : G →* H) (hφ : Continuous φ) :
151 Continuous (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ) := by
152 let A := CompletedGroupAlgebraInClass C hC R G
153 let S := completedGroupAlgebraSystemInClass C hC R H
154 letI : ∀ V : CompletedGroupAlgebraIndexInClass H C,
155 TopologicalSpace (CompletedGroupAlgebraStageInClass C R H V) :=
156 fun V => S.topologicalSpace V
157 have hval : Continuous fun x : A =>
158 ((completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x) :
159 (V : CompletedGroupAlgebraIndexInClass H C) → S.X V) := by
160 change Continuous fun x : A =>
161 fun V : CompletedGroupAlgebraIndexInClass H C =>
163 (G := G) (H := H) C hHer (R := R) φ hφ V
164 (completedGroupAlgebraProjectionInClass C hC R G
165 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
166 apply continuous_pi
167 intro V
168 letI : TopologicalSpace
169 (CompletedGroupAlgebraStageInClass C R G
170 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
171 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace
172 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
174 (R := R) (G := G) (H := H) C hC hHer φ hφ V).comp
175 ((completedGroupAlgebraSystemInClass C hC R G).continuous_projection
176 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
177 exact Continuous.subtype_mk hval fun x =>
178 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x).2
180/-- The in-class completed group-algebra map composes with the dense abstract map as expected. -/
182 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
184 (φ : G →* H) (hφ : Continuous φ) :
185 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ).comp
188 (MonoidAlgebra.mapDomainRingHom R φ) := by
189 apply RingHom.ext
190 intro x
191 apply (completedGroupAlgebraSystemInClass C hC R H).ext
192 intro V
193 have hstage := congrFun
194 (congrArg DFunLike.coe
196 (R := R) (G := G) (H := H) C hHer φ hφ V))
197 x
199 (G := G) (H := H) C hHer (R := R) φ hφ V
200 (completedGroupAlgebraStageMapInClass C R G
201 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x) =
202 completedGroupAlgebraStageMapInClass C R H V (MonoidAlgebra.mapDomainRingHom R φ x)
203 exact hstage
205/-- A surjective continuous homomorphism onto a pro-`C` group induces a surjective map on
206`C`-indexed completed group algebras. -/
208 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
211 (hR : IsProfiniteRing R) (hH : IsProCGroup C H)
212 (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
213 Function.Surjective
214 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ) := by
215 let f := completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
216 letI : CompactSpace (CompletedGroupAlgebraInClass C hC R G) :=
218 letI : T2Space (CompletedGroupAlgebraInClass C hC R H) :=
219 completedGroupAlgebraInClass_t2Space (R := R) (G := H) C hC hR
220 have hfcont : Continuous f :=
222 C hC hHer φ hφ
223 have hclosed : IsClosed (Set.range f) := (isCompact_range hfcont).isClosed
224 have hdense : DenseRange (toCompletedGroupAlgebraInClassRingHom C hC R H) := by
225 change DenseRange (toCompletedGroupAlgebraInClass C hC R H)
226 exact denseRange_toCompletedGroupAlgebraInClass (R := R) (G := H) C hC hForm hH
227 have hcanonical_subset :
228 Set.range (toCompletedGroupAlgebraInClassRingHom C hC R H) ⊆ Set.range f := by
229 intro y hy
230 rcases hy with ⟨a, rfl⟩
231 rcases (show Function.Surjective (MonoidAlgebra.mapDomainRingHom R φ) from by
232 simpa [MonoidAlgebra.mapDomainRingHom_apply] using
233 (Finsupp.mapDomain_surjective (M := R) hφsurj)) a with
234 ⟨b, hb⟩
235 refine ⟨toCompletedGroupAlgebraInClassRingHom C hC R G b, ?_⟩
236 have hcomp := congrFun
237 (congrArg DFunLike.coe
239 (R := R) (G := G) (H := H) C hC hHer φ hφ))
240 b
241 simpa [f, RingHom.comp_apply, hb] using hcomp
242 intro y
243 have hycanonical :
244 y ∈ closure (Set.range (toCompletedGroupAlgebraInClassRingHom C hC R H)) := by
245 rw [hdense.closure_range]
246 exact Set.mem_univ y
247 have hyf : y ∈ closure (Set.range f) :=
248 closure_mono hcanonical_subset hycanonical
249 exact hclosed.closure_subset_iff.2 (fun z hz => hz) hyf
251/-- Continuous ring homomorphisms out of `[[R G]]_C` are determined by their values on the
252dense abstract group algebra. -/
254 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
256 (hR : IsProfiniteRing R) (hG : IsProCGroup C G)
257 {f g : CompletedGroupAlgebraInClass C hC R G →+*
258 CompletedGroupAlgebraInClass C hC R H}
259 (hf : Continuous f) (hg : Continuous g)
260 (hfg : f.comp (toCompletedGroupAlgebraInClassRingHom C hC R G) =
262 f = g := by
263 letI : T2Space (CompletedGroupAlgebraInClass C hC R H) :=
264 completedGroupAlgebraInClass_t2Space (R := R) (G := H) C hC hR
265 have hdense : DenseRange (toCompletedGroupAlgebraInClassRingHom C hC R G) := by
266 change DenseRange (toCompletedGroupAlgebraInClass C hC R G)
267 exact denseRange_toCompletedGroupAlgebraInClass (R := R) (G := G) C hC hForm hG
268 have hcomp : (f : CompletedGroupAlgebraInClass C hC R G →
269 CompletedGroupAlgebraInClass C hC R H) ∘
271 (g : CompletedGroupAlgebraInClass C hC R G →
272 CompletedGroupAlgebraInClass C hC R H) ∘
274 funext x
275 exact congrFun (congrArg DFunLike.coe hfg) x
276 have hfun : (f : CompletedGroupAlgebraInClass C hC R G →
277 CompletedGroupAlgebraInClass C hC R H) = g :=
278 DenseRange.equalizer hdense hf hg hcomp
279 exact RingHom.ext fun x => congrFun hfun x
281/-- Identity law for the `C`-indexed completed-group-algebra functor. -/
283 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
286 (hR : IsProfiniteRing R) (hG : IsProCGroup C G) :
287 completedGroupAlgebraMapInClass (G := G) (H := G) C hC hHer R
288 (MonoidHom.id G) continuous_id =
289 RingHom.id (CompletedGroupAlgebraInClass C hC R G) := by
291 (R := R) (G := G) (H := G) C hC hForm hR hG
292 · exact continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := G)
293 C hC hHer (MonoidHom.id G) continuous_id
294 · exact continuous_id
297 rfl
299/-- Identity law for the `C`-indexed completed-group-algebra functor, as an `R`-algebra
300homomorphism. -/
302 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
305 (hR : IsProfiniteRing R) (hG : IsProCGroup C G) :
306 completedGroupAlgebraMapAlgHomInClass (G := G) (H := G) C hC hHer R
307 (MonoidHom.id G) continuous_id =
308 AlgHom.id R (CompletedGroupAlgebraInClass C hC R G) := by
309 apply AlgHom.ext
310 intro x
311 have h := congrFun
312 (congrArg DFunLike.coe
313 (completedGroupAlgebraMapInClass_id (R := R) (G := G) C hC hForm hHer hR hG))
314 x
315 simpa using h
317/-- Composition law for the `C`-indexed completed-group-algebra functor. -/
319 {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
320 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
323 (hR : IsProfiniteRing R) (hG : IsProCGroup C G)
324 (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
325 (completedGroupAlgebraMapInClass (G := H) (H := K) C hC hHer R ψ hψ).comp
326 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ) =
327 completedGroupAlgebraMapInClass (G := G) (H := K) C hC hHer R
328 (ψ.comp φ) (hψ.comp hφ) := by
330 (R := R) (G := G) (H := K) C hC hForm hR hG
331 · exact (continuous_completedGroupAlgebraMapInClass (R := R) (G := H) (H := K)
332 C hC hHer ψ hψ).comp
334 C hC hHer φ hφ)
335 · exact continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := K)
336 C hC hHer (ψ.comp φ) (hψ.comp hφ)
337 · apply RingHom.ext
338 intro x
339 have hφdense := congrFun
340 (congrArg DFunLike.coe
342 (R := R) (G := G) (H := H) C hC hHer φ hφ))
343 x
344 have hψdense := congrFun
345 (congrArg DFunLike.coe
347 (R := R) (G := H) (H := K) C hC hHer ψ hψ))
348 (MonoidAlgebra.mapDomainRingHom R φ x)
349 have hdomain := congrFun
350 (congrArg DFunLike.coe
352 x
353 have hcompdense := congrFun
354 (congrArg DFunLike.coe
356 (R := R) (G := G) (H := K) C hC hHer (ψ.comp φ) (hψ.comp hφ)))
357 x
358 calc
359 (((completedGroupAlgebraMapInClass (G := H) (H := K) C hC hHer R ψ hψ).comp
360 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)).comp
362 =
363 completedGroupAlgebraMapInClass (G := H) (H := K) C hC hHer R ψ hψ
364 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
366 _ =
367 completedGroupAlgebraMapInClass (G := H) (H := K) C hC hHer R ψ hψ
369 (MonoidAlgebra.mapDomainRingHom R φ x)) := by
370 have hφdense' :
371 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
374 (MonoidAlgebra.mapDomainRingHom R φ x) := by
375 simpa [RingHom.comp_apply] using hφdense
376 exact congrArg (completedGroupAlgebraMapInClass (G := H) (H := K)
377 C hC hHer R ψ hψ) hφdense'
378 _ =
380 (MonoidAlgebra.mapDomainRingHom R ψ (MonoidAlgebra.mapDomainRingHom R φ x)) := by
381 simpa [RingHom.comp_apply] using hψdense
382 _ =
384 (MonoidAlgebra.mapDomainRingHom R (ψ.comp φ) x) := by
385 exact congrArg (toCompletedGroupAlgebraInClassRingHom C hC R K) (by
386 change (MonoidAlgebra.mapDomainRingHom R ψ)
387 ((MonoidAlgebra.mapDomainRingHom R φ) x) =
388 (MonoidAlgebra.mapDomainRingHom R (ψ.comp φ)) x at hdomain
389 exact hdomain)
390 _ =
391 ((completedGroupAlgebraMapInClass (G := G) (H := K) C hC hHer R
392 (ψ.comp φ) (hψ.comp hφ)).comp
394 simpa [RingHom.comp_apply] using hcompdense.symm
396/-- Composition law for the `C`-indexed completed-group-algebra functor, as an `R`-algebra
397homomorphism. -/
399 {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
400 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
403 (hR : IsProfiniteRing R) (hG : IsProCGroup C G)
404 (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
405 (completedGroupAlgebraMapAlgHomInClass (G := H) (H := K) C hC hHer R ψ hψ).comp
406 (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ) =
407 completedGroupAlgebraMapAlgHomInClass (G := G) (H := K) C hC hHer R
408 (ψ.comp φ) (hψ.comp hφ) := by
409 apply AlgHom.ext
410 intro x
411 have h := congrFun
412 (congrArg DFunLike.coe
413 (completedGroupAlgebraMapInClass_comp (R := R) (G := G) (H := H) (K := K)
414 C hC hForm hHer hR hG φ hφ ψ hψ))
415 x
416 simpa using h
418/-- The in-class completed group-algebra map sends group-like elements to group-like elements. -/
419@[simp]
421 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
423 (φ : G →* H) (hφ : Continuous φ) (g : G) :
424 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
425 (toCompletedGroupAlgebraInClass C hC R G (MonoidAlgebra.of R G g)) =
426 toCompletedGroupAlgebraInClass C hC R H (MonoidAlgebra.of R H (φ g)) := by
427 have h := congrFun
428 (congrArg DFunLike.coe
430 (R := R) (G := G) (H := H) C hC hHer φ hφ))
431 (MonoidAlgebra.of R G g)
432 simpa [RingHom.comp_apply, finiteGroupAlgebra_mapDomainRingHom_of] using h
434/-- The in-class completed group-algebra map sends group-like augmentation generators to their images. -/
435@[simp]
437 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
439 (φ : G →* H) (hφ : Continuous φ) (g : G) :
440 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
441 (toCompletedGroupAlgebraInClass C hC R G (MonoidAlgebra.of R G g) - 1) =
442 toCompletedGroupAlgebraInClass C hC R H (MonoidAlgebra.of R H (φ g)) - 1 := by
445end