CompletedGroupAlgebra/AllFiniteFunctoriality/InClassNaturality.lean
1import CompletedGroupAlgebra.AllFiniteFunctoriality.Map
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/AllFiniteFunctoriality/InClassNaturality.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# In-class comparison naturality for all-finite 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/-- Continuous ring homomorphisms from the all-finite completed group algebra to a `C`-indexed
31completed group algebra are determined by their values on the dense abstract group algebra. -/
33 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
34 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
35 {f g : Carrier R G →+* CompletedGroupAlgebraInClass C hC R H}
36 (hf : Continuous f) (hg : Continuous g)
37 (hfg : f.comp (toCompletedGroupAlgebraRingHom R G) =
38 g.comp (toCompletedGroupAlgebraRingHom R G)) :
39 f = g := by
40 letI : T2Space (CompletedGroupAlgebraInClass C hC R H) :=
41 completedGroupAlgebraInClass_t2Space (R := R) (G := H) C hC hR
42 have hdense : DenseRange (toCompletedGroupAlgebraRingHom R G) :=
43 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG
44 have hcomp : (f : Carrier R G → CompletedGroupAlgebraInClass C hC R H) ∘
45 (toCompletedGroupAlgebraRingHom R G) =
46 (g : Carrier R G → CompletedGroupAlgebraInClass C hC R H) ∘
47 (toCompletedGroupAlgebraRingHom R G) := by
48 funext x
49 exact congrFun (congrArg DFunLike.coe hfg) x
50 have hfun : (f : Carrier R G → CompletedGroupAlgebraInClass C hC R H) = g :=
51 DenseRange.equalizer hdense hf hg hcomp
52 exact RingHom.ext fun x => congrFun hfun x
54/-- Naturality of the comparison from the all-finite completed group algebra to the `C`-indexed
55completed group algebra in the group variable. -/
57 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
58 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
59 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
60 (φ : G →* H) (hφ : Continuous φ) :
61 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ).comp
62 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) =
63 (completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC).comp
64 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ) := by
66 (R := R) (G := G) (H := H) C hC hR hG
67 · exact (continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := H)
68 C hC hHer φ hφ).comp
69 (continuous_completedGroupAlgebraToInClass (R := R) (G := G) C hC)
70 · exact (continuous_completedGroupAlgebraToInClass (R := R) (G := H) C hC).comp
71 (continuous_completedGroupAlgebraMap (R := R) (G := G) (H := H) hG φ hφ)
72 · apply RingHom.ext
73 intro x
74 have htoG := congrFun
75 (congrArg DFunLike.coe
77 (R := R) (G := G) C hC))
78 x
79 have hmapC := congrFun
80 (congrArg DFunLike.coe
82 (R := R) (G := G) (H := H) C hC hHer φ hφ))
83 x
84 have hmapAll := congrFun
85 (congrArg DFunLike.coe
87 (R := R) (G := G) (H := H) hG φ hφ))
88 x
89 have htoH := congrFun
90 (congrArg DFunLike.coe
92 (R := R) (G := H) C hC))
93 (MonoidAlgebra.mapDomainRingHom R φ x)
94 calc
95 ((((completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ).comp
96 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)).comp
97 (toCompletedGroupAlgebraRingHom R G)) x) =
98 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
99 ((completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
100 (toCompletedGroupAlgebraRingHom R G x)) := rfl
101 _ =
102 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
103 (toCompletedGroupAlgebraInClassRingHom C hC R G x) := by
104 exact congrArg (completedGroupAlgebraMapInClass (G := G) (H := H)
105 C hC hHer R φ hφ) (by
106 exact htoG)
107 _ =
108 toCompletedGroupAlgebraInClassRingHom C hC R H
109 (MonoidAlgebra.mapDomainRingHom R φ x) := by
110 simpa [RingHom.comp_apply] using hmapC
111 _ =
112 completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC
113 (toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x)) := by
114 have htoH' :
115 completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC
117 (MonoidAlgebra.mapDomainRingHom R φ x)) =
118 toCompletedGroupAlgebraInClassRingHom C hC R H
119 (MonoidAlgebra.mapDomainRingHom R φ x) := by
120 exact htoH
121 exact htoH'.symm
122 _ =
123 completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC
124 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
125 (toCompletedGroupAlgebraRingHom R G x)) := by
126 have hmapAll' :
127 completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
128 (toCompletedGroupAlgebraRingHom R G x) =
129 toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x) := by
130 exact hmapAll
131 exact congrArg (completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC)
132 hmapAll'.symm
133 _ =
134 ((((completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC).comp
135 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)).comp
136 (toCompletedGroupAlgebraRingHom R G)) x) := rfl
138/-- Algebra-hom form of the naturality of the comparison from the all-finite completed group
139algebra to the `C`-indexed completed group algebra. -/
141 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
142 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
143 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
144 (φ : G →* H) (hφ : Continuous φ) :
145 (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ).comp
146 (completedGroupAlgebraToInClassAlgHom (R := R) (G := G) C hC) =
147 (completedGroupAlgebraToInClassAlgHom (R := R) (G := H) C hC).comp
148 (completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG φ hφ) := by
149 apply AlgHom.ext
150 intro x
151 have h := congrFun
152 (congrArg DFunLike.coe
154 (R := R) (G := G) (H := H) C hC hHer hR hG φ hφ))
155 x
156 simpa using h
158/-- Naturality of the inverse comparison from the `C`-indexed completed group algebra back to the
161 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
162 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
163 (hForm : ProCGroups.FiniteGroupClass.Formation C)
164 (hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
165 (φ : G →* H) (hφ : Continuous φ) :
166 (completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ).comp
167 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG) =
168 (completedGroupAlgebraFromInClassRingHom (R := R) (G := H) C hC hForm hH).comp
169 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ) := by
170 apply RingHom.ext
171 intro x
172 rcases completedGroupAlgebraToInClass_surjective (R := R) (G := G) C hC hForm hG x with
173 ⟨y, rfl⟩
174 have hnat := congrFun
175 (congrArg DFunLike.coe
177 (R := R) (G := G) (H := H) C hC hHer hR hG.1 φ hφ))
178 y
179 calc
180 ((completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ).comp
181 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG))
182 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC y)
183 =
184 completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ
185 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
186 (completedGroupAlgebraToInClass (R := R) (G := G) C hC y)) := rfl
187 _ =
188 completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ y := by
190 _ =
191 completedGroupAlgebraFromInClass (R := R) (G := H) C hC hForm hH
192 (completedGroupAlgebraToInClass (R := R) (G := H) C hC
193 (completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ y)) := by
195 _ =
196 completedGroupAlgebraFromInClass (R := R) (G := H) C hC hForm hH
197 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
198 (completedGroupAlgebraToInClass (R := R) (G := G) C hC y)) := by
199 exact congrArg (completedGroupAlgebraFromInClass (R := R) (G := H) C hC hForm hH)
200 hnat.symm
201 _ =
202 ((completedGroupAlgebraFromInClassRingHom (R := R) (G := H) C hC hForm hH).comp
203 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ))
204 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC y) := rfl
206/-- Algebra-hom form of the naturality of the inverse comparison from the `C`-indexed completed
209 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
210 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
211 (hForm : ProCGroups.FiniteGroupClass.Formation C)
212 (hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
213 (φ : G →* H) (hφ : Continuous φ) :
214 (completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG.1 φ hφ).comp
215 (completedGroupAlgebraFromInClassAlgHom (R := R) (G := G) C hC hForm hG) =
216 (completedGroupAlgebraFromInClassAlgHom (R := R) (G := H) C hC hForm hH).comp
217 (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ) := by
218 apply AlgHom.ext
219 intro x
220 have h := congrFun
221 (congrArg DFunLike.coe
223 (R := R) (G := G) (H := H) C hC hHer hForm hR hG hH φ hφ))
224 x
225 simpa using h
227/-- The ring equivalence from all-finite to in-class completions is natural in the group. -/
228@[simp]
230 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
231 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
232 (hForm : ProCGroups.FiniteGroupClass.Formation C)
233 (hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
234 (φ : G →* H) (hφ : Continuous φ) (x : Carrier R G) :
235 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
236 (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG x) =
237 completedGroupAlgebraInClassRingEquiv (R := R) (G := H) C hC hForm hH
238 (completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ x) := by
239 have h := congrFun
240 (congrArg DFunLike.coe
242 (R := R) (G := G) (H := H) C hC hHer hR hG.1 φ hφ))
243 x
244 simpa [RingHom.comp_apply] using h
246/-- The inverse ring equivalence from in-class to all-finite completions is natural in the group. -/
247@[simp]
249 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
250 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
251 (hForm : ProCGroups.FiniteGroupClass.Formation C)
252 (hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
253 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C hC R G) :
254 completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ
255 ((completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG).symm x) =
256 (completedGroupAlgebraInClassRingEquiv (R := R) (G := H) C hC hForm hH).symm
257 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x) := by
258 have h := congrFun
259 (congrArg DFunLike.coe
261 (R := R) (G := G) (H := H) C hC hHer hForm hR hG hH φ hφ))
262 x
263 simpa [RingHom.comp_apply] using h
265/-- The algebra equivalence from all-finite to in-class completions is natural in the group. -/
266@[simp]
268 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
269 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
270 (hForm : ProCGroups.FiniteGroupClass.Formation C)
271 (hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
272 (φ : G →* H) (hφ : Continuous φ) (x : Carrier R G) :
273 completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ
274 (completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hC hForm hG x) =
275 completedGroupAlgebraInClassAlgEquiv (R := R) (G := H) C hC hForm hH
276 (completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG.1 φ hφ x) := by
277 have h := congrFun
278 (congrArg DFunLike.coe
280 (R := R) (G := G) (H := H) C hC hHer hR hG.1 φ hφ))
281 x
282 simpa using h
284/-- The inverse algebra equivalence from in-class to all-finite completions is natural in the group. -/
285@[simp]
287 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
288 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
289 (hForm : ProCGroups.FiniteGroupClass.Formation C)
290 (hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
291 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C hC R G) :
292 completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG.1 φ hφ
293 ((completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hC hForm hG).symm x) =
294 (completedGroupAlgebraInClassAlgEquiv (R := R) (G := H) C hC hForm hH).symm
295 (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ x) := by
296 have h := congrFun
297 (congrArg DFunLike.coe
299 (R := R) (G := G) (H := H) C hC hHer hForm hR hG hH φ hφ))
300 x
301 simpa using h
303end