CompletedGroupAlgebra/Augmentation/CanonicalAugmentation.lean
1import CompletedGroupAlgebra.Augmentation.StageAugmentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Augmentation/CanonicalAugmentation.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 value of the `C`-indexed completed augmentation, read at a finite stage. -/
35 (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
36 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
37 [IsTopologicalGroup G] (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
38 (U : CompletedGroupAlgebraIndexInClass G C) :
39 CompletedGroupAlgebraInClass C hC R G → R :=
40 fun x => completedGroupAlgebraStageAugmentationInClass C R G U
41 (completedGroupAlgebraProjectionInClass C hC R G U x)
43/-- The augmentation value read at a finer in-class stage agrees after transition. -/
44@[simp 900]
46 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
47 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
48 (x : CompletedGroupAlgebraInClass C hC R G) :
49 completedGroupAlgebraAugmentationAtInClass C R G hC U x =
50 completedGroupAlgebraAugmentationAtInClass C R G hC V x := by
52 have hcomp := congrFun
53 (congrArg DFunLike.coe
55 (R := R) (G := G) C (U := U) (V := V) hUV))
56 (completedGroupAlgebraProjectionInClass C hC R G V x)
57 calc
59 (completedGroupAlgebraProjectionInClass C hC R G U x)
60 =
62 (completedGroupAlgebraTransitionInClass C R G hUV
63 (completedGroupAlgebraProjectionInClass C hC R G V x)) := by
65 (R := R) (G := G) C hC hUV x]
66 _ =
68 (completedGroupAlgebraProjectionInClass C hC R G V x) := hcomp
70/-- The canonical augmentation on the `C`-indexed completed group algebra. -/
72 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
74 CompletedGroupAlgebraInClass C hC R G →+* R :=
76 (terminalCompletedGroupAlgebraIndexInClass (G := G) C)).comp
78 (terminalCompletedGroupAlgebraIndexInClass (G := G) C))
80/-- The in-class canonical augmentation can be computed at any in-class stage. -/
81@[simp]
83 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
85 (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
86 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC x =
87 completedGroupAlgebraAugmentationAtInClass C R G hC U x :=
88 completedGroupAlgebraAugmentationAtInClass_eq_of_le (R := R) (G := G) C hC
89 (U := terminalCompletedGroupAlgebraIndexInClass (G := G) C) (V := U)
90 (terminalCompletedGroupAlgebraIndexInClass_le (G := G) C U) x
92/-- Stage augmentation after projection is the in-class canonical augmentation. -/
93@[simp]
95 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
97 (U : CompletedGroupAlgebraIndexInClass G C) :
98 (completedGroupAlgebraStageAugmentationInClass C R G U).comp
99 (completedGroupAlgebraProjectionRingHomInClass C hC R G U) =
100 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC := by
101 apply RingHom.ext
102 intro x
104 (R := R) (G := G) C hC U x).symm
106/-- The in-class canonical augmentation extends the abstract augmentation on the dense map. -/
107@[simp]
109 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
110 [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (x : MonoidAlgebra R G) :
111 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
112 (toCompletedGroupAlgebraInClass C hC R G x) =
113 groupAlgebraAugmentation R G x := by
114 change completedGroupAlgebraStageAugmentationInClass C R G
115 (terminalCompletedGroupAlgebraIndexInClass (G := G) C)
116 (completedGroupAlgebraProjectionInClass C hC R G
117 (terminalCompletedGroupAlgebraIndexInClass (G := G) C)
118 (toCompletedGroupAlgebraInClass C hC R G x)) =
119 groupAlgebraAugmentation R G x
121 exact congrFun
122 (congrArg DFunLike.coe
124 (R := R) (G := G) C (terminalCompletedGroupAlgebraIndexInClass (G := G) C)))
125 x
127/-- Composing the dense in-class map with canonical augmentation gives abstract augmentation. -/
128@[simp]
130 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
132 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC).comp
133 (toCompletedGroupAlgebraInClassRingHom C hC R G) =
134 groupAlgebraAugmentation R G := by
135 apply RingHom.ext
136 intro x
138 (R := R) (G := G) C hC x
140/-- In-class canonical augmentation is natural in the coefficient ring. -/
141@[simp 900]
143 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
145 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
146 (f : R →+* S) :
147 (completedGroupAlgebraCanonicalAugmentationInClass (R := S) (G := G) C hC).comp
148 (completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C hC S f) =
149 f.comp (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC) := by
150 apply RingHom.ext
151 intro x
152 let U := terminalCompletedGroupAlgebraIndexInClass (G := G) C
153 change
155 (completedGroupAlgebraProjectionInClass C hC S G U
156 (completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C hC S f x)) =
157 f (completedGroupAlgebraStageAugmentationInClass C R G U
158 (completedGroupAlgebraProjectionInClass C hC R G U x))
160 exact congrFun
161 (congrArg DFunLike.coe
163 (R := R) (G := G) C S f U))
164 (completedGroupAlgebraProjectionInClass C hC R G U x)
166/-- The in-class canonical augmentation sends scalar algebra-map elements to their scalar. -/
167@[simp 900]
169 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
170 [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (r : R) :
171 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
172 (algebraMap R (CompletedGroupAlgebraInClass C hC R G) r) = r := by
173 let U := terminalCompletedGroupAlgebraIndexInClass (G := G) C
174 calc
175 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
176 (algebraMap R (CompletedGroupAlgebraInClass C hC R G) r)
177 =
179 (completedGroupAlgebraProjectionInClass C hC R G U
180 (algebraMap R (CompletedGroupAlgebraInClass C hC R G) r)) := rfl
181 _ =
183 (algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r) := by
184 change completedGroupAlgebraStageAugmentationInClass C R G U
185 (completedGroupAlgebraProjectionInClass C hC R G U
186 (completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C hC r)) =
188 (algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r)
189 exact congrArg (completedGroupAlgebraStageAugmentationInClass C R G U)
191 (R := R) (G := G) C hC U r)
192 _ = r := by
193 simp only [completedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.coe_algebraMap,
194 Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq, groupAlgebraAugmentation_single]
196/-- The in-class canonical augmentation is surjective. -/
198 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
200 Function.Surjective
201 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC) := by
202 intro r
203 refine ⟨algebraMap R (CompletedGroupAlgebraInClass C hC R G) r, ?_⟩
206/-- The `C`-indexed completed augmentation is continuous. -/
208 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
210 Continuous (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC) := by
211 let U := terminalCompletedGroupAlgebraIndexInClass (G := G) C
212 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
214 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
215 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
216 change Continuous fun x : CompletedGroupAlgebraInClass C hC R G =>
218 (completedGroupAlgebraProjectionInClass C hC R G U x)
220 (CompletedGroupAlgebraQuotientInClass G C U)).comp
221 ((completedGroupAlgebraSystemInClass C hC R G).continuous_projection U)
223/-- The `C`-indexed completed group algebra carries the standard model-independent
224augmentation package. -/
226 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
228 hasCompletedGroupAlgebraAugmentation R G (CompletedGroupAlgebraInClass C hC R G)
229 (toCompletedGroupAlgebraInClassRingHom C hC R G) := by
230 refine ⟨completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC, ?_, ?_⟩
232 (R := R) (G := G) C hC
233 · exact continuous_completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
235end