CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Augmentation/Abstract.lean
1import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Functoriality
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Augmentation/Abstract.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14This module treats the ordinary finite group-algebra augmentation and its augmentation ideal before passing to completed or inverse-limit objects.
15-/
17open scoped Topology
18open ProCGroups
20namespace CompletedGroupAlgebra
22universe u v w z
24/-- The augmentation map `R[G] → R`, sending every group-like basis element to `1`. -/
25noncomputable def groupAlgebraAugmentation
26 (R : Type u) (G : Type v) [CommRing R] [Group G] :
27 MonoidAlgebra R G →+* R :=
28 (MonoidAlgebra.lift R R G (1 : MonoidHom G R)).toRingHom
30/-- On a group-like basis element, the abstract augmentation is `1`. -/
31@[simp]
32theorem groupAlgebraAugmentation_of
33 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
34 groupAlgebraAugmentation R G (MonoidAlgebra.of R G g) = 1 := by
35 simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, MonoidAlgebra.of_apply, RingHom.coe_coe,
36 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
38/-- On a finitely supported singleton, the abstract augmentation returns its coefficient. -/
39@[simp]
41 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) (r : R) :
42 groupAlgebraAugmentation R G (MonoidAlgebra.single g r) = r := by
43 simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single,
44 MonoidHom.one_apply, smul_eq_mul, mul_one]
46/-- The abstract augmentation restricts to the identity on coefficient scalars. -/
47@[simp]
49 (R : Type u) (G : Type v) [CommRing R] [Group G] (r : R) :
50 groupAlgebraAugmentation R G (algebraMap R (MonoidAlgebra R G) r) = r := by
51 simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, MonoidAlgebra.coe_algebraMap,
52 Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq, RingHom.coe_coe, MonoidAlgebra.lift_single,
53 MonoidHom.one_apply, smul_eq_mul, mul_one]
55/-- The abstract group-algebra augmentation is split by the coefficient inclusion. -/
57 (R : Type u) (G : Type v) [CommRing R] [Group G] :
58 Function.Surjective (groupAlgebraAugmentation R G) := by
59 intro r
60 refine ⟨algebraMap R (MonoidAlgebra R G) r, ?_⟩
61 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
64/-- The augmentation map `R[G] → R`, viewed as an `R`-linear map. -/
65noncomputable def groupAlgebraAugmentationLinearMap
66 (R : Type u) (G : Type v) [CommRing R] [Group G] :
67 MonoidAlgebra R G →ₗ[R] R where
68 toFun := groupAlgebraAugmentation R G
69 map_add' := by
70 intro x y
71 exact map_add (groupAlgebraAugmentation R G) x y
72 map_smul' := by
73 intro r x
74 simp only [Algebra.smul_def, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id,
75 Function.comp_apply, id_eq, map_mul, groupAlgebraAugmentation_single, RingHom.id_apply]
77/-- The linear augmentation agrees definitionally with the ring augmentation. -/
78@[simp]
80 (R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
81 groupAlgebraAugmentationLinearMap R G x = groupAlgebraAugmentation R G x :=
82 rfl
84/-- The `R`-linear augmentation is split by the coefficient inclusion. -/
86 (R : Type u) (G : Type v) [CommRing R] [Group G] :
87 Function.Surjective (groupAlgebraAugmentationLinearMap R G) := by
88 simpa [groupAlgebraAugmentationLinearMap] using groupAlgebraAugmentation_surjective R G
90/-- The augmentation ideal of an abstract group algebra. -/
91noncomputable def groupAlgebraAugmentationIdeal
92 (R : Type u) (G : Type v) [CommRing R] [Group G] :
93 Ideal (MonoidAlgebra R G) :=
94 RingHom.ker (groupAlgebraAugmentation R G)
96/-- The augmentation ideal of an abstract group algebra, regarded as an `R`-submodule. -/
97noncomputable def groupAlgebraAugmentationIdealSubmodule
98 (R : Type u) (G : Type v) [CommRing R] [Group G] :
99 Submodule R (MonoidAlgebra R G) :=
100 (groupAlgebraAugmentationIdeal R G).restrictScalars R
102/-- Membership in the abstract augmentation ideal is the vanishing of the augmentation. -/
103@[simp]
105 (R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
106 x ∈ groupAlgebraAugmentationIdeal R G ↔ groupAlgebraAugmentation R G x = 0 :=
107 Iff.rfl
109/-- Membership in the augmentation ideal as an `R`-submodule is augmentation-zero. -/
110@[simp]
112 (R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
113 x ∈ groupAlgebraAugmentationIdealSubmodule R G ↔ groupAlgebraAugmentation R G x = 0 :=
114 Iff.rfl
116/-- The inclusion of the abstract augmentation ideal into the group algebra is injective. -/
118 (R : Type u) (G : Type v) [CommRing R] [Group G] :
119 Function.Injective
120 (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G)) := by
121 intro x y hxy
122 exact Subtype.ext hxy
124/-- The abstract augmentation ideal is exactly the kernel of the augmentation. -/
126 (R : Type u) (G : Type v) [CommRing R] [Group G] :
127 Function.Exact
128 (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G))
129 (groupAlgebraAugmentation R G) := by
130 intro x
131 constructor
132 · intro hx
133 exact ⟨⟨x, hx⟩, rfl⟩
134 · rintro ⟨y, rfl⟩
135 exact y.2
137/-- The abstract augmentation sequence `0 → I_G → R[G] → R → 0` is short exact. -/
139 (R : Type u) (G : Type v) [CommRing R] [Group G] :
140 Function.Injective
141 (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G)) ∧
142 Function.Exact
143 (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G))
144 (groupAlgebraAugmentation R G) ∧
145 Function.Surjective (groupAlgebraAugmentation R G) := by
146 exact ⟨groupAlgebraAugmentationIdeal_subtype_injective R G,
150/-- The inclusion of the abstract augmentation ideal into the group algebra as an `R`-linear map. -/
151noncomputable def groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap
152 (R : Type u) (G : Type v) [CommRing R] [Group G] :
153 groupAlgebraAugmentationIdealSubmodule R G →ₗ[R] MonoidAlgebra R G :=
156/-- The `R`-linear augmentation-ideal inclusion is injective. -/
158 (R : Type u) (G : Type v) [CommRing R] [Group G] :
159 Function.Injective (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G) := by
160 intro x y hxy
161 exact Subtype.ext hxy
163/-- The abstract augmentation ideal is the kernel of the `R`-linear augmentation. -/
165 (R : Type u) (G : Type v) [CommRing R] [Group G] :
166 Function.Exact
168 (groupAlgebraAugmentationLinearMap R G) := by
169 intro x
170 constructor
171 · intro hx
172 exact ⟨⟨x, hx⟩, rfl⟩
173 · rintro ⟨y, rfl⟩
174 exact y.2
176/-- The abstract augmentation sequence `0 → I_G → R[G] → R → 0` in `R`-linear form. -/
178 (R : Type u) (G : Type v) [CommRing R] [Group G] :
179 Function.Injective (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G) ∧
180 Function.Exact
182 (groupAlgebraAugmentationLinearMap R G) ∧
183 Function.Surjective (groupAlgebraAugmentationLinearMap R G) := by
188/-- The standard generator `g - 1` of the abstract augmentation ideal. -/
189noncomputable def groupAlgebraAugmentationGenerator
190 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
191 MonoidAlgebra R G :=
192 MonoidAlgebra.of R G g - 1
194/-- The ideal generated by the standard abstract augmentation generators `g - 1`. -/
195noncomputable def groupAlgebraAugmentationGeneratorIdeal
196 (R : Type u) (G : Type v) [CommRing R] [Group G] :
197 Ideal (MonoidAlgebra R G) :=
198 Ideal.span (Set.range (groupAlgebraAugmentationGenerator R G))
200/-- A standard abstract augmentation generator lies in the augmentation ideal. -/
202 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
203 groupAlgebraAugmentationGenerator R G g ∈ groupAlgebraAugmentationIdeal R G := by
204 simp only [groupAlgebraAugmentationGenerator, MonoidAlgebra.of_apply, mem_groupAlgebraAugmentationIdeal_iff,
205 map_sub, groupAlgebraAugmentation_single, map_one, sub_self]
207/-- A standard abstract augmentation generator lies in the ideal generated by such generators. -/
209 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
210 groupAlgebraAugmentationGenerator R G g ∈
211 groupAlgebraAugmentationGeneratorIdeal R G := by
212 exact Ideal.subset_span ⟨g, rfl⟩
214/-- The standard-generator ideal is contained in the abstract augmentation ideal. -/
216 (R : Type u) (G : Type v) [CommRing R] [Group G] :
217 groupAlgebraAugmentationGeneratorIdeal R G ≤ groupAlgebraAugmentationIdeal R G := by
218 refine Ideal.span_le.2 ?_
219 rintro _ ⟨g, rfl⟩
222/-- Every abstract group-algebra element differs from its augmentation scalar by an element of
225 (R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
226 ∃ y ∈ groupAlgebraAugmentationGeneratorIdeal R G,
227 x = y + algebraMap R (MonoidAlgebra R G) (groupAlgebraAugmentation R G x) := by
228 refine MonoidAlgebra.induction_on
229 (p := fun x : MonoidAlgebra R G =>
230 ∃ y ∈ groupAlgebraAugmentationGeneratorIdeal R G,
231 x = y + algebraMap R (MonoidAlgebra R G) (groupAlgebraAugmentation R G x))
232 x ?_ ?_ ?_
233 · intro g
234 refine
235 ⟨groupAlgebraAugmentationGenerator R G g,
238 change MonoidAlgebra.of R G g =
239 (MonoidAlgebra.of R G g - 1) +
240 algebraMap R (MonoidAlgebra R G) (1 : R)
242 rw [sub_add_cancel]
243 · intro x z hx hz
244 rcases hx with ⟨y, hy, hxy⟩
245 rcases hz with ⟨w, hw, hwz⟩
246 refine ⟨y + w, (groupAlgebraAugmentationGeneratorIdeal R G).add_mem hy hw, ?_⟩
247 have hy0 : groupAlgebraAugmentation R G y = 0 :=
248 (mem_groupAlgebraAugmentationIdeal_iff R G y).1
250 have hw0 : groupAlgebraAugmentation R G w = 0 :=
251 (mem_groupAlgebraAugmentationIdeal_iff R G w).1
254 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
255 add_left_comm, add_assoc, map_add, hy0, groupAlgebraAugmentation_single, zero_add, hw0]
256 · intro r x hx
257 rcases hx with ⟨y, hy, hxy⟩
258 refine ⟨r • y, ?_, ?_⟩
259 · have hy' :
260 algebraMap R (MonoidAlgebra R G) r * y ∈
262 (groupAlgebraAugmentationGeneratorIdeal R G).mul_mem_left _ hy
263 simpa [Algebra.smul_def] using hy'
264 · have hy0 : groupAlgebraAugmentation R G y = 0 :=
265 (mem_groupAlgebraAugmentationIdeal_iff R G y).1
267 rw [hxy, smul_add]
268 simp only [Algebra.smul_def, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id,
270 groupAlgebraAugmentation_single, hy0, mul_zero, zero_add]
272/-- The abstract augmentation ideal is generated by the standard elements `g - 1`. -/
274 (R : Type u) (G : Type v) [CommRing R] [Group G] :
275 groupAlgebraAugmentationGeneratorIdeal R G = groupAlgebraAugmentationIdeal R G := by
276 refine le_antisymm
278 intro x hx
279 rcases exists_mem_groupAlgebraAugmentationGeneratorIdeal_add R G x with ⟨y, hy, hxy⟩
280 have haug : groupAlgebraAugmentation R G x = 0 :=
281 (mem_groupAlgebraAugmentationIdeal_iff R G x).1 hx
282 rw [hxy, haug]
283 simpa using hy
285/-- The standard generators `g - 1`, viewed inside the augmentation ideal. -/
286noncomputable def groupAlgebraAugmentationGeneratorSubtype
287 (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
288 groupAlgebraAugmentationIdeal R G :=
289 ⟨groupAlgebraAugmentationGenerator R G g,
292/-- The augmentation ideal is spanned by the standard generators viewed in the ideal itself. -/
294 (R : Type u) (G : Type v) [CommRing R] [Group G] :
295 Submodule.span (MonoidAlgebra R G)
296 (Set.range (groupAlgebraAugmentationGeneratorSubtype R G)) = ⊤ := by
297 have hspan :
298 Submodule.span (MonoidAlgebra R G)
299 (Set.range fun g =>
300 (⟨groupAlgebraAugmentationGenerator R G g,
302 groupAlgebraAugmentationIdeal R G)) = ⊤ := by
303 rw [Submodule.span_range_subtype_eq_top_iff
304 (p := groupAlgebraAugmentationIdeal R G)
305 (s := groupAlgebraAugmentationGenerator R G)
307 simpa [groupAlgebraAugmentationGeneratorIdeal] using
308 congrArg
309 (fun I : Ideal (MonoidAlgebra R G) =>
310 (I : Submodule (MonoidAlgebra R G) (MonoidAlgebra R G)))
312 simpa [groupAlgebraAugmentationGeneratorSubtype] using hspan
314/-- On a finite group algebra, the augmentation is the finite sum of coordinates. -/
316 (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G]
317 (x : MonoidAlgebra R G) :
318 letI : Fintype G := Fintype.ofFinite G
319 groupAlgebraAugmentation R G x = ∑ g : G, x g := by
320 classical
321 letI : Fintype G := Fintype.ofFinite G
322 calc
323 groupAlgebraAugmentation R G x = x.sum (fun _ r => r) := by
324 simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_apply,
325 MonoidHom.one_apply, smul_eq_mul, mul_one]
326 _ = ∑ g : G, x g := by
327 exact Finsupp.sum_fintype x (fun _ r => r) (by intro g; simp only)
329/-- The coefficient inclusion into a finite-stage group algebra is continuous for the product
330topology. -/
332 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
333 [Group G] [Finite G] :
334 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
335 Continuous (algebraMap R (MonoidAlgebra R G)) := by
336 classical
337 letI : Fintype G := Fintype.ofFinite G
338 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
339 let e : MonoidAlgebra R G ≃ (G → R) := Finsupp.equivFunOnFinite
340 have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
341 Topology.IsInducing.induced e
342 rw [he.continuous_iff]
343 apply continuous_pi
344 intro g
345 change Continuous fun r : R => (algebraMap R (MonoidAlgebra R G) r) g
346 by_cases hg : g = 1
347 · subst g
348 simpa [MonoidAlgebra.coe_algebraMap] using (continuous_id : Continuous fun r : R => r)
349 · rw [show (fun r : R => (algebraMap R (MonoidAlgebra R G) r) g) =
350 (fun _ : R => 0) from by
351 funext r
352 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
353 ne_eq, hg, not_false_eq_true, Finsupp.single_eq_of_ne]]
354 exact continuous_const
356/-- The augmentation map is continuous on each finite-stage group algebra. -/
358 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
359 [Group G] [Finite G] :
360 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
361 Continuous (groupAlgebraAugmentation R G) := by
362 classical
363 letI : Fintype G := Fintype.ofFinite G
364 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
365 change Continuous (fun x : MonoidAlgebra R G => groupAlgebraAugmentation R G x)
366 rw [show (fun x : MonoidAlgebra R G => groupAlgebraAugmentation R G x) =
367 (fun x : MonoidAlgebra R G => ∑ g : G, x g) from by
368 funext x
369 exact finiteGroupAlgebra_augmentation_apply_eq_sum R G x]
370 apply continuous_finset_sum
371 intro g _hg
372 exact finiteGroupAlgebra_coordinate_continuous R G g
374/-- The augmentation is natural for the finite-stage group-algebra functor. -/
376 (R : Type u) (G : Type v) (H : Type w) [CommRing R] [Group G] [Group H]
377 (φ : G →* H) (x : MonoidAlgebra R G) :
378 groupAlgebraAugmentation R H (MonoidAlgebra.mapDomainRingHom R φ x) =
379 groupAlgebraAugmentation R G x := by
380 have hhom :
381 (groupAlgebraAugmentation R H).comp (MonoidAlgebra.mapDomainRingHom R φ) =
382 groupAlgebraAugmentation R G :=
383 MonoidAlgebra.ringHom_ext
384 (f := (groupAlgebraAugmentation R H).comp (MonoidAlgebra.mapDomainRingHom R φ))
385 (g := groupAlgebraAugmentation R G)
386 (by intro r; simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
388 MonoidAlgebra.lift_single, smul_eq_mul, mul_one])
389 (by intro g; simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
390 Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, MonoidAlgebra.lift_single,
391 MonoidHom.one_apply, smul_eq_mul, mul_one])
392 exact congrArg (fun f : MonoidAlgebra R G →+* R => f x) hhom
394/-- The augmentation is natural in the coefficient ring. -/
396 (R : Type u) (S : Type w) (G : Type v) [CommRing R] [CommRing S] [Group G]
397 (f : R →+* S) (x : MonoidAlgebra R G) :
398 groupAlgebraAugmentation S G (MonoidAlgebra.mapRangeRingHom G f x) =
399 f (groupAlgebraAugmentation R G x) := by
400 have hhom :
401 (groupAlgebraAugmentation S G).comp (MonoidAlgebra.mapRangeRingHom G f) =
402 f.comp (groupAlgebraAugmentation R G) :=
403 MonoidAlgebra.ringHom_ext
404 (f := (groupAlgebraAugmentation S G).comp (MonoidAlgebra.mapRangeRingHom G f))
405 (g := f.comp (groupAlgebraAugmentation R G))
406 (by intro r; simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
407 Function.comp_apply, MonoidAlgebra.mapRangeRingHom_single, MonoidAlgebra.lift_single, MonoidHom.one_apply,
408 smul_eq_mul, mul_one])
409 (by intro g; simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
410 Function.comp_apply, MonoidAlgebra.mapRangeRingHom_single, map_one, MonoidAlgebra.lift_single, MonoidHom.one_apply,
411 smul_eq_mul, mul_one])
412 exact congrArg (fun h : MonoidAlgebra R G →+* S => h x) hhom