Yamaguchi Lean 4 Library
CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Topology.lean
CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Topology/Source

CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Topology.lean

1import CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals
2import Mathlib.GroupTheory.FiniteAbelian.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Topology.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Finite group algebra topology and free-module structure
15This module equips finite group algebras with the finite product topology and records the coordinate continuity used for continuous-linear extension arguments.
16-/
18open scoped Topology
19open ProCGroups
23universe u v w z
25/-- A completed-group-algebra model consists of a profinite coefficient ring, a profinite group,
26a profinite topological ring carrier, and a dense algebraic group-algebra map from a chosen
27topology on `R[G]`. -/
28structure IsCompletedGroupAlgebraModel (R : Type u) (G : Type v) (RG : Type w)
29 [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [Ring RG]
30 [TopologicalSpace RG] : Prop where
31 (coefficient_isProfiniteRing : IsProfiniteRing R)
32 (group_isProfiniteGroup : IsProfiniteGroup G)
33 (carrier_isProfiniteRing : IsProfiniteRing RG)
34 (dense_algebraicMap :
35 ∃ τ : TopologicalSpace (MonoidAlgebra R G),
36 letI := τ
37 ∃ dense : MonoidAlgebra R G →+* RG, DenseRange dense ∧ Continuous dense)
39/-- The product topology on the group algebra of a finite group, transported through
40`R[G] = G →₀ R ≃ G → R`. This is the finite stage used in the construction of the completed
41group algebra. -/
43 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R] :
44 TopologicalSpace (MonoidAlgebra R G) :=
45 TopologicalSpace.induced (Finsupp.equivFunOnFinite : MonoidAlgebra R G ≃ (G → R))
46 inferInstance
48/-- The finite group algebra with its transported product topology is homeomorphic to `G → R`. -/
50 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R] :
51 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
52 MonoidAlgebra R G ≃ₜ (G → R) := by
53 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
54 let e : MonoidAlgebra R G ≃ (G → R) := Finsupp.equivFunOnFinite
55 have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
56 Topology.IsInducing.induced e
57 exact e.toHomeomorphOfIsInducing he
59/-- The finite-stage group algebra is the finite product of copies of the coefficient ring as a
60topological `R`-module. -/
62 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R] :
63 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
64 MonoidAlgebra R G ≃L[R] (G → R) := by
65 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
66 let e : MonoidAlgebra R G ≃ (G → R) := Finsupp.equivFunOnFinite
67 have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
68 Topology.IsInducing.induced e
69 exact ContinuousLinearEquiv.mk
70 (Finsupp.linearEquivFunOnFinite R R G)
71 (by
72 change Continuous (e : MonoidAlgebra R G → G → R)
73 exact he.continuous)
74 (by
75 change Continuous ((e.toHomeomorphOfIsInducing he).symm : (G → R) → MonoidAlgebra R G)
76 exact (e.toHomeomorphOfIsInducing he).symm.continuous)
78@[simp]
80 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
81 (x : MonoidAlgebra R G) :
82 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
83 finiteGroupAlgebraContinuousLinearEquivPi R G x = Finsupp.equivFunOnFinite x :=
84 rfl
86/-- Coordinate evaluation on a finite group algebra is continuous for the transported product
87topology. -/
89 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R] :
90 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
91 ∀ g : G, Continuous fun x : MonoidAlgebra R G => x g := by
92 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
93 let e : MonoidAlgebra R G ≃ (G → R) := Finsupp.equivFunOnFinite
94 intro g
95 simpa [e] using
96 (continuous_apply g).comp (continuous_induced_dom : Continuous (e : MonoidAlgebra R G → G → R))
98/-- Addition is continuous for the finite-stage group algebra topology. -/
100 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
101 [IsTopologicalRing R] :
102 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
103 ContinuousAdd (MonoidAlgebra R G) := by
104 classical
105 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
106 let A := MonoidAlgebra R G
107 let e : A ≃ (G → R) := Finsupp.equivFunOnFinite
108 have he : Topology.IsInducing (e : A → G → R) := Topology.IsInducing.induced e
109 have hcoord : ∀ g : G, Continuous fun x : A => x g :=
111 refine ⟨?_⟩
112 rw [he.continuous_iff]
113 apply continuous_pi
114 intro g
115 change Continuous fun p : A × A => (p.1 + p.2) g
116 simpa using ((hcoord g).comp continuous_fst).add ((hcoord g).comp continuous_snd)
118/-- Negation is continuous for the finite-stage group algebra topology. -/
120 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
121 [IsTopologicalRing R] :
122 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
123 ContinuousNeg (MonoidAlgebra R G) := by
124 classical
125 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
126 let A := MonoidAlgebra R G
127 let e : A ≃ (G → R) := Finsupp.equivFunOnFinite
128 have he : Topology.IsInducing (e : A → G → R) := Topology.IsInducing.induced e
129 have hcoord : ∀ g : G, Continuous fun x : A => x g :=
131 refine ⟨?_⟩
132 rw [he.continuous_iff]
133 apply continuous_pi
134 intro g
135 change Continuous fun x : A => (-x) g
136 simpa using (hcoord g).neg
138/-- Multiplication is continuous for the finite-stage group algebra topology. The coordinate
139formula is the finite convolution sum over pairs `(g₁,g₂)` with `g₁*g₂ = g`. -/
141 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
142 [IsTopologicalRing R] :
143 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
144 ContinuousMul (MonoidAlgebra R G) := by
145 classical
146 letI : Fintype G := Fintype.ofFinite G
147 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
148 let A := MonoidAlgebra R G
149 let e : A ≃ (G → R) := Finsupp.equivFunOnFinite
150 have he : Topology.IsInducing (e : A → G → R) := Topology.IsInducing.induced e
151 have hcoord : ∀ g : G, Continuous fun x : A => x g :=
153 refine ⟨?_⟩
154 rw [he.continuous_iff]
155 apply continuous_pi
156 intro g
157 change Continuous fun p : A × A => (p.1 * p.2) g
158 rw [show (fun p : A × A => (p.1 * p.2) g) =
159 (fun p : A × A => ∑ q ∈ (Finset.univ.filter (fun q : G × G => q.1 * q.2 = g)),
160 p.1 q.1 * p.2 q.2) from ?_]
161 · apply continuous_finset_sum
162 intro q _hq
163 exact ((hcoord q.1).comp continuous_fst).mul ((hcoord q.2).comp continuous_snd)
164 · funext p
165 exact MonoidAlgebra.mul_apply_antidiagonal p.1 p.2 g
166 (Finset.univ.filter (fun q : G × G => q.1 * q.2 = g)) (by intro q; simp only [Finset.mem_filter, Finset.mem_univ, true_and])
168/-- Scalar multiplication by the coefficient ring is continuous on the finite-stage group
169algebra topology. -/
171 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
172 [IsTopologicalRing R] :
173 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
174 ContinuousSMul R (MonoidAlgebra R G) := by
175 classical
176 letI : Fintype G := Fintype.ofFinite G
177 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
178 let A := MonoidAlgebra R G
179 let e : A ≃ (G → R) := Finsupp.equivFunOnFinite
180 have he : Topology.IsInducing (e : A → G → R) := Topology.IsInducing.induced e
181 have hcoord : ∀ g : G, Continuous fun x : A => x g :=
183 refine ContinuousSMul.mk ?_
184 rw [he.continuous_iff]
185 apply continuous_pi
186 intro g
187 change Continuous fun p : R × A => p.1 * p.2 g
188 exact continuous_fst.mul ((hcoord g).comp continuous_snd)
190/-- The finite-stage group algebra topology makes `R[G]` a topological ring. -/
192 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
193 [IsTopologicalRing R] :
194 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
195 IsTopologicalRing (MonoidAlgebra R G) := by
196 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
197 letI : ContinuousAdd (MonoidAlgebra R G) := finiteGroupAlgebra_continuousAdd R G
198 letI : ContinuousMul (MonoidAlgebra R G) := finiteGroupAlgebra_continuousMul R G
199 letI : ContinuousNeg (MonoidAlgebra R G) := finiteGroupAlgebra_continuousNeg R G
200 letI : IsTopologicalSemiring (MonoidAlgebra R G) := IsTopologicalSemiring.mk
201 exact IsTopologicalRing.mk
203/-- The finite-stage group algebra of a profinite coefficient ring over a finite group is
204profinite. -/
206 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
207 (hR : IsProfiniteRing R) :
208 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
209 IsProfiniteRing (MonoidAlgebra R G) := by
210 letI : IsTopologicalRing R := hR.1
211 letI : CompactSpace R := hR.2.1
212 letI : T2Space R := hR.2.2.1
213 letI : TotallyDisconnectedSpace R := hR.2.2.2
214 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
216 letI : IsTopologicalRing (MonoidAlgebra R G) := finiteGroupAlgebra_isTopologicalRing R G
217 letI : CompactSpace (MonoidAlgebra R G) := Homeomorph.compactSpace e.symm
218 letI : T2Space (MonoidAlgebra R G) := Homeomorph.t2Space e.symm
219 letI : TotallyDisconnectedSpace (MonoidAlgebra R G) :=
220 Homeomorph.totallyDisconnectedSpace e.symm
221 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
223/-- The finite-stage group algebra of a profinite coefficient ring over a finite group is a
224profinite module over the coefficient ring. -/
226 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
227 (hR : IsProfiniteRing R) :
228 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
229 IsProfiniteModule R (MonoidAlgebra R G) := by
230 letI : IsTopologicalRing R := hR.1
231 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
232 letI : IsTopologicalRing (MonoidAlgebra R G) := finiteGroupAlgebra_isTopologicalRing R G
233 letI : IsTopologicalAddGroup (MonoidAlgebra R G) := inferInstance
234 letI : ContinuousSMul R (MonoidAlgebra R G) := finiteGroupAlgebra_continuousSMul R G
235 have hA : IsProfiniteRing (MonoidAlgebra R G) := finiteGroupAlgebra_isProfiniteRing R G hR
236 exact ⟨hR, inferInstance, inferInstance, hA.2.1, hA.2.2.1, hA.2.2.2⟩
238private noncomputable def finiteGroupAlgebraPiLift
239 (R : Type u) (G : Type v) (N : Type w)
240 [Ring R] [TopologicalSpace R] [Fintype G]
241 [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousSMul R N]
242 (f : G -> N) : (G -> R) →L[R] N where
243 toLinearMap :=
244 { toFun := fun m => ∑ x : G, m x • f x
245 map_add' := by
246 intro m n
247 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
248 map_smul' := by
249 intro lam m
250 simp only [Pi.smul_apply, smul_eq_mul, mul_smul, RingHom.id_apply, Finset.smul_sum]}
251 cont := by
252 apply continuous_finset_sum
253 intro x _hx
254 exact (continuous_apply x).smul continuous_const
257 (R : Type u) (G : Type v) (N : Type w)
258 [Ring R] [TopologicalSpace R] [Fintype G] [DecidableEq G]
259 [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousSMul R N]
260 (f : G -> N) (g : G) :
261 finiteGroupAlgebraPiLift R G N f (Pi.single g (1 : R)) = f g := by
262 simp only [finiteGroupAlgebraPiLift, ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk,
263 Pi.single_apply, ite_smul, one_smul, zero_smul, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte]
265/-- The continuous linear map out of a finite group algebra determined by the values on group
266elements. -/
267noncomputable def finiteGroupAlgebraLift
268 (R : Type u) (G : Type v) (N : Type w) [CommRing R] [Group G] [Finite G]
269 [TopologicalSpace R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
270 [ContinuousAdd N] [ContinuousSMul R N] (f : G → N) :
271 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
272 MonoidAlgebra R G →L[R] N := by
273 classical
274 letI : Fintype G := Fintype.ofFinite G
275 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
276 letI : TopologicalSpace (G →₀ R) := finiteGroupAlgebraTopology R G
277 exact
278 { toLinearMap :=
279 (finiteGroupAlgebraPiLift R G N f).toLinearMap.comp
280 (Finsupp.linearEquivFunOnFinite R R G).toLinearMap
281 cont :=
282 by
283 have hcont :
284 Continuous
285 ((Finsupp.linearEquivFunOnFinite R R G) :
286 MonoidAlgebra R G → G → R) := by
288 change Continuous ((e : MonoidAlgebra R G ≃ₜ (G → R)) :
289 MonoidAlgebra R G → G → R)
290 exact e.continuous
291 exact (finiteGroupAlgebraPiLift R G N f).continuous.comp hcont }
293/-- The finite group-algebra lift sends the group-like basis vector at `g` to `f g`. -/
294@[simp]
296 (R : Type u) (G : Type v) (N : Type w) [CommRing R] [Group G] [Finite G]
297 [TopologicalSpace R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
298 [ContinuousAdd N] [ContinuousSMul R N] (f : G → N) (g : G) :
299 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
300 finiteGroupAlgebraLift R G N f (MonoidAlgebra.of R G g) = f g := by
301 classical
302 letI : Fintype G := Fintype.ofFinite G
303 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
305 ((Finsupp.linearEquivFunOnFinite R R G) (Finsupp.single g (1 : R))) =
306 f g
307 rw [Finsupp.linearEquivFunOnFinite_single]
310/-- Finite-stage group algebras are the free profinite modules on the underlying finite
311discrete group. -/
313 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
314 [TopologicalSpace G] [Finite G] [DiscreteTopology G] (hR : IsProfiniteRing R) :
315 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
316 IsFreeProfiniteModuleOn R G (MonoidAlgebra R G) (MonoidAlgebra.of R G) := by
317 classical
318 letI : Fintype G := Fintype.ofFinite G
319 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
320 have hM : IsProfiniteModule R (MonoidAlgebra R G) :=
322 refine ⟨hR, hM, continuous_of_discreteTopology, ?_, ?_⟩
323 · rw [Set.eq_univ_iff_forall]
324 intro m
325 apply subset_closure
326 change m ∈ Submodule.span R (Set.range (MonoidAlgebra.of R G))
327 have hm : m = ∑ g : G, (m g) • MonoidAlgebra.of R G g := by
328 have hm_single : m = ∑ g : G, MonoidAlgebra.single g (m g) := by
329 have hsum : m.sum MonoidAlgebra.single = m := MonoidAlgebra.sum_single m
330 have hfin :
331 m.sum MonoidAlgebra.single = ∑ g : G, MonoidAlgebra.single g (m g) :=
332 Finsupp.sum_fintype m (fun g r => MonoidAlgebra.single g r) (by intro g; simp only [Finsupp.single_zero])
333 exact hsum.symm.trans hfin
334 simpa [MonoidAlgebra.of] using hm_single
335 rw [hm]
336 exact Submodule.sum_mem _ fun g _ => Submodule.smul_mem _ (m g)
337 (Submodule.subset_span ⟨g, rfl⟩)
338 · intro N _addN _topN _modN hN f _hf
339 letI : IsTopologicalAddGroup N := hN.2.1
340 letI : ContinuousAdd N := inferInstance
341 letI : ContinuousSMul R N := hN.2.2.1
342 let F : MonoidAlgebra R G →L[R] N := finiteGroupAlgebraLift R G N f
343 refine ⟨F, ?_, ?_⟩
344 · intro g
346 · intro H hH
347 ext m
348 let s : MonoidAlgebra R G := ∑ g : G, (m g) • MonoidAlgebra.of R G g
349 have hm : m = s := by
350 have hm_single : m = ∑ g : G, MonoidAlgebra.single g (m g) := by
351 have hsum : m.sum MonoidAlgebra.single = m := MonoidAlgebra.sum_single m
352 have hfin :
353 m.sum MonoidAlgebra.single = ∑ g : G, MonoidAlgebra.single g (m g) :=
354 Finsupp.sum_fintype m (fun g r => MonoidAlgebra.single g r) (by intro g; simp only [Finsupp.single_zero])
355 exact hsum.symm.trans hfin
356 simpa [s, MonoidAlgebra.of] using hm_single
357 rw [hm]
358 calc
359 H s = ∑ g : G, (m g) • H (MonoidAlgebra.of R G g) := by
360 change H (∑ g : G, (m g) • MonoidAlgebra.of R G g) =
361 ∑ g : G, (m g) • H (MonoidAlgebra.of R G g)
362 simp only [map_sum, map_smul]
363 _ = ∑ g : G, (m g) • f g := by
364 apply Finset.sum_congr rfl
365 intro g _hg
366 rw [hH]
367 _ = F s := by
368 symm
369 calc
370 F s = ∑ g : G, (m g) • F (MonoidAlgebra.of R G g) := by
371 change F (∑ g : G, (m g) • MonoidAlgebra.of R G g) =
372 ∑ g : G, (m g) • F (MonoidAlgebra.of R G g)
373 simp only [map_sum, map_smul]
374 _ = ∑ g : G, (m g) • f g := by
375 apply Finset.sum_congr rfl
376 intro g _hg
377 have hFg : F (MonoidAlgebra.of R G g) = f g := by
378 simpa [F] using finiteGroupAlgebraLift_apply_of R G N f g
379 rw [hFg]