Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.InClassNaturality
ProCGroups/CompletedGroupAlgebra/AllFiniteFunctoriality/InClassNaturality/Source

Source: ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.InClassNaturality

1import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Map
2import ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Maps
3import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison
5/-!
6# Completed Group Algebra / All Finite Functoriality / Within a Class Naturality
8This module proves that the comparison between the all-finite and \(C\)-indexed completions is
9natural for continuous group homomorphisms, in ring-, algebra-, and equivalence-valued forms.
10-/
12open scoped Topology
14namespace CompletedGroupAlgebra
16noncomputable section
18open ProCGroups
19open ProCGroups.ProC
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/--
28Continuous ring homomorphisms from the all-finite completed group algebra to a \(C\)-indexed
29completed group algebra are determined by their values on the dense abstract group algebra.
30-/
31theorem completedGroupAlgebraRingHomToInClass_ext_of_comp_toCompleted
32 (C : ProCGroups.FiniteGroupClass.{v})
33 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
34 {f g : CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraInClass C R H}
35 (hf : Continuous f) (hg : Continuous g)
36 (hfg : f.comp (toCompletedGroupAlgebraRingHom R G) =
37 g.comp (toCompletedGroupAlgebraRingHom R G)) :
38 f = g := by
39 letI : T2Space (CompletedGroupAlgebraInClass C R H) :=
40 completedGroupAlgebraInClass_t2Space (R := R) (G := H) C
41 have hdense : DenseRange (toCompletedGroupAlgebraRingHom R G) :=
42 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G)
43 have hcomp : (f : CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraInClass C R H) ∘
44 (toCompletedGroupAlgebraRingHom R G) =
45 (g : CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraInClass C R H) ∘
46 (toCompletedGroupAlgebraRingHom R G) := by
47 funext x
48 exact congrFun (congrArg DFunLike.coe hfg) x
49 have hfun : (f : CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraInClass C R H) = g :=
50 DenseRange.equalizer hdense hf hg hcomp
51 exact RingHom.ext fun x => congrFun hfun x
53/--
54Naturality of the comparison from the all-finite completed group algebra to the \(C\)-indexed
55completed group algebra in the group variable.
56-/
57theorem completedGroupAlgebraToInClassRingHom_naturality
58 (C : ProCGroups.FiniteGroupClass.{v})
60 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
61 (φ : G →* H) (hφ : Continuous φ) :
62 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ).comp
63 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) =
64 (completedGroupAlgebraToInClassRingHom (R := R) (G := H) C ).comp
65 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ) := by
66 apply completedGroupAlgebraRingHomToInClass_ext_of_comp_toCompleted
67 (R := R) (G := G) (H := H) C
68 · exact (continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := H)
69 C hHer φ hφ).comp
70 (continuous_completedGroupAlgebraToInClass (R := R) (G := G) C )
71 · exact (continuous_completedGroupAlgebraToInClass (R := R) (G := H) C ).comp
72 (continuous_completedGroupAlgebraMap (R := R) (G := G) (H := H) φ hφ)
73 · apply RingHom.ext
74 intro x
75 have htoG := congrFun
76 (congrArg DFunLike.coe
77 (completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
78 (R := R) (G := G) C ))
79 x
80 have hmapC := congrFun
81 (congrArg DFunLike.coe
82 (completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
83 (R := R) (G := G) (H := H) C hHer φ hφ))
84 x
85 have hmapAll := congrFun
86 (congrArg DFunLike.coe
87 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra
88 (R := R) (G := G) (H := H) φ hφ))
89 x
90 have htoH := congrFun
91 (congrArg DFunLike.coe
92 (completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
93 (R := R) (G := H) C ))
94 (MonoidAlgebra.mapDomainRingHom R φ x)
95 calc
96 ((((completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ).comp
97 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )).comp
98 (toCompletedGroupAlgebraRingHom R G)) x) =
99 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
100 ((completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
101 (toCompletedGroupAlgebraRingHom R G x)) := rfl
102 _ =
103 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
104 (toCompletedGroupAlgebraInClassRingHom C R G x) := by
105 exact congrArg (completedGroupAlgebraMapInClass (G := G) (H := H)
106 C hHer R φ hφ) (by
107 exact htoG)
108 _ =
109 toCompletedGroupAlgebraInClassRingHom C R H
110 (MonoidAlgebra.mapDomainRingHom R φ x) := by
111 simpa [RingHom.comp_apply] using hmapC
112 _ =
113 completedGroupAlgebraToInClassRingHom (R := R) (G := H) C
114 (toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x)) := by
115 have htoH' :
116 completedGroupAlgebraToInClassRingHom (R := R) (G := H) C
117 (toCompletedGroupAlgebraRingHom R H
118 (MonoidAlgebra.mapDomainRingHom R φ x)) =
119 toCompletedGroupAlgebraInClassRingHom C R H
120 (MonoidAlgebra.mapDomainRingHom R φ x) := by
121 exact htoH
122 exact htoH'.symm
123 _ =
124 completedGroupAlgebraToInClassRingHom (R := R) (G := H) C
125 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ
126 (toCompletedGroupAlgebraRingHom R G x)) := by
127 have hmapAll' :
128 completedGroupAlgebraMap (G := G) (H := H) R φ hφ
129 (toCompletedGroupAlgebraRingHom R G x) =
130 toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x) := by
131 exact hmapAll
132 exact congrArg (completedGroupAlgebraToInClassRingHom (R := R) (G := H) C )
133 hmapAll'.symm
134 _ =
135 ((((completedGroupAlgebraToInClassRingHom (R := R) (G := H) C ).comp
136 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)).comp
137 (toCompletedGroupAlgebraRingHom R G)) x) := rfl
139/--
140Algebra-homomorphism form of the naturality of the comparison from the all-finite completed
141group algebra to the \(C\)-indexed completed group algebra.
142-/
143theorem completedGroupAlgebraToInClassAlgHom_naturality
144 (C : ProCGroups.FiniteGroupClass.{v})
146 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
147 (φ : G →* H) (hφ : Continuous φ) :
148 (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ).comp
149 (completedGroupAlgebraToInClassAlgHom (R := R) (G := G) C ) =
150 (completedGroupAlgebraToInClassAlgHom (R := R) (G := H) C ).comp
151 (completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ) := by
152 apply AlgHom.ext
153 intro x
154 have h := congrFun
155 (congrArg DFunLike.coe
156 (completedGroupAlgebraToInClassRingHom_naturality
157 (R := R) (G := G) (H := H) C hHer φ hφ))
158 x
159 simpa using h
161/--
162Naturality of the inverse comparison from the \(C\)-indexed completed group algebra back to the
163all-finite completed group algebra, for pro-\(C\) groups.
164-/
165theorem completedGroupAlgebraFromInClassRingHom_naturality
166 (C : ProCGroups.FiniteGroupClass.{v})
169 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
170 (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
171 (φ : G →* H) (hφ : Continuous φ) :
172 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ).comp
173 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG) =
174 (completedGroupAlgebraFromInClassRingHom (R := R) (G := H) C hForm hH).comp
175 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ) := by
176 apply RingHom.ext
177 intro x
178 rcases completedGroupAlgebraToInClass_surjective (R := R) (G := G) C hForm hG x with
179 ⟨y, rfl⟩
180 have hnat := congrFun
181 (congrArg DFunLike.coe
182 (completedGroupAlgebraToInClassRingHom_naturality
183 (R := R) (G := G) (H := H) C hHer φ hφ))
184 y
185 calc
186 ((completedGroupAlgebraMap (G := G) (H := H) R φ hφ).comp
187 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG))
188 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C y)
189 =
190 completedGroupAlgebraMap (G := G) (H := H) R φ hφ
191 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
192 (completedGroupAlgebraToInClass (R := R) (G := G) C y)) := rfl
193 _ =
194 completedGroupAlgebraMap (G := G) (H := H) R φ hφ y := by
195 rw [completedGroupAlgebraFromInClass_toInClass]
196 _ =
197 completedGroupAlgebraFromInClass (R := R) (G := H) C hForm hH
198 (completedGroupAlgebraToInClass (R := R) (G := H) C
199 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ y)) := by
200 rw [completedGroupAlgebraFromInClass_toInClass]
201 _ =
202 completedGroupAlgebraFromInClass (R := R) (G := H) C hForm hH
203 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
204 (completedGroupAlgebraToInClass (R := R) (G := G) C y)) := by
205 exact congrArg (completedGroupAlgebraFromInClass (R := R) (G := H) C hForm hH)
206 hnat.symm
207 _ =
208 ((completedGroupAlgebraFromInClassRingHom (R := R) (G := H) C hForm hH).comp
209 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ))
210 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C y) := rfl
212/--
213Algebra-homomorphism form of the naturality of the inverse comparison from the \(C\)-indexed
214completed group algebra back to the all-finite completed group algebra.
215-/
216theorem completedGroupAlgebraFromInClassAlgHom_naturality
217 (C : ProCGroups.FiniteGroupClass.{v})
220 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
221 (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
222 (φ : G →* H) (hφ : Continuous φ) :
223 (completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ).comp
224 (completedGroupAlgebraFromInClassAlgHom (R := R) (G := G) C hForm hG) =
225 (completedGroupAlgebraFromInClassAlgHom (R := R) (G := H) C hForm hH).comp
226 (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ) := by
227 apply AlgHom.ext
228 intro x
229 have h := congrFun
230 (congrArg DFunLike.coe
231 (completedGroupAlgebraFromInClassRingHom_naturality
232 (R := R) (G := G) (H := H) C hHer hForm hG hH φ hφ))
233 x
234 simpa using h
236/-- The ring equivalence from all-finite to in-class completions is natural in the group. -/
237@[simp]
238theorem completedGroupAlgebraInClassRingEquiv_naturality
239 (C : ProCGroups.FiniteGroupClass.{v})
242 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
243 (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
244 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraCarrier R G) :
245 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
246 (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG x) =
247 completedGroupAlgebraInClassRingEquiv (R := R) (G := H) C hForm hH
248 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x) := by
249 have h := congrFun
250 (congrArg DFunLike.coe
251 (completedGroupAlgebraToInClassRingHom_naturality
252 (R := R) (G := G) (H := H) C hHer φ hφ))
253 x
254 simpa [RingHom.comp_apply] using h
256/-- The inverse ring equivalence from in-class to all-finite completions is natural in the group. -/
257@[simp]
258theorem completedGroupAlgebraInClassRingEquiv_symm_naturality
259 (C : ProCGroups.FiniteGroupClass.{v})
262 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
263 (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
264 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
265 completedGroupAlgebraMap (G := G) (H := H) R φ hφ
266 ((completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG).symm x) =
267 (completedGroupAlgebraInClassRingEquiv (R := R) (G := H) C hForm hH).symm
268 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x) := by
269 have h := congrFun
270 (congrArg DFunLike.coe
271 (completedGroupAlgebraFromInClassRingHom_naturality
272 (R := R) (G := G) (H := H) C hHer hForm hG hH φ hφ))
273 x
274 simpa [RingHom.comp_apply] using h
276/-- The algebra equivalence from all-finite to in-class completions is natural in the group. -/
277@[simp]
278theorem completedGroupAlgebraInClassAlgEquiv_naturality
279 (C : ProCGroups.FiniteGroupClass.{v})
282 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
283 (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
284 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraCarrier R G) :
285 completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ
286 (completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG x) =
287 completedGroupAlgebraInClassAlgEquiv (R := R) (G := H) C hForm hH
288 (completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ x) := by
289 have h := congrFun
290 (congrArg DFunLike.coe
291 (completedGroupAlgebraToInClassAlgHom_naturality
292 (R := R) (G := G) (H := H) C hHer φ hφ))
293 x
294 simpa using h
296/--
297The inverse algebra equivalence from in-class to all-finite completions is natural in the group.
298-/
299@[simp]
300theorem completedGroupAlgebraInClassAlgEquiv_symm_naturality
301 (C : ProCGroups.FiniteGroupClass.{v})
304 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
305 (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
306 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
307 completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ
308 ((completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG).symm x) =
309 (completedGroupAlgebraInClassAlgEquiv (R := R) (G := H) C hForm hH).symm
310 (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ x) := by
311 have h := congrFun
312 (congrArg DFunLike.coe
313 (completedGroupAlgebraFromInClassAlgHom_naturality
314 (R := R) (G := G) (H := H) C hHer hForm hG hH φ hφ))
315 x
316 simpa using h
318end
320end CompletedGroupAlgebra