CompletedGroupAlgebra/AllFiniteAugmentation/AugmentationIdeal.lean
1import CompletedGroupAlgebra.AllFiniteAugmentation.InClassComparison
2import CompletedGroupAlgebra.AllFiniteFunctoriality.Surjectivity
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/CompletedGroupAlgebra/AllFiniteAugmentation/AugmentationIdeal.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Completed group algebras
15The 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.
16-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
26open ProCGroups.Completion
28universe u v w
30variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
31variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34/-- The canonical augmentation ideal of the concrete inverse-limit completed group algebra. -/
35def completedGroupAlgebraCanonicalAugmentationIdeal (R : Type u) (G : Type v) [CommRing R]
36 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
37 [IsTopologicalGroup G] : Ideal (Carrier R G) :=
38 RingHom.ker (completedGroupAlgebraCanonicalAugmentation R G)
40/-- Membership in the all-finite canonical augmentation ideal is vanishing under the canonical augmentation. -/
41@[simp]
43 (x : Carrier R G) :
45 completedGroupAlgebraCanonicalAugmentation R G x = 0 :=
46 Iff.rfl
48/-- The inclusion of the canonical completed augmentation ideal is injective. -/
50 Function.Injective
51 (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
52 (x : Carrier R G)) := by
53 intro x y hxy
54 exact Subtype.ext hxy
56/-- The canonical completed augmentation ideal is exactly the kernel of the canonical
57augmentation. -/
59 Function.Exact
60 (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
61 (x : Carrier R G))
62 (completedGroupAlgebraCanonicalAugmentation R G) := by
63 intro x
64 constructor
65 · intro hx
66 exact ⟨⟨x, hx⟩, rfl⟩
67 · rintro ⟨y, rfl⟩
68 exact y.2
70/-- The canonical completed augmentation sequence `0 → I_G → [[R G]] → R → 0` is short
71exact. -/
73 Function.Injective
74 (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
75 (x : Carrier R G)) ∧
76 Function.Exact
77 (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
78 (x : Carrier R G))
80 Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G) := by
81 exact ⟨completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective (R := R) (G := G),
82 exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype (R := R) (G := G),
83 completedGroupAlgebraCanonicalAugmentation_surjective (R := R) (G := G)⟩
85/-- The all-finite augmentation ideal pulls back along the from-in-class comparison map to the class-indexed augmentation ideal. -/
86@[simp]
88 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
90 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
91 Ideal.comap (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)
93 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC := by
94 ext x
95 rw [Ideal.mem_comap, mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff,
100/-- The from-in-class comparison map sends the class-indexed augmentation ideal into the all-finite augmentation ideal. -/
101@[simp]
103 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
105 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
106 Ideal.map (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)
107 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC) =
110 (R := R) (G := G) C hC hForm hG]
111 exact Ideal.map_comap_of_surjective
112 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)
113 (completedGroupAlgebraFromInClass_surjective (R := R) (G := G) C hC hForm hG)
116/-- The to-in-class comparison map preserves and reflects membership in the canonical augmentation ideal. -/
117@[simp]
119 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
121 (x : Carrier R G) :
122 completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x ∈
123 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC ↔
124 x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G := by
127 have haug := congrFun
128 (congrArg DFunLike.coe
130 (R := R) (G := G) C hC))
131 x
132 change completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
133 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x) =
134 completedGroupAlgebraCanonicalAugmentation R G x at haug
135 rw [haug]
137/-- The class-indexed augmentation ideal pulls back along the to-in-class comparison map to the all-finite augmentation ideal. -/
138@[simp]
140 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
142 Ideal.comap (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
143 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC) =
145 ext x
147 (R := R) (G := G) C hC x
149/-- The to-in-class comparison map sends the all-finite augmentation ideal into the class-indexed augmentation ideal. -/
150@[simp]
152 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
154 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
155 Ideal.map (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
157 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC := by
159 (R := R) (G := G) C hC]
160 exact Ideal.map_comap_of_surjective
161 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
162 (completedGroupAlgebraToInClass_surjective (R := R) (G := G) C hC hForm hG)
163 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC)
165/-- A functorial all-finite completed group-algebra map sends augmentation generators to their images. -/
166@[simp]
168 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) (g : G) :
169 completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
170 (completedGroupAlgebraOf R G g - 1) =
171 completedGroupAlgebraOf R H (φ g) - 1 := by
172 rw [map_sub, completedGroupAlgebraMap_of, map_one]
174/-- A functorial all-finite completed group-algebra map preserves and reflects the canonical augmentation ideal when appropriate. -/
175@[simp]
177 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
178 (x : Carrier R G) :
179 completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x ∈
181 x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G := by
186/-- The canonical completed augmentation ideal is pulled back to the canonical completed
187augmentation ideal by any completed group-algebra map. -/
188@[simp]
190 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
191 Ideal.comap (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)
194 ext x
196 (R := R) (G := G) (H := H) hG φ hφ x
198/-- A surjective functorial map sends the canonical completed augmentation ideal onto the target
199canonical augmentation ideal. -/
201 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
202 (hH : ProCGroups.IsProfiniteGroup H) (φ : G →* H) (hφ : Continuous φ)
203 (hφsurj : Function.Surjective φ) :
204 Ideal.map (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)
208 (R := R) (G := G) (H := H) hG φ hφ]
209 exact Ideal.map_comap_of_surjective
210 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)
212 (R := R) (G := G) (H := H) hR hG hH φ hφ hφsurj)
214end