CompletedGroupAlgebra/AllFiniteFunctoriality/GroupLike.lean
1import CompletedGroupAlgebra.AllFiniteFunctoriality.Map
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/AllFiniteFunctoriality/GroupLike.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Group-like formulas for completed group algebra functoriality
13-/
15open scoped Topology
17namespace CompletedGroupAlgebra
19noncomputable section
21open ProCGroups
22open ProCGroups.ProC
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/-- The completed functorial map sends the group-like element of `g` to that of `φ g`. -/
31theorem completedGroupAlgebraMap_of
32 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) (g : G) :
33 completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ (completedGroupAlgebraOf R G g) =
34 completedGroupAlgebraOf R H (φ g) := by
35 have h := congrFun
36 (congrArg DFunLike.coe
37 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := G) (H := H)
38 hG φ hφ))
39 (MonoidAlgebra.of R G g)
40 simpa [completedGroupAlgebraOf, finiteGroupAlgebra_mapDomainRingHom_of] using h
42/-- The algebra-hom completed functorial map sends group-like elements to their images. -/
43@[simp]
45 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) (g : G) :
46 completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG φ hφ
47 (completedGroupAlgebraOf R G g) =
48 completedGroupAlgebraOf R H (φ g) :=
49 completedGroupAlgebraMap_of (R := R) (G := G) (H := H) hG φ hφ g
50end