Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Topology
1import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals
2import Mathlib.GroupTheory.FiniteAbelian.Basic
4/-!
5# Topology and universal maps for finite group algebras
7A finite group algebra over a profinite coefficient ring is identified with a finite product of
8coefficients and given its profinite ring topology. This file proves continuity of its operations
9and constructs continuous linear lifts from basis data.
10-/
12open scoped Topology
13open ProCGroups
15namespace CompletedGroupAlgebra
17universe u v w
19/--
20The product topology on the group algebra of a finite group, transported through \(R[G] = G
21\to_0 R \simeq G \to R\). This is the finite stage used in the construction of the completed
22group algebra.
23-/
24@[reducible]
25noncomputable def finiteGroupAlgebraTopology
26 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R] :
27 TopologicalSpace (MonoidAlgebra R G) :=
28 TopologicalSpace.induced
29 ((MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans
30 Finsupp.equivFunOnFinite : MonoidAlgebra R G ≃ (G → R))
31 inferInstance
33/--
34The finite group algebra with its transported product topology is homeomorphic to the function
35space \(G \to R\).
36-/
37noncomputable def finiteGroupAlgebraHomeomorph
38 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R] :
39 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
40 MonoidAlgebra R G ≃ₜ (G → R) := by
41 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
42 let e : MonoidAlgebra R G ≃ (G → R) :=
43 (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
44 have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
45 Topology.IsInducing.induced e
46 exact e.toHomeomorphOfIsInducing he
48/--
49The finite-stage group algebra is the finite product of copies of the coefficient ring as a
50topological \(R\)-module.
51-/
52noncomputable def finiteGroupAlgebraContinuousLinearEquivPi
53 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R] :
54 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
55 MonoidAlgebra R G ≃L[R] (G → R) := by
56 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
57 let e : MonoidAlgebra R G ≃ (G → R) :=
58 (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
59 have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
60 Topology.IsInducing.induced e
61 exact ContinuousLinearEquiv.mk
62 ((MonoidAlgebra.coeffLinearEquiv R).trans
63 (Finsupp.linearEquivFunOnFinite R R G))
64 (by
65 change Continuous (e : MonoidAlgebra R G → G → R)
66 exact he.continuous)
67 (by
68 change Continuous ((e.toHomeomorphOfIsInducing he).symm : (G → R) → MonoidAlgebra R G)
69 exact (e.toHomeomorphOfIsInducing he).symm.continuous)
71/-- The continuous equivalence is evaluated by the corresponding comparison formula. -/
72@[simp]
73theorem finiteGroupAlgebraContinuousLinearEquivPi_apply
74 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
75 (x : MonoidAlgebra R G) :
76 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
77 finiteGroupAlgebraContinuousLinearEquivPi R G x =
78 Finsupp.equivFunOnFinite x.coeff :=
79 rfl
81/--
82Coordinate evaluation on a finite group algebra is continuous for the transported product
83topology.
84-/
85theorem finiteGroupAlgebra_coordinate_continuous
86 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R] :
87 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
88 ∀ g : G, Continuous fun x : MonoidAlgebra R G => x.coeff g := by
89 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
90 let e : MonoidAlgebra R G ≃ (G → R) :=
91 (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
92 intro g
93 change Continuous ((fun p : G → R => p g) ∘
94 (e : MonoidAlgebra R G → G → R))
95 exact
96 (continuous_apply g).comp
97 (continuous_induced_dom : Continuous (e : MonoidAlgebra R G → G → R))
99/-- Addition is continuous for the finite-stage group algebra topology. -/
100theorem finiteGroupAlgebra_continuousAdd
101 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
102 [IsTopologicalRing R] :
103 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
104 ContinuousAdd (MonoidAlgebra R G) := by
105 classical
106 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
107 let A := MonoidAlgebra R G
108 let e : A ≃ (G → R) :=
109 (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
110 have he : Topology.IsInducing (e : A → G → R) := Topology.IsInducing.induced e
111 have hcoord : ∀ g : G, Continuous fun x : A => x.coeff g :=
112 finiteGroupAlgebra_coordinate_continuous R G
113 refine ⟨?_⟩
114 rw [he.continuous_iff]
115 apply continuous_pi
116 intro g
117 change Continuous fun p : A × A => p.1.coeff g + p.2.coeff g
118 exact ((hcoord g).comp continuous_fst).add ((hcoord g).comp continuous_snd)
120/-- Negation is continuous for the finite-stage group algebra topology. -/
121theorem finiteGroupAlgebra_continuousNeg
122 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
123 [IsTopologicalRing R] :
124 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
125 ContinuousNeg (MonoidAlgebra R G) := by
126 classical
127 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
128 let A := MonoidAlgebra R G
129 let e : A ≃ (G → R) :=
130 (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
131 have he : Topology.IsInducing (e : A → G → R) := Topology.IsInducing.induced e
132 have hcoord : ∀ g : G, Continuous fun x : A => x.coeff g :=
133 finiteGroupAlgebra_coordinate_continuous R G
134 refine ⟨?_⟩
135 rw [he.continuous_iff]
136 apply continuous_pi
137 intro g
138 change Continuous fun x : A => -x.coeff g
139 exact (hcoord g).neg
141/--
142Multiplication is continuous for the finite-stage group algebra topology. The coordinate formula
143is the finite convolution sum over pairs (g1,g2) with \(g1*g2 = g\).
144-/
145theorem finiteGroupAlgebra_continuousMul
146 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
147 [IsTopologicalRing R] :
148 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
149 ContinuousMul (MonoidAlgebra R G) := by
150 classical
151 letI : Fintype G := Fintype.ofFinite G
152 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
153 let A := MonoidAlgebra R G
154 let e : A ≃ (G → R) :=
155 (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
156 have he : Topology.IsInducing (e : A → G → R) := Topology.IsInducing.induced e
157 have hcoord : ∀ g : G, Continuous fun x : A => x.coeff g :=
158 finiteGroupAlgebra_coordinate_continuous R G
159 refine ⟨?_⟩
160 rw [he.continuous_iff]
161 apply continuous_pi
162 intro g
163 change Continuous fun p : A × A => (p.1 * p.2).coeff g
164 rw [show (fun p : A × A => (p.1 * p.2).coeff g) =
165 (fun p : A × A => ∑ q ∈ (Finset.univ.filter (fun q : G × G => q.1 * q.2 = g)),
166 p.1.coeff q.1 * p.2.coeff q.2) from ?_]
167 · apply continuous_finsetSum
168 intro q _hq
169 exact ((hcoord q.1).comp continuous_fst).mul ((hcoord q.2).comp continuous_snd)
170 · funext p
171 exact MonoidAlgebra.coeff_mul_antidiag p.1 p.2 g
172 (Finset.univ.filter (fun q : G × G => q.1 * q.2 = g)) (by intro q; simp only
173 [Finset.mem_filter, Finset.mem_univ, true_and])
175/--
176Scalar multiplication by the coefficient ring is continuous on the finite-stage group algebra
177topology.
178-/
179theorem finiteGroupAlgebra_continuousSMul
180 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
181 [IsTopologicalRing R] :
182 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
183 ContinuousSMul R (MonoidAlgebra R G) := by
184 classical
185 letI : Fintype G := Fintype.ofFinite G
186 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
187 let A := MonoidAlgebra R G
188 let e : A ≃ (G → R) :=
189 (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
190 have he : Topology.IsInducing (e : A → G → R) := Topology.IsInducing.induced e
191 have hcoord : ∀ g : G, Continuous fun x : A => x.coeff g :=
192 finiteGroupAlgebra_coordinate_continuous R G
193 refine ContinuousSMul.mk ?_
194 rw [he.continuous_iff]
195 apply continuous_pi
196 intro g
197 change Continuous fun p : R × A => p.1 * p.2.coeff g
198 exact continuous_fst.mul ((hcoord g).comp continuous_snd)
200/-- The finite-stage group algebra topology makes \(R[G]\) a topological ring. -/
201theorem finiteGroupAlgebra_isTopologicalRing
202 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G] [TopologicalSpace R]
203 [IsTopologicalRing R] :
204 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
205 IsTopologicalRing (MonoidAlgebra R G) := by
206 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
207 letI : ContinuousAdd (MonoidAlgebra R G) := finiteGroupAlgebra_continuousAdd R G
208 letI : ContinuousMul (MonoidAlgebra R G) := finiteGroupAlgebra_continuousMul R G
209 letI : ContinuousNeg (MonoidAlgebra R G) := finiteGroupAlgebra_continuousNeg R G
210 letI : IsTopologicalSemiring (MonoidAlgebra R G) := IsTopologicalSemiring.mk
211 exact IsTopologicalRing.mk
213/-- Compactness of the coefficient ring passes to a finite-stage group algebra. -/
214theorem finiteGroupAlgebra_compactSpace
215 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
216 [CompactSpace R] :
217 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
218 CompactSpace (MonoidAlgebra R G) := by
219 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
220 exact Homeomorph.compactSpace (finiteGroupAlgebraHomeomorph R G).symm
222/-- The Hausdorff property of the coefficient ring passes to a finite-stage group algebra. -/
223theorem finiteGroupAlgebra_t2Space
224 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
225 [T2Space R] :
226 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
227 T2Space (MonoidAlgebra R G) := by
228 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
229 exact Homeomorph.t2Space (finiteGroupAlgebraHomeomorph R G).symm
231/-- Total disconnectedness of the coefficient ring passes to a finite-stage group algebra. -/
232theorem finiteGroupAlgebra_totallyDisconnectedSpace
233 (R : Type u) (G : Type v) [CommRing R] [Finite G] [TopologicalSpace R]
234 [TotallyDisconnectedSpace R] :
235 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
236 TotallyDisconnectedSpace (MonoidAlgebra R G) := by
237 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
238 exact Homeomorph.totallyDisconnectedSpace (finiteGroupAlgebraHomeomorph R G).symm
240/--
241The finite function-space lift sends a coefficient function to the finite sum of its
242coefficients acting on the prescribed values.
243-/
244private noncomputable def finiteGroupAlgebraPiLift
245 (R : Type u) (G : Type v) (N : Type w)
246 [Ring R] [TopologicalSpace R] [Fintype G]
247 [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousSMul R N]
248 (f : G -> N) : (G -> R) →L[R] N where
249 toLinearMap :=
250 { toFun := fun m => ∑ x : G, m x • f x
251 map_add' := by
252 intro m n
253 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
254 map_smul' := by
255 intro lam m
256 simp only [Pi.smul_apply, smul_eq_mul, mul_smul, RingHom.id_apply, Finset.smul_sum]}
257 cont := by
258 apply continuous_finsetSum
259 intro x _hx
260 exact (continuous_apply x).smul continuous_const
262/--
263The finite function-space lift sends the basis function \(\mathrm{Pi.single}\ g\ 1\) to
264\(f(g)\).
265-/
266private theorem finiteGroupAlgebraPiLift_apply_basis
267 (R : Type u) (G : Type v) (N : Type w)
268 [Ring R] [TopologicalSpace R] [Fintype G] [DecidableEq G]
269 [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousSMul R N]
270 (f : G -> N) (g : G) :
271 finiteGroupAlgebraPiLift R G N f (Pi.single g (1 : R)) = f g := by
272 simp only [finiteGroupAlgebraPiLift, ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk,
273 Pi.single_apply, ite_smul, one_smul, zero_smul, Finset.sum_ite_eq', Finset.mem_univ,
274 ↓reduceIte]
276/--
277A continuous linear map out of a finite group algebra is determined by its values on group
278elements.
279-/
280noncomputable def finiteGroupAlgebraLift
281 (R : Type u) (G : Type v) (N : Type w) [CommRing R] [Finite G]
282 [TopologicalSpace R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
283 [ContinuousAdd N] [ContinuousSMul R N] (f : G → N) :
284 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
285 MonoidAlgebra R G →L[R] N := by
286 classical
287 letI : Fintype G := Fintype.ofFinite G
288 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
289 exact
290 { toLinearMap :=
291 (finiteGroupAlgebraPiLift R G N f).toLinearMap.comp
292 ((MonoidAlgebra.coeffLinearEquiv R).trans
293 (Finsupp.linearEquivFunOnFinite R R G)).toLinearMap
294 cont :=
295 by
296 have hcont :
297 Continuous
298 (((MonoidAlgebra.coeffLinearEquiv R).trans
299 (Finsupp.linearEquivFunOnFinite R R G)) :
300 MonoidAlgebra R G → G → R) := by
301 let e := finiteGroupAlgebraHomeomorph R G
302 change Continuous ((e : MonoidAlgebra R G ≃ₜ (G → R)) :
303 MonoidAlgebra R G → G → R)
304 exact e.continuous
305 exact (finiteGroupAlgebraPiLift R G N f).continuous.comp hcont }
307/-- The finite group-algebra lift sends the group-like basis vector at \(g\) to \(f(g)\). -/
308@[simp]
309theorem finiteGroupAlgebraLift_apply_of
310 (R : Type u) (G : Type v) (N : Type w) [CommRing R] [Group G] [Finite G]
311 [TopologicalSpace R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
312 [ContinuousAdd N] [ContinuousSMul R N] (f : G → N) (g : G) :
313 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
314 finiteGroupAlgebraLift R G N f (MonoidAlgebra.of R G g) = f g := by
315 classical
316 letI : Fintype G := Fintype.ofFinite G
317 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
318 rw [show MonoidAlgebra.of R G g =
319 (MonoidAlgebra.single g 1 : MonoidAlgebra R G) by rfl]
320 change finiteGroupAlgebraPiLift R G N f
321 ((Finsupp.linearEquivFunOnFinite R R G)
322 ((MonoidAlgebra.single g (1 : R) : MonoidAlgebra R G).coeff)) =
323 f g
324 rw [MonoidAlgebra.coeff_single]
325 rw [Finsupp.linearEquivFunOnFinite_single]
326 exact finiteGroupAlgebraPiLift_apply_basis R G N f g
328end CompletedGroupAlgebra