CompletedGroupAlgebra/FunctorialityComposition.lean
1import CompletedGroupAlgebra.Separation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/FunctorialityComposition.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
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]
33variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
35/-- Lemma 5.3.5(e), composition law for the completed-group-algebra functor. -/
36theorem completedGroupAlgebraMap_comp
37 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
38 (hH : ProCGroups.IsProfiniteGroup H)
39 (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
40 (completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ).comp
41 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ) =
42 completedGroupAlgebraMap (G := G) (H := K) R hG (ψ.comp φ) (hψ.comp hφ) := by
43 apply completedGroupAlgebraRingHom_ext_of_comp_toCompleted (R := R) (G := G) (H := K)
44 hR hG
45 · exact (continuous_completedGroupAlgebraMap (R := R) (G := H) (H := K) hH ψ hψ).comp
46 (continuous_completedGroupAlgebraMap (R := R) (G := G) (H := H) hG φ hφ)
47 · exact continuous_completedGroupAlgebraMap (R := R) (G := G) (H := K)
48 hG (ψ.comp φ) (hψ.comp hφ)
49 · apply RingHom.ext
50 intro x
51 have hφdense := congrFun
52 (congrArg DFunLike.coe
53 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := G) (H := H)
54 hG φ hφ))
55 x
56 have hψdense := congrFun
57 (congrArg DFunLike.coe
58 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := H) (H := K)
59 hH ψ hψ))
60 (MonoidAlgebra.mapDomainRingHom R φ x)
61 have hdomain := congrFun
62 (congrArg DFunLike.coe
63 (finiteGroupAlgebra_mapDomainRingHom_comp R G H K φ ψ))
64 x
65 have hcompdense := congrFun
66 (congrArg DFunLike.coe
67 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := G) (H := K)
68 hG (ψ.comp φ) (hψ.comp hφ)))
69 x
70 calc
71 (((completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ).comp
72 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)).comp
73 (toCompletedGroupAlgebraRingHom R G)) x
74 =
75 completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ
76 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
77 (toCompletedGroupAlgebraRingHom R G x)) := rfl
78 _ =
79 completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ
80 (toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x)) := by
81 have hφdense' :
82 completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
83 (toCompletedGroupAlgebraRingHom R G x) =
84 toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x) := by
85 simpa [RingHom.comp_apply] using hφdense
86 exact congrArg (completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ) hφdense'
87 _ =
89 (MonoidAlgebra.mapDomainRingHom R ψ (MonoidAlgebra.mapDomainRingHom R φ x)) := by
90 simpa [RingHom.comp_apply] using hψdense
91 _ =
93 (MonoidAlgebra.mapDomainRingHom R (ψ.comp φ) x) := by
94 exact congrArg (toCompletedGroupAlgebraRingHom R K) (by
95 change (MonoidAlgebra.mapDomainRingHom R ψ)
96 ((MonoidAlgebra.mapDomainRingHom R φ) x) =
97 (MonoidAlgebra.mapDomainRingHom R (ψ.comp φ)) x at hdomain
98 exact hdomain)
99 _ =
100 ((completedGroupAlgebraMap (G := G) (H := K) R hG (ψ.comp φ) (hψ.comp hφ)).comp
101 (toCompletedGroupAlgebraRingHom R G)) x := by
102 simpa [RingHom.comp_apply] using hcompdense.symm
104/-- Lemma 5.3.5(e), composition law for the completed-group-algebra functor, as an `R`-algebra
105homomorphism. -/
107 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
108 (hH : ProCGroups.IsProfiniteGroup H)
109 (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
110 (completedGroupAlgebraMapAlgHom (G := H) (H := K) R hH ψ hψ).comp
111 (completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG φ hφ) =
112 completedGroupAlgebraMapAlgHom (G := G) (H := K) R hG (ψ.comp φ) (hψ.comp hφ) := by
113 apply AlgHom.ext
114 intro x
115 have h := congrFun
116 (congrArg DFunLike.coe
117 (completedGroupAlgebraMap_comp (R := R) (G := G) (H := H) (K := K)
118 hR hG hH φ hφ ψ hψ))
119 x
120 simpa [RingHom.comp_apply] using h
121end