Source: ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Map
1import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap
3/-!
4# Completed Group Algebra / All Finite Functoriality / Map
6This module lifts the functorial finite-stage maps to the named all-finite completed carrier and
7proves their algebraic, topological, and dense-subalgebra characterizations.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
19universe u v w
21variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
22variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
23variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
25/--
26In Lemma 5.3.5(e), map construction, a continuous homomorphism of profinite groups \(\varphi : G
27\to H\) induces a continuous ring homomorphism \(\widehat{R[G]} \to \widehat{R[H]}\).
28-/
29def completedGroupAlgebraMap
30 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
31 (φ : G →* H) (hφ : Continuous φ) :
32 CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraCarrier R H where
33 toFun x :=
34 (completedGroupAlgebraCompatibleFamilyEquiv (R := R) (G := H)).symm
35 ((completedGroupAlgebraSystem R H).inverseLimitLift
36 (fun V x =>
37 completedGroupAlgebraFunctorialStageMap
38 (G := G) (H := H) (R := R) φ hφ V
39 (completedGroupAlgebraProjection R G
40 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x))
41 (by
42 intro V W hVW
43 funext x
44 have hcomp := congrFun
45 (congrArg DFunLike.coe
46 (completedGroupAlgebraFunctorialStageMap_transition
47 (R := R) (G := G) (H := H) φ hφ hVW))
48 (completedGroupAlgebraProjection R G
49 (completedGroupAlgebraComapIndex (G := G) φ hφ W) x)
50 rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
51 simp only [Function.comp_apply]
52 rw [← completedGroupAlgebraProjection_compatible
53 (R := R) (G := G) x
54 (completedGroupAlgebraComapIndex_mono
55 (G := G) φ hφ hVW)]
56 exact hcomp) x)
57 map_zero' := by
58 apply completedGroupAlgebra_ext (R := R) (G := H)
59 intro V
60 exact map_zero (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
61 φ hφ V)
62 map_one' := by
63 apply completedGroupAlgebra_ext (R := R) (G := H)
64 intro V
65 exact map_one (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
66 φ hφ V)
67 map_add' x y := by
68 apply completedGroupAlgebra_ext (R := R) (G := H)
69 intro V
70 exact map_add (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
71 φ hφ V)
72 (completedGroupAlgebraProjection R G
73 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x)
74 (completedGroupAlgebraProjection R G
75 (completedGroupAlgebraComapIndex (G := G) φ hφ V) y)
76 map_mul' x y := by
77 apply completedGroupAlgebra_ext (R := R) (G := H)
78 intro V
79 exact map_mul (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
80 φ hφ V)
81 (completedGroupAlgebraProjection R G
82 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x)
83 (completedGroupAlgebraProjection R G
84 (completedGroupAlgebraComapIndex (G := G) φ hφ V) y)
86/-- Projection of the completed functorial map is computed by the corresponding stage map. -/
87@[simp]
88theorem completedGroupAlgebraProjection_map
89 (φ : G →* H) (hφ : Continuous φ)
90 (V : CompletedGroupAlgebraIndex H) (x : CompletedGroupAlgebraCarrier R G) :
91 completedGroupAlgebraProjection R H V
92 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x) =
93 completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V
94 (completedGroupAlgebraProjection R G
95 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x) :=
96 rfl
98/--
99In Lemma 5.3.5(e), algebra form, a continuous homomorphism of profinite groups induces an
100\(R\)-algebra homomorphism on completed group algebras.
101-/
102def completedGroupAlgebraMapAlgHom
103 (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
104 (φ : G →* H) (hφ : Continuous φ) :
105 CompletedGroupAlgebraCarrier R G →ₐ[R] CompletedGroupAlgebraCarrier R H where
106 toRingHom := completedGroupAlgebraMap (G := G) (H := H) R φ hφ
107 commutes' := by
108 intro r
109 apply completedGroupAlgebra_ext (R := R) (G := H)
110 intro V
111 change completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V
112 (algebraMap R
113 (CompletedGroupAlgebraStage R G
114 (completedGroupAlgebraComapIndex (G := G) φ hφ V)) r) =
115 algebraMap R (CompletedGroupAlgebraStage R H V) r
116 exact completedGroupAlgebraFunctorialStageMap_algebraMap
117 (R := R) (G := G) (H := H) φ hφ V r
119/--
120The algebra homomorphism form of the completed functorial map has the same underlying function
121as the corresponding completed ring homomorphism.
122-/
123@[simp]
124theorem completedGroupAlgebraMapAlgHom_apply
125 (φ : G →* H) (hφ : Continuous φ)
126 (x : CompletedGroupAlgebraCarrier R G) :
127 completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ x =
128 completedGroupAlgebraMap (G := G) (H := H) R φ hφ x :=
129 rfl
131/-- The completed group-algebra map induced by a continuous group homomorphism is continuous. -/
132theorem continuous_completedGroupAlgebraMap
133 (φ : G →* H) (hφ : Continuous φ) :
134 Continuous (completedGroupAlgebraMap (G := G) (H := H) R φ hφ) := by
135 let S := completedGroupAlgebraSystem R H
136 letI : ∀ V, TopologicalSpace (CompletedGroupAlgebraStage R H V) :=
137 fun V => (completedGroupAlgebraSystem R H).topologicalSpace V
138 let π : ∀ V : CompletedGroupAlgebraIndex H,
139 CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraStage R H V :=
140 fun V x =>
141 completedGroupAlgebraFunctorialStageMap
142 (G := G) (H := H) (R := R) φ hφ V
143 (completedGroupAlgebraProjection R G
144 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x)
145 have hπ : ∀ V, Continuous (π V) := by
146 intro V
147 letI : TopologicalSpace
148 (CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) φ hφ V)) :=
149 (completedGroupAlgebraSystem R G).topologicalSpace
150 (completedGroupAlgebraComapIndex (G := G) φ hφ V)
151 exact (continuous_completedGroupAlgebraFunctorialStageMap (R := R) (G := G) (H := H)
152 φ hφ V).comp
153 ((completedGroupAlgebraSystem R G).continuous_projection
154 (completedGroupAlgebraComapIndex (G := G) φ hφ V))
155 have hcompat : S.CompatibleMaps π := by
156 intro V W hVW
157 funext x
158 have hcomp := congrFun
159 (congrArg DFunLike.coe
160 (completedGroupAlgebraFunctorialStageMap_transition
161 (R := R) (G := G) (H := H) φ hφ hVW))
162 (completedGroupAlgebraProjection R G
163 (completedGroupAlgebraComapIndex (G := G) φ hφ W) x)
164 rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
165 simp only [S, π, Function.comp_apply]
166 rw [← completedGroupAlgebraProjection_compatible
167 (R := R) (G := G) x
168 (completedGroupAlgebraComapIndex_mono (G := G) φ hφ hVW)]
169 exact hcomp
170 change Continuous (S.inverseLimitLift π hcompat)
171 exact S.continuous_inverseLimitLift π hπ hcompat
173/--
174The completed functorial map agrees on the dense abstract group algebra with the ordinary
175group-algebra map induced by the group homomorphism.
176-/
177theorem completedGroupAlgebraMap_comp_toCompletedGroupAlgebra
178 (φ : G →* H) (hφ : Continuous φ) :
179 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ).comp
180 (toCompletedGroupAlgebraRingHom R G) =
181 (toCompletedGroupAlgebraRingHom R H).comp (MonoidAlgebra.mapDomainRingHom R φ) := by
182 apply RingHom.ext
183 intro x
184 apply completedGroupAlgebra_ext (R := R) (G := H)
185 intro V
186 have hstage := congrFun
187 (congrArg DFunLike.coe
188 (completedGroupAlgebraFunctorialStageMap_comp_stageMap (R := R) (G := G) (H := H)
189 φ hφ V))
190 x
191 change completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V
192 (completedGroupAlgebraStageMap R G
193 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x) =
194 completedGroupAlgebraStageMap R H V (MonoidAlgebra.mapDomainRingHom R φ x)
195 exact hstage
197end
199end CompletedGroupAlgebra