Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Maps
ProCGroups/CompletedGroupAlgebra/InClassFunctoriality/Maps/Source

Source: ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Maps

1import ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.StageMaps
3/-!
4# Completed Group Algebra / Functoriality Within a Class / Maps
6This module lifts hereditary \(C\)-indexed finite-stage maps to the named completed carrier and
7proves their algebraic, topological, and dense-subalgebra characterizations.
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]
25variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27/--
28A continuous homomorphism of groups induces a ring homomorphism on \(C\)-indexed completed group
29algebras, when \(C\) is hereditary.
30-/
31def completedGroupAlgebraMapInClass
32 (C : ProCGroups.FiniteGroupClass.{v})
34 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
35 (φ : G →* H) (hφ : Continuous φ) :
36 CompletedGroupAlgebraInClass C R G →+* CompletedGroupAlgebraInClass C R H where
37 toFun x :=
38 (completedGroupAlgebraInClassCompatibleFamilyEquiv
39 (R := R) (G := H) C).symm
40 ((completedGroupAlgebraSystemInClass C R H).inverseLimitLift
41 (fun V x =>
42 completedGroupAlgebraFunctorialStageMapInClass
43 (G := G) (H := H) C hHer (R := R) φ hφ V
44 (completedGroupAlgebraProjectionInClass C R G
45 (completedGroupAlgebraComapIndexInClass
46 (G := G) (H := H) C hHer φ hφ V) x))
47 (by
48 intro V W hVW
49 funext x
50 have hcomp := congrFun
51 (congrArg DFunLike.coe
52 (completedGroupAlgebraFunctorialStageMapInClass_transition
53 (R := R) (G := G) (H := H) C hHer φ hφ hVW))
54 (completedGroupAlgebraProjectionInClass C R G
55 (completedGroupAlgebraComapIndexInClass
56 (G := G) (H := H) C hHer φ hφ W) x)
57 rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
58 simp only [Function.comp_apply]
59 rw [← completedGroupAlgebraProjectionInClass_compatible
60 (R := R) (G := G) C
61 (completedGroupAlgebraComapIndexInClass_mono
62 (G := G) (H := H) C hHer φ hφ hVW) x]
63 exact hcomp) x)
64 map_zero' := by
65 apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
66 intro V
67 exact map_zero (completedGroupAlgebraFunctorialStageMapInClass
68 (G := G) (H := H) C hHer (R := R) φ hφ V)
69 map_one' := by
70 apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
71 intro V
72 exact map_one (completedGroupAlgebraFunctorialStageMapInClass
73 (G := G) (H := H) C hHer (R := R) φ hφ V)
74 map_add' x y := by
75 apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
76 intro V
77 exact map_add (completedGroupAlgebraFunctorialStageMapInClass
78 (G := G) (H := H) C hHer (R := R) φ hφ V)
79 (completedGroupAlgebraProjectionInClass C R G
80 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
81 (completedGroupAlgebraProjectionInClass C R G
82 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)
83 map_mul' x y := by
84 apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
85 intro V
86 exact map_mul (completedGroupAlgebraFunctorialStageMapInClass
87 (G := G) (H := H) C hHer (R := R) φ hφ V)
88 (completedGroupAlgebraProjectionInClass C R G
89 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
90 (completedGroupAlgebraProjectionInClass C R G
91 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)
93/-- The in-class completed group-algebra map is characterized by its finite-stage projections. -/
94@[simp 900]
95theorem completedGroupAlgebraProjectionInClass_map
96 (C : ProCGroups.FiniteGroupClass.{v})
98 (φ : G →* H) (hφ : Continuous φ)
99 (V : CompletedGroupAlgebraIndexInClass H C) (x : CompletedGroupAlgebraInClass C R G) :
100 completedGroupAlgebraProjectionInClass C R H V
101 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x) =
102 completedGroupAlgebraFunctorialStageMapInClass
103 (G := G) (H := H) C hHer (R := R) φ hφ V
104 (completedGroupAlgebraProjectionInClass C R G
105 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x) :=
106 rfl
108/--
109A continuous group homomorphism \(\varphi:G\to H\) induces an \(R\)-algebra homomorphism between
110the corresponding \(C\)-indexed completed group algebras.
111-/
112def completedGroupAlgebraMapAlgHomInClass
113 (C : ProCGroups.FiniteGroupClass.{v})
115 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
116 (φ : G →* H) (hφ : Continuous φ) :
117 CompletedGroupAlgebraInClass C R G →ₐ[R] CompletedGroupAlgebraInClass C R H where
118 toRingHom := completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
119 commutes' := by
120 intro r
121 apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
122 intro V
123 change completedGroupAlgebraFunctorialStageMapInClass
124 (G := G) (H := H) C hHer (R := R) φ hφ V
125 (algebraMap R
126 (CompletedGroupAlgebraStageInClass C R G
127 (completedGroupAlgebraComapIndexInClass
128 (G := G) (H := H) C hHer φ hφ V)) r) =
129 algebraMap R (CompletedGroupAlgebraStageInClass C R H V) r
130 exact completedGroupAlgebraFunctorialStageMapInClass_algebraMap
131 (R := R) (G := G) (H := H) C hHer φ hφ V r
133/--
134Evaluating the algebra homomorphism induced by \(\varphi\) at \(x\) gives
135`completedGroupAlgebraMapInClass` applied to \(x\).
136-/
137@[simp]
138theorem completedGroupAlgebraMapAlgHomInClass_apply
139 (C : ProCGroups.FiniteGroupClass.{v})
141 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
142 completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ x =
143 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x :=
144 rfl
146/-- The induced \(C\)-indexed completed-group-algebra map is continuous. -/
147theorem continuous_completedGroupAlgebraMapInClass
148 (C : ProCGroups.FiniteGroupClass.{v})
150 (φ : G →* H) (hφ : Continuous φ) :
151 Continuous (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ) := by
152 let S := completedGroupAlgebraSystemInClass C R H
153 letI : ∀ V, TopologicalSpace (CompletedGroupAlgebraStageInClass C R H V) :=
154 fun V => (completedGroupAlgebraSystemInClass C R H).topologicalSpace V
155 let π : ∀ V : CompletedGroupAlgebraIndexInClass H C,
156 CompletedGroupAlgebraInClass C R G →
157 CompletedGroupAlgebraStageInClass C R H V :=
158 fun V x =>
159 completedGroupAlgebraFunctorialStageMapInClass
160 (G := G) (H := H) C hHer (R := R) φ hφ V
161 (completedGroupAlgebraProjectionInClass C R G
162 (completedGroupAlgebraComapIndexInClass
163 (G := G) (H := H) C hHer φ hφ V) x)
164 have hπ : ∀ V, Continuous (π V) := by
165 intro V
166 letI : TopologicalSpace
167 (CompletedGroupAlgebraStageInClass C R G
168 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
169 (completedGroupAlgebraSystemInClass C R G).topologicalSpace
170 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
171 exact (continuous_completedGroupAlgebraFunctorialStageMapInClass
172 (R := R) (G := G) (H := H) C hHer φ hφ V).comp
173 ((completedGroupAlgebraSystemInClass C R G).continuous_projection
174 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
175 have hcompat : S.CompatibleMaps π := by
176 intro V W hVW
177 funext x
178 have hcomp := congrFun
179 (congrArg DFunLike.coe
180 (completedGroupAlgebraFunctorialStageMapInClass_transition
181 (R := R) (G := G) (H := H) C hHer φ hφ hVW))
182 (completedGroupAlgebraProjectionInClass C R G
183 (completedGroupAlgebraComapIndexInClass
184 (G := G) (H := H) C hHer φ hφ W) x)
185 rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
186 simp only [S, π, Function.comp_apply]
187 rw [← completedGroupAlgebraProjectionInClass_compatible
188 (R := R) (G := G) C
189 (completedGroupAlgebraComapIndexInClass_mono
190 (G := G) (H := H) C hHer φ hφ hVW) x]
191 exact hcomp
192 change Continuous (S.inverseLimitLift π hcompat)
193 exact S.continuous_inverseLimitLift π hπ hcompat
195/-- The in-class completed group-algebra map composes with the dense abstract map as expected. -/
196theorem completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
197 (C : ProCGroups.FiniteGroupClass.{v})
199 (φ : G →* H) (hφ : Continuous φ) :
200 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ).comp
201 (toCompletedGroupAlgebraInClassRingHom C R G) =
202 (toCompletedGroupAlgebraInClassRingHom C R H).comp
203 (MonoidAlgebra.mapDomainRingHom R φ) := by
204 apply RingHom.ext
205 intro x
206 apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
207 intro V
208 have hstage := congrFun
209 (congrArg DFunLike.coe
210 (completedGroupAlgebraFunctorialStageMapInClass_comp_stageMap
211 (R := R) (G := G) (H := H) C hHer φ hφ V))
212 x
213 change completedGroupAlgebraFunctorialStageMapInClass
214 (G := G) (H := H) C hHer (R := R) φ hφ V
215 (completedGroupAlgebraStageMapInClass C R G
216 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x) =
217 completedGroupAlgebraStageMapInClass C R H V (MonoidAlgebra.mapDomainRingHom R φ x)
218 exact hstage
220/--
221A surjective continuous homomorphism onto a pro-\(C\) group induces a surjective map on
222\(C\)-indexed completed group algebras.
223-/
224theorem completedGroupAlgebraMapInClass_surjective_of_surjective
225 (C : ProCGroups.FiniteGroupClass.{v})
228 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
229 (hH : HasOpenNormalBasisInClass C H)
230 (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
231 Function.Surjective
232 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ) := by
233 let f := completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
234 letI : CompactSpace (CompletedGroupAlgebraInClass C R G) :=
235 completedGroupAlgebraInClass_compactSpace (R := R) (G := G) C
236 letI : T2Space (CompletedGroupAlgebraInClass C R H) :=
237 completedGroupAlgebraInClass_t2Space (R := R) (G := H) C
238 have hfcont : Continuous f :=
239 continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := H)
240 C hHer φ hφ
241 have hclosed : IsClosed (Set.range f) := (isCompact_range hfcont).isClosed
242 have hdense : DenseRange (toCompletedGroupAlgebraInClassRingHom C R H) := by
243 change DenseRange (toCompletedGroupAlgebraInClass C R H)
244 exact denseRange_toCompletedGroupAlgebraInClass (R := R) (G := H) C hForm hH
245 have hcanonical_subset :
246 Set.range (toCompletedGroupAlgebraInClassRingHom C R H) ⊆ Set.range f := by
247 intro y hy
248 rcases hy with ⟨a, rfl⟩
249 obtain ⟨bCoeff, hbCoeff⟩ :=
250 Finsupp.mapDomain_surjective (M := R) hφsurj a.coeff
251 let b : MonoidAlgebra R G := MonoidAlgebra.ofCoeff bCoeff
252 have hb : MonoidAlgebra.mapDomainRingHom R φ b = a := by
253 apply MonoidAlgebra.coeff_injective
254 exact hbCoeff
255 refine ⟨toCompletedGroupAlgebraInClassRingHom C R G b, ?_⟩
256 have hcomp := congrFun
257 (congrArg DFunLike.coe
258 (completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
259 (R := R) (G := G) (H := H) C hHer φ hφ))
260 b
261 simpa [f, RingHom.comp_apply, hb] using hcomp
262 intro y
263 have hycanonical :
264 y ∈ closure (Set.range (toCompletedGroupAlgebraInClassRingHom C R H)) := by
265 rw [hdense.closure_range]
266 exact Set.mem_univ y
267 have hyf : y ∈ closure (Set.range f) :=
268 closure_mono hcanonical_subset hycanonical
269 exact hclosed.closure_subset_iff.2 (fun z hz => hz) hyf
271/--
272Continuous ring homomorphisms out of \(\widehat{R[G]}_C\) are determined by their values on the
273dense abstract group algebra.
274-/
275theorem completedGroupAlgebraInClassRingHom_ext_of_comp_toCompleted
276 (C : ProCGroups.FiniteGroupClass.{v})
278 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
279 (hG : HasOpenNormalBasisInClass C G)
280 {f g : CompletedGroupAlgebraInClass C R G →+*
281 CompletedGroupAlgebraInClass C R H}
282 (hf : Continuous f) (hg : Continuous g)
283 (hfg : f.comp (toCompletedGroupAlgebraInClassRingHom C R G) =
284 g.comp (toCompletedGroupAlgebraInClassRingHom C R G)) :
285 f = g := by
286 letI : T2Space (CompletedGroupAlgebraInClass C R H) :=
287 completedGroupAlgebraInClass_t2Space (R := R) (G := H) C
288 have hdense : DenseRange (toCompletedGroupAlgebraInClassRingHom C R G) := by
289 change DenseRange (toCompletedGroupAlgebraInClass C R G)
290 exact denseRange_toCompletedGroupAlgebraInClass (R := R) (G := G) C hForm hG
291 have hcomp : (f : CompletedGroupAlgebraInClass C R G →
292 CompletedGroupAlgebraInClass C R H) ∘
293 (toCompletedGroupAlgebraInClassRingHom C R G) =
294 (g : CompletedGroupAlgebraInClass C R G →
295 CompletedGroupAlgebraInClass C R H) ∘
296 (toCompletedGroupAlgebraInClassRingHom C R G) := by
297 funext x
298 exact congrFun (congrArg DFunLike.coe hfg) x
299 have hfun : (f : CompletedGroupAlgebraInClass C R G →
300 CompletedGroupAlgebraInClass C R H) = g :=
301 DenseRange.equalizer hdense hf hg hcomp
302 exact RingHom.ext fun x => congrFun hfun x
304/-- Identity law for the \(C\)-indexed completed-group-algebra functor. -/
305theorem completedGroupAlgebraMapInClass_id
306 (C : ProCGroups.FiniteGroupClass.{v})
309 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
310 (hG : HasOpenNormalBasisInClass C G) :
311 completedGroupAlgebraMapInClass (G := G) (H := G) C hHer R
312 (MonoidHom.id G) continuous_id =
313 RingHom.id (CompletedGroupAlgebraInClass C R G) := by
314 apply completedGroupAlgebraInClassRingHom_ext_of_comp_toCompleted
315 (R := R) (G := G) (H := G) C hForm hG
316 · exact continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := G)
317 C hHer (MonoidHom.id G) continuous_id
318 · exact continuous_id
319 · rw [completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass,
320 finiteGroupAlgebra_mapDomainRingHom_id]
321 rfl
323/--
324Identity law for the \(C\)-indexed completed-group-algebra functor, as an \(R\)-algebra
325homomorphism.
326-/
327theorem completedGroupAlgebraMapAlgHomInClass_id
328 (C : ProCGroups.FiniteGroupClass.{v})
331 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
332 (hG : HasOpenNormalBasisInClass C G) :
333 completedGroupAlgebraMapAlgHomInClass (G := G) (H := G) C hHer R
334 (MonoidHom.id G) continuous_id =
335 AlgHom.id R (CompletedGroupAlgebraInClass C R G) := by
336 apply AlgHom.ext
337 intro x
338 have h := congrFun
339 (congrArg DFunLike.coe
340 (completedGroupAlgebraMapInClass_id (R := R) (G := G) C hForm hHer hG))
341 x
342 simpa using h
344/-- Composition law for the \(C\)-indexed completed-group-algebra functor. -/
345theorem completedGroupAlgebraMapInClass_comp
346 {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
347 (C : ProCGroups.FiniteGroupClass.{v})
350 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
351 (hG : HasOpenNormalBasisInClass C G)
352 (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
353 (completedGroupAlgebraMapInClass (G := H) (H := K) C hHer R ψ hψ).comp
354 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ) =
355 completedGroupAlgebraMapInClass (G := G) (H := K) C hHer R
356 (ψ.comp φ) (hψ.comp hφ) := by
357 apply completedGroupAlgebraInClassRingHom_ext_of_comp_toCompleted
358 (R := R) (G := G) (H := K) C hForm hG
359 · exact (continuous_completedGroupAlgebraMapInClass (R := R) (G := H) (H := K)
360 C hHer ψ hψ).comp
361 (continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := H)
362 C hHer φ hφ)
363 · exact continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := K)
364 C hHer (ψ.comp φ) (hψ.comp hφ)
365 · apply RingHom.ext
366 intro x
367 have hφdense := congrFun
368 (congrArg DFunLike.coe
369 (completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
370 (R := R) (G := G) (H := H) C hHer φ hφ))
371 x
372 have hψdense := congrFun
373 (congrArg DFunLike.coe
374 (completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
375 (R := R) (G := H) (H := K) C hHer ψ hψ))
376 (MonoidAlgebra.mapDomainRingHom R φ x)
377 have hdomain := congrFun
378 (congrArg DFunLike.coe
379 (finiteGroupAlgebra_mapDomainRingHom_comp R G H K φ ψ))
380 x
381 have hcompdense := congrFun
382 (congrArg DFunLike.coe
383 (completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
384 (R := R) (G := G) (H := K) C hHer (ψ.comp φ) (hψ.comp hφ)))
385 x
386 calc
387 (((completedGroupAlgebraMapInClass (G := H) (H := K) C hHer R ψ hψ).comp
388 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)).comp
389 (toCompletedGroupAlgebraInClassRingHom C R G)) x
390 =
391 completedGroupAlgebraMapInClass (G := H) (H := K) C hHer R ψ hψ
392 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
393 (toCompletedGroupAlgebraInClassRingHom C R G x)) := rfl
394 _ =
395 completedGroupAlgebraMapInClass (G := H) (H := K) C hHer R ψ hψ
396 (toCompletedGroupAlgebraInClassRingHom C R H
397 (MonoidAlgebra.mapDomainRingHom R φ x)) := by
398 have hφdense' :
399 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
400 (toCompletedGroupAlgebraInClassRingHom C R G x) =
401 toCompletedGroupAlgebraInClassRingHom C R H
402 (MonoidAlgebra.mapDomainRingHom R φ x) := by
403 simpa [RingHom.comp_apply] using hφdense
404 exact congrArg (completedGroupAlgebraMapInClass (G := H) (H := K)
405 C hHer R ψ hψ) hφdense'
406 _ =
407 toCompletedGroupAlgebraInClassRingHom C R K
408 (MonoidAlgebra.mapDomainRingHom R ψ (MonoidAlgebra.mapDomainRingHom R φ x)) := by
409 simpa [RingHom.comp_apply] using hψdense
410 _ =
411 toCompletedGroupAlgebraInClassRingHom C R K
412 (MonoidAlgebra.mapDomainRingHom R (ψ.comp φ) x) := by
413 exact congrArg (toCompletedGroupAlgebraInClassRingHom C R K) (by
414 change (MonoidAlgebra.mapDomainRingHom R ψ)
415 ((MonoidAlgebra.mapDomainRingHom R φ) x) =
416 (MonoidAlgebra.mapDomainRingHom R (ψ.comp φ)) x at hdomain
417 exact hdomain)
418 _ =
419 ((completedGroupAlgebraMapInClass (G := G) (H := K) C hHer R
420 (ψ.comp φ) (hψ.comp hφ)).comp
421 (toCompletedGroupAlgebraInClassRingHom C R G)) x := by
422 simpa [RingHom.comp_apply] using hcompdense.symm
424/--
425Composition law for the \(C\)-indexed completed-group-algebra functor, as an \(R\)-algebra
426homomorphism.
427-/
428theorem completedGroupAlgebraMapAlgHomInClass_comp
429 {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
430 (C : ProCGroups.FiniteGroupClass.{v})
433 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
434 (hG : HasOpenNormalBasisInClass C G)
435 (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
436 (completedGroupAlgebraMapAlgHomInClass (G := H) (H := K) C hHer R ψ hψ).comp
437 (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ) =
438 completedGroupAlgebraMapAlgHomInClass (G := G) (H := K) C hHer R
439 (ψ.comp φ) (hψ.comp hφ) := by
440 apply AlgHom.ext
441 intro x
442 have h := congrFun
443 (congrArg DFunLike.coe
444 (completedGroupAlgebraMapInClass_comp (R := R) (G := G) (H := H) (K := K)
445 C hForm hHer hG φ hφ ψ hψ))
446 x
447 simpa using h
449/-- The in-class completed group-algebra map sends group-like elements to group-like elements. -/
450@[simp]
451theorem completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of
452 (C : ProCGroups.FiniteGroupClass.{v})
454 (φ : G →* H) (hφ : Continuous φ) (g : G) :
455 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
456 (toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G g)) =
457 toCompletedGroupAlgebraInClass C R H (MonoidAlgebra.of R H (φ g)) := by
458 have h := congrFun
459 (congrArg DFunLike.coe
460 (completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
461 (R := R) (G := G) (H := H) C hHer φ hφ))
462 (MonoidAlgebra.of R G g)
463 simpa [RingHom.comp_apply, finiteGroupAlgebra_mapDomainRingHom_of] using h
465/--
466The in-class completed group-algebra map sends group-like augmentation generators to their
467images.
468-/
469@[simp]
470theorem completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_sub_one_of
471 (C : ProCGroups.FiniteGroupClass.{v})
473 (φ : G →* H) (hφ : Continuous φ) (g : G) :
474 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
475 (toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G g) - 1) =
476 toCompletedGroupAlgebraInClass C R H (MonoidAlgebra.of R H (φ g)) - 1 := by
477 rw [map_sub, completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of, map_one]
479end
481end CompletedGroupAlgebra