CompletedGroupAlgebra/Augmentation/AugmentationIdeal.lean
1import CompletedGroupAlgebra.Augmentation.CanonicalAugmentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Augmentation/AugmentationIdeal.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Augmentation and augmentation ideals
14The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.
15-/
16open scoped Topology
18namespace CompletedGroupAlgebra
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
24open ProCGroups.InverseSystems
25open ProCGroups.Completion
27universe u v w
29variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/-- The canonical augmentation ideal of the `C`-indexed completed group algebra. -/
35 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
37 Ideal (CompletedGroupAlgebraInClass C hC R G) :=
38 RingHom.ker (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC)
40/-- Membership in the in-class canonical augmentation ideal is kernel membership. -/
41@[simp]
43 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
45 (x : CompletedGroupAlgebraInClass C hC R G) :
46 x ∈ completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC ↔
47 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC x = 0 :=
48 Iff.rfl
50/-- The inclusion of the `C`-indexed canonical augmentation ideal is injective. -/
52 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
54 Function.Injective
56 (R := R) (G := G) C hC => (x : CompletedGroupAlgebraInClass C hC R G)) := by
57 intro x y hxy
58 exact Subtype.ext hxy
60/-- The `C`-indexed canonical augmentation ideal is exactly the kernel of the canonical
61augmentation. -/
63 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
65 Function.Exact
67 (R := R) (G := G) C hC => (x : CompletedGroupAlgebraInClass C hC R G))
68 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC) := by
69 intro x
70 constructor
71 · intro hx
72 exact ⟨⟨x, hx⟩, rfl⟩
73 · rintro ⟨y, rfl⟩
74 exact y.2
76/-- The `C`-indexed canonical augmentation sequence `0 → I_G → [[R G]]_C → R → 0` is
77short exact. -/
79 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
81 Function.Injective
83 (R := R) (G := G) C hC => (x : CompletedGroupAlgebraInClass C hC R G)) ∧
84 Function.Exact
86 (R := R) (G := G) C hC => (x : CompletedGroupAlgebraInClass C hC R G))
87 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC) ∧
88 Function.Surjective
89 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC) := by
91 (R := R) (G := G) C hC,
93 (R := R) (G := G) C hC,
94 completedGroupAlgebraCanonicalAugmentationInClass_surjective (R := R) (G := G) C hC⟩
96/-- The in-class canonical augmentation sends every completed group-like element to one. -/
97@[simp]
99 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
100 [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (g : G) :
101 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
102 (completedGroupAlgebraOfInClass C hC R G g) = 1 := by
105 simp only [MonoidAlgebra.of_apply, groupAlgebraAugmentation_single]
107end