Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract
1import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Functoriality
3/-!
4# Algebraic group-algebra augmentation
6This file defines augmentation of an abstract group algebra, its linear form and kernel ideal,
7and the resulting short exact sequences. It also proves that the differences \(g-1\) generate the
8augmentation ideal.
9-/
11open scoped Topology
12open ProCGroups
14namespace CompletedGroupAlgebra
16universe u v w z
18/-- The augmentation map \(R[G] \to R\), sending every group-like basis element to \(1\). -/
19noncomputable def groupAlgebraAugmentation
20 (R : Type u) (G : Type v) [CommRing R] [Group G] :
21 MonoidAlgebra R G →+* R :=
22 (MonoidAlgebra.lift R R G (1 : MonoidHom G R)).toRingHom
24/-- On a group-like basis element, the abstract augmentation is 1. -/
25@[simp]
26theorem groupAlgebraAugmentation_of
27 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
28 groupAlgebraAugmentation R G (MonoidAlgebra.of R G g) = 1 := by
29 simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, MonoidAlgebra.of_apply,
30 RingHom.coe_coe,
31 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
33/-- On a finitely supported singleton, the abstract augmentation returns its coefficient. -/
34@[simp]
35theorem groupAlgebraAugmentation_single
36 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) (r : R) :
37 groupAlgebraAugmentation R G (MonoidAlgebra.single g r) = r := by
38 simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
39 MonoidAlgebra.lift_single,
40 MonoidHom.one_apply, smul_eq_mul, mul_one]
42/-- The abstract augmentation restricts to the identity on coefficient scalars. -/
43@[simp]
44theorem groupAlgebraAugmentation_algebraMap
45 (R : Type u) (G : Type v) [CommRing R] [Group G] (r : R) :
46 groupAlgebraAugmentation R G (algebraMap R (MonoidAlgebra R G) r) = r := by
47 simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, MonoidAlgebra.coe_algebraMap,
48 Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq, RingHom.coe_coe,
49 MonoidAlgebra.lift_single,
50 MonoidHom.one_apply, smul_eq_mul, mul_one]
52/-- The abstract group-algebra augmentation is split by the coefficient inclusion. -/
53theorem groupAlgebraAugmentation_surjective
54 (R : Type u) (G : Type v) [CommRing R] [Group G] :
55 Function.Surjective (groupAlgebraAugmentation R G) := by
56 intro r
57 refine ⟨algebraMap R (MonoidAlgebra R G) r, ?_⟩
58 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id,
59 Function.comp_apply, id_eq,
60 groupAlgebraAugmentation_single]
62/-- The augmentation map \(R[G] \to R\) is viewed as an \(R\)-linear map. -/
63noncomputable def groupAlgebraAugmentationLinearMap
64 (R : Type u) (G : Type v) [CommRing R] [Group G] :
65 MonoidAlgebra R G →ₗ[R] R where
66 toFun := groupAlgebraAugmentation R G
67 map_add' := by
68 intro x y
69 exact map_add (groupAlgebraAugmentation R G) x y
70 map_smul' := by
71 intro r x
72 simp only [Algebra.smul_def, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
73 RingHom.coe_id,
74 Function.comp_apply, id_eq, map_mul, groupAlgebraAugmentation_single, RingHom.id_apply]
76/--
77The augmentation map is evaluated by projecting to the corresponding finite group-algebra stage
78and summing coefficients via the usual group-algebra augmentation.
79-/
80@[simp]
81theorem groupAlgebraAugmentationLinearMap_apply
82 (R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
83 groupAlgebraAugmentationLinearMap R G x = groupAlgebraAugmentation R G x :=
84 rfl
86/-- The \(R\)-linear augmentation is split by the coefficient inclusion. -/
87theorem groupAlgebraAugmentationLinearMap_surjective
88 (R : Type u) (G : Type v) [CommRing R] [Group G] :
89 Function.Surjective (groupAlgebraAugmentationLinearMap R G) := by
90 simpa [groupAlgebraAugmentationLinearMap] using groupAlgebraAugmentation_surjective R G
92/-- The augmentation ideal of an abstract group algebra. -/
93noncomputable def groupAlgebraAugmentationIdeal
94 (R : Type u) (G : Type v) [CommRing R] [Group G] :
95 Ideal (MonoidAlgebra R G) :=
96 RingHom.ker (groupAlgebraAugmentation R G)
98/-- The augmentation ideal of an abstract group algebra, regarded as an \(R\)-submodule. -/
99noncomputable def groupAlgebraAugmentationIdealSubmodule
100 (R : Type u) (G : Type v) [CommRing R] [Group G] :
101 Submodule R (MonoidAlgebra R G) :=
102 (groupAlgebraAugmentationIdeal R G).restrictScalars R
104/--
105An abstract group-algebra element lies in the augmentation ideal iff its augmentation is zero.
106-/
107@[simp]
108theorem mem_groupAlgebraAugmentationIdeal_iff
109 {R : Type u} {G : Type v} [CommRing R] [Group G] {x : MonoidAlgebra R G} :
110 x ∈ groupAlgebraAugmentationIdeal R G ↔ groupAlgebraAugmentation R G x = 0 :=
111 Iff.rfl
113/--
114An abstract group-algebra element lies in the augmentation ideal submodule iff its augmentation
115is zero.
116-/
117@[simp]
118theorem mem_groupAlgebraAugmentationIdealSubmodule_iff
119 {R : Type u} {G : Type v} [CommRing R] [Group G] {x : MonoidAlgebra R G} :
120 x ∈ groupAlgebraAugmentationIdealSubmodule R G ↔ groupAlgebraAugmentation R G x = 0 :=
121 Iff.rfl
123/-- The inclusion of the abstract augmentation ideal into the group algebra is injective. -/
124theorem groupAlgebraAugmentationIdeal_subtype_injective
125 (R : Type u) (G : Type v) [CommRing R] [Group G] :
126 Function.Injective
127 (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G)) := by
128 intro x y hxy
129 exact Subtype.ext hxy
131/-- The abstract augmentation ideal is exactly the kernel of the augmentation. -/
132theorem exact_groupAlgebraAugmentationIdeal_subtype
133 (R : Type u) (G : Type v) [CommRing R] [Group G] :
134 Function.Exact
135 (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G))
136 (groupAlgebraAugmentation R G) := by
137 intro x
138 constructor
139 · intro hx
140 exact ⟨⟨x, hx⟩, rfl⟩
141 · rintro ⟨y, rfl⟩
142 exact y.2
144/--
145At the level of underlying functions, the subtype inclusion of the abstract augmentation ideal,
146followed by the ordinary augmentation, is a short exact sequence.
147-/
148theorem groupAlgebraAugmentation_shortExact
149 (R : Type u) (G : Type v) [CommRing R] [Group G] :
150 Function.Injective
151 (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G)) ∧
152 Function.Exact
153 (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G))
154 (groupAlgebraAugmentation R G) ∧
155 Function.Surjective (groupAlgebraAugmentation R G) := by
156 exact ⟨groupAlgebraAugmentationIdeal_subtype_injective R G,
157 exact_groupAlgebraAugmentationIdeal_subtype R G,
158 groupAlgebraAugmentation_surjective R G⟩
160/--
161The inclusion of the abstract augmentation ideal into the group algebra as an \(R\)-linear map.
162-/
163noncomputable def groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap
164 (R : Type u) (G : Type v) [CommRing R] [Group G] :
165 groupAlgebraAugmentationIdealSubmodule R G →ₗ[R] MonoidAlgebra R G :=
166 (groupAlgebraAugmentationIdealSubmodule R G).subtype
168/--
169The subtype linear map from the abstract augmentation-ideal submodule into the group algebra is
170injective.
171-/
172theorem groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap_injective
173 (R : Type u) (G : Type v) [CommRing R] [Group G] :
174 Function.Injective (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G) := by
175 intro x y hxy
176 exact Subtype.ext hxy
178/-- The abstract augmentation ideal is the kernel of the \(R\)-linear augmentation. -/
179theorem exact_groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap
180 (R : Type u) (G : Type v) [CommRing R] [Group G] :
181 Function.Exact
182 (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G)
183 (groupAlgebraAugmentationLinearMap R G) := by
184 intro x
185 constructor
186 · intro hx
187 exact ⟨⟨x, hx⟩, rfl⟩
188 · rintro ⟨y, rfl⟩
189 exact y.2
191/--
192The \(R\)-linear inclusion of the abstract augmentation-ideal submodule, followed by the linear
193augmentation, is a short exact sequence of underlying functions.
194-/
195theorem groupAlgebraAugmentationLinearMap_shortExact
196 (R : Type u) (G : Type v) [CommRing R] [Group G] :
197 Function.Injective (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G) ∧
198 Function.Exact
199 (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G)
200 (groupAlgebraAugmentationLinearMap R G) ∧
201 Function.Surjective (groupAlgebraAugmentationLinearMap R G) := by
202 exact ⟨groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap_injective R G,
203 exact_groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G,
204 groupAlgebraAugmentationLinearMap_surjective R G⟩
206/-- The standard generator \(g-1\) of the abstract augmentation ideal. -/
207noncomputable def groupAlgebraAugmentationGenerator
208 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
209 MonoidAlgebra R G :=
210 MonoidAlgebra.of R G g - 1
212/-- The ideal generated by the standard abstract augmentation generators \(g-1\). -/
213noncomputable def groupAlgebraAugmentationGeneratorIdeal
214 (R : Type u) (G : Type v) [CommRing R] [Group G] :
215 Ideal (MonoidAlgebra R G) :=
216 Ideal.span (Set.range (groupAlgebraAugmentationGenerator R G))
218/-- A standard abstract augmentation generator lies in the augmentation ideal. -/
219theorem groupAlgebraAugmentationGenerator_mem_augmentationIdeal
220 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
221 groupAlgebraAugmentationGenerator R G g ∈ groupAlgebraAugmentationIdeal R G := by
222 simp only [groupAlgebraAugmentationGenerator, MonoidAlgebra.of_apply,
223 mem_groupAlgebraAugmentationIdeal_iff,
224 map_sub, groupAlgebraAugmentation_single, map_one, sub_self]
226/-- A standard abstract augmentation generator lies in the ideal generated by such generators. -/
227theorem groupAlgebraAugmentationGenerator_mem_generatorIdeal
228 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
229 groupAlgebraAugmentationGenerator R G g ∈
230 groupAlgebraAugmentationGeneratorIdeal R G := by
231 exact Ideal.subset_span ⟨g, rfl⟩
233/-- The standard-generator ideal is contained in the abstract augmentation ideal. -/
234theorem groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal
235 (R : Type u) (G : Type v) [CommRing R] [Group G] :
236 groupAlgebraAugmentationGeneratorIdeal R G ≤ groupAlgebraAugmentationIdeal R G := by
237 refine Ideal.span_le.2 ?_
238 rintro _ ⟨g, rfl⟩
239 exact groupAlgebraAugmentationGenerator_mem_augmentationIdeal R G g
241/--
242Every abstract group-algebra element differs from its augmentation scalar by an element of the
243standard-generator ideal.
244-/
245theorem exists_mem_groupAlgebraAugmentationGeneratorIdeal_add
246 (R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
247 ∃ y ∈ groupAlgebraAugmentationGeneratorIdeal R G,
248 x = y + algebraMap R (MonoidAlgebra R G) (groupAlgebraAugmentation R G x) := by
249 refine MonoidAlgebra.induction_on
250 (p := fun x : MonoidAlgebra R G =>
251 ∃ y ∈ groupAlgebraAugmentationGeneratorIdeal R G,
252 x = y + algebraMap R (MonoidAlgebra R G) (groupAlgebraAugmentation R G x))
253 x ?_ ?_ ?_
254 · intro g
255 refine
256 ⟨groupAlgebraAugmentationGenerator R G g,
257 groupAlgebraAugmentationGenerator_mem_generatorIdeal R G g, ?_⟩
258 rw [groupAlgebraAugmentationGenerator, groupAlgebraAugmentation_of]
259 rw [map_one]
260 rw [sub_add_cancel]
261 · intro x z hx hz
262 rcases hx with ⟨y, hy, hxy⟩
263 rcases hz with ⟨w, hw, hwz⟩
264 refine ⟨y + w, (groupAlgebraAugmentationGeneratorIdeal R G).add_mem hy hw, ?_⟩
265 have hy0 : groupAlgebraAugmentation R G y = 0 :=
266 (mem_groupAlgebraAugmentationIdeal_iff (R := R) (G := G) (x := y)).1
267 (groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal R G hy)
268 have hw0 : groupAlgebraAugmentation R G w = 0 :=
269 (mem_groupAlgebraAugmentationIdeal_iff (R := R) (G := G) (x := w)).1
270 (groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal R G hw)
271 rw [hxy, hwz, map_add]
272 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id,
273 Function.comp_apply, id_eq,
274 add_left_comm, add_assoc, map_add, hy0, groupAlgebraAugmentation_single, zero_add, hw0]
275 · intro r x hx
276 rcases hx with ⟨y, hy, hxy⟩
277 refine ⟨r • y, ?_, ?_⟩
278 · have hy' :
279 algebraMap R (MonoidAlgebra R G) r * y ∈
280 groupAlgebraAugmentationGeneratorIdeal R G :=
281 (groupAlgebraAugmentationGeneratorIdeal R G).mul_mem_left _ hy
282 simpa [Algebra.smul_def] using hy'
283 · have hy0 : groupAlgebraAugmentation R G y = 0 :=
284 (mem_groupAlgebraAugmentationIdeal_iff (R := R) (G := G) (x := y)).1
285 (groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal R G hy)
286 rw [hxy, smul_add]
287 simp only [Algebra.smul_def, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
288 RingHom.coe_id,
289 Function.comp_apply, id_eq, MonoidAlgebra.single_mul_single, mul_one, map_add, map_mul,
290 groupAlgebraAugmentation_single, hy0, mul_zero, zero_add]
292/-- The abstract augmentation ideal is generated by the standard elements \(g-1\). -/
293theorem groupAlgebraAugmentationGeneratorIdeal_eq_augmentationIdeal
294 (R : Type u) (G : Type v) [CommRing R] [Group G] :
295 groupAlgebraAugmentationGeneratorIdeal R G = groupAlgebraAugmentationIdeal R G := by
296 refine le_antisymm
297 (groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal R G) ?_
298 intro x hx
299 rcases exists_mem_groupAlgebraAugmentationGeneratorIdeal_add R G x with ⟨y, hy, hxy⟩
300 have haug : groupAlgebraAugmentation R G x = 0 :=
301 (mem_groupAlgebraAugmentationIdeal_iff (R := R) (G := G) (x := x)).1 hx
302 rw [hxy, haug]
303 simpa using hy
305/-- The standard generators \(g-1\), viewed inside the augmentation ideal. -/
306noncomputable def groupAlgebraAugmentationGeneratorSubtype
307 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
308 groupAlgebraAugmentationIdeal R G :=
309 ⟨groupAlgebraAugmentationGenerator R G g,
310 groupAlgebraAugmentationGenerator_mem_augmentationIdeal R G g⟩
312/-- The augmentation ideal is spanned by the standard generators viewed in the ideal itself. -/
313theorem groupAlgebraAugmentationGeneratorSubtype_span_eq_top
314 (R : Type u) (G : Type v) [CommRing R] [Group G] :
315 Submodule.span (MonoidAlgebra R G)
316 (Set.range (groupAlgebraAugmentationGeneratorSubtype R G)) = ⊤ := by
317 have hspan :
318 Submodule.span (MonoidAlgebra R G)
319 (Set.range fun g =>
320 (⟨groupAlgebraAugmentationGenerator R G g,
321 groupAlgebraAugmentationGenerator_mem_augmentationIdeal R G g⟩ :
322 groupAlgebraAugmentationIdeal R G)) = ⊤ := by
323 rw [Submodule.span_range_subtype_eq_top_iff
324 (p := groupAlgebraAugmentationIdeal R G)
325 (s := groupAlgebraAugmentationGenerator R G)
326 (hs := groupAlgebraAugmentationGenerator_mem_augmentationIdeal R G)]
327 simpa [groupAlgebraAugmentationGeneratorIdeal] using
328 congrArg
329 (fun I : Ideal (MonoidAlgebra R G) =>
330 (I : Submodule (MonoidAlgebra R G) (MonoidAlgebra R G)))
331 (groupAlgebraAugmentationGeneratorIdeal_eq_augmentationIdeal R G)
332 unfold groupAlgebraAugmentationGeneratorSubtype
333 exact hspan
335/-- On a finite group algebra, the augmentation is the finite sum of coordinates. -/
336theorem finiteGroupAlgebra_augmentation_apply_eq_sum
337 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G]
338 (x : MonoidAlgebra R G) :
339 letI : Fintype G := Fintype.ofFinite G
340 groupAlgebraAugmentation R G x = ∑ g : G, x.coeff g := by
341 classical
342 letI : Fintype G := Fintype.ofFinite G
343 calc
344 groupAlgebraAugmentation R G x = x.coeff.sum (fun _ r => r) := by
345 simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
346 MonoidAlgebra.lift_apply,
347 MonoidHom.one_apply, smul_eq_mul, mul_one]
348 _ = ∑ g : G, x.coeff g := by
349 exact Finsupp.sum_fintype x.coeff (fun _ r => r) (by intro g; simp only)
351/--
352The coefficient inclusion into a finite-stage group algebra is continuous for the product
353topology.
354-/
355theorem finiteGroupAlgebra_algebraMap_continuous
356 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
357 [Group G] [Finite G] :
358 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
359 Continuous (algebraMap R (MonoidAlgebra R G)) := by
360 classical
361 letI : Fintype G := Fintype.ofFinite G
362 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
363 let e : MonoidAlgebra R G ≃ (G → R) :=
364 (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
365 have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
366 Topology.IsInducing.induced e
367 rw [he.continuous_iff]
368 apply continuous_pi
369 intro g
370 change Continuous fun r : R => (MonoidAlgebra.single (1 : G) r).coeff g
371 by_cases hg : g = 1
372 · subst g
373 simpa only [MonoidAlgebra.coeff_single, Finsupp.single_apply, if_pos] using
374 (continuous_id' : Continuous fun r : R => r)
375 · rw [show (fun r : R => (MonoidAlgebra.single (1 : G) r).coeff g) =
376 (fun _ : R => 0) from by
377 funext r
378 simp only [MonoidAlgebra.coeff_single, Finsupp.single_apply,
379 if_neg (Ne.symm hg)]]
380 exact continuous_const
382/-- The augmentation map is continuous on each finite-stage group algebra. -/
383theorem finiteGroupAlgebra_augmentation_continuous
384 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
385 [Group G] [Finite G] :
386 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
387 Continuous (groupAlgebraAugmentation R G) := by
388 classical
389 letI : Fintype G := Fintype.ofFinite G
390 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
391 change Continuous (fun x : MonoidAlgebra R G => groupAlgebraAugmentation R G x)
392 rw [show (fun x : MonoidAlgebra R G => groupAlgebraAugmentation R G x) =
393 (fun x : MonoidAlgebra R G => ∑ g : G, x.coeff g) from by
394 funext x
395 exact finiteGroupAlgebra_augmentation_apply_eq_sum R G x]
396 apply continuous_finsetSum
397 intro g _hg
398 exact finiteGroupAlgebra_coordinate_continuous R G g
400/-- The augmentation is natural for the finite-stage group-algebra functor. -/
401theorem groupAlgebraAugmentation_mapDomainRingHom
402 (R : Type u) (G : Type v) (H : Type w) [CommRing R] [Group G] [Group H]
403 (φ : G →* H) (x : MonoidAlgebra R G) :
404 groupAlgebraAugmentation R H (MonoidAlgebra.mapDomainRingHom R φ x) =
405 groupAlgebraAugmentation R G x := by
406 refine MonoidAlgebra.induction_linear x ?_ ?_ ?_
407 · simp only [map_zero]
408 · intro y z hy hz
409 simp only [map_add, hy, hz]
410 · intro g r
411 rw [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single,
412 groupAlgebraAugmentation_single, groupAlgebraAugmentation_single]
414/-- The augmentation is natural in the coefficient ring. -/
415theorem groupAlgebraAugmentation_mapRangeRingHom
416 (R : Type u) (S : Type w) (G : Type v) [CommRing R] [CommRing S] [Group G]
417 (f : R →+* S) (x : MonoidAlgebra R G) :
418 groupAlgebraAugmentation S G (MonoidAlgebra.mapRingHom G f x) =
419 f (groupAlgebraAugmentation R G x) := by
420 refine MonoidAlgebra.induction_linear x ?_ ?_ ?_
421 · simp only [map_zero]
422 · intro y z hy hz
423 simp only [map_add, hy, hz]
424 · intro g r
425 rw [MonoidAlgebra.mapRingHom_single, groupAlgebraAugmentation_single,
426 groupAlgebraAugmentation_single]
428end CompletedGroupAlgebra