CompletedGroupAlgebra/AllFiniteAugmentation/CanonicalAugmentation.lean
1import CompletedGroupAlgebra.AllFiniteAugmentation.StageAugmentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/AllFiniteAugmentation/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# Completed group algebras
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 completed augmentation, read at a finite stage. -/
34def completedGroupAlgebraAugmentationAt (R : Type u) (G : Type v) [CommRing R]
35 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
36 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
37 Carrier R G → R :=
38 fun x => completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)
40/-- The coordinate defining the completed augmentation is independent of the chosen sufficiently terminal index. -/
41@[simp]
43 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (x : Carrier R G) :
44 completedGroupAlgebraAugmentationAt R G U x =
45 completedGroupAlgebraAugmentationAt R G V x := by
47 have hcomp := congrFun
48 (congrArg DFunLike.coe
49 (completedGroupAlgebraStageAugmentation_compatible (R := R) (G := G)
50 (U := U) (V := V) hUV))
51 (completedGroupAlgebraProjection R G V x)
52 calc
53 completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)
54 =
56 (completedGroupAlgebraTransition R G hUV (completedGroupAlgebraProjection R G V x)) := by
57 rw [← completedGroupAlgebraProjection_compatible (R := R) (G := G) x hUV]
58 _ = completedGroupAlgebraStageAugmentation R G V
59 (completedGroupAlgebraProjection R G V x) := hcomp
61/-- The canonical augmentation on `[[R G]]`, obtained from the compatible finite-stage
62augmentations. This is the fixed-coefficient analogue of the map used in RZ §6.3. -/
63def completedGroupAlgebraCanonicalAugmentation (R : Type u) (G : Type v) [CommRing R]
64 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
65 [IsTopologicalGroup G] :
66 Carrier R G →+* R where
67 toFun := completedGroupAlgebraAugmentationAt R G (terminalCompletedGroupAlgebraIndex G)
68 map_zero' := by
70 simp only [InverseSystem.projection_apply, coe_zero_completedGroupAlgebra, Pi.zero_apply, map_zero]
71 map_one' := by
73 simp only [InverseSystem.projection_apply, coe_one_completedGroupAlgebra, Pi.one_apply, map_one]
74 map_add' x y := by
76 simp only [InverseSystem.projection_apply, coe_add_completedGroupAlgebra, Pi.add_apply, map_add]
77 map_mul' x y := by
79 simp only [InverseSystem.projection_apply, coe_mul_completedGroupAlgebra, Pi.mul_apply, map_mul]
81/-- The canonical completed augmentation is computed at any finite stage. -/
82@[simp]
84 (U : CompletedGroupAlgebraIndex G) (x : Carrier R G) :
86 completedGroupAlgebraAugmentationAt R G U x :=
87 completedGroupAlgebraAugmentationAt_eq_of_le (R := R) (G := G)
88 (U := terminalCompletedGroupAlgebraIndex G) (V := U)
89 (terminalCompletedGroupAlgebraIndex_le (G := G) U) x
91/-- The completed projection followed by finite-stage augmentation is the canonical augmentation. -/
92@[simp]
94 (U : CompletedGroupAlgebraIndex G) :
95 (completedGroupAlgebraStageAugmentation R G U).comp
96 (completedGroupAlgebraProjectionRingHom R G U) =
97 completedGroupAlgebraCanonicalAugmentation R G := by
98 apply RingHom.ext
99 intro x
100 exact (completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := G) U x).symm
102/-- The canonical augmentation extends the abstract group-algebra augmentation through the dense map. -/
103@[simp]
105 (x : MonoidAlgebra R G) :
107 groupAlgebraAugmentation R G x := by
110 (toCompletedGroupAlgebra R G x)) = groupAlgebraAugmentation R G x
112 exact congrFun
113 (congrArg DFunLike.coe
114 (completedGroupAlgebraStageAugmentation_comp_stageMap (R := R) (G := G)
116 x
118/-- The canonical augmentation composed with the dense map is the abstract augmentation. -/
119@[simp]
121 (completedGroupAlgebraCanonicalAugmentation R G).comp
122 (toCompletedGroupAlgebraRingHom R G) =
123 groupAlgebraAugmentation R G := by
124 apply RingHom.ext
125 intro x
126 exact completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra (R := R) (G := G) x
128/-- Canonical augmentation is natural in the coefficient ring. -/
129@[simp]
131 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
132 (f : R →+* S) :
133 (completedGroupAlgebraCanonicalAugmentation S G).comp
134 (completedGroupAlgebraCoeffMap (R := R) (G := G) S f) =
135 f.comp (completedGroupAlgebraCanonicalAugmentation R G) := by
136 apply RingHom.ext
137 intro x
138 change
141 (completedGroupAlgebraCoeffMap (R := R) (G := G) S f x)) =
145 exact congrFun
146 (congrArg DFunLike.coe
148 (R := R) (G := G) S f (terminalCompletedGroupAlgebraIndex G)))
151/-- Canonical augmentation is natural with respect to functorial completed group-algebra maps. -/
152@[simp 900]
154 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
155 (x : Carrier R G) :
157 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x) =
158 completedGroupAlgebraCanonicalAugmentation R G x := by
159 let V : CompletedGroupAlgebraIndex H := terminalCompletedGroupAlgebraIndex H
160 calc
162 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x)
163 =
165 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x) := by
166 exact completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := H) V
167 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x)
168 _ =
170 (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
172 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)) := by
174 _ =
176 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)
178 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x) := by
179 have hstage := congrFun
180 (congrArg DFunLike.coe
182 (R := R) (G := G) (H := H) hG φ hφ V))
184 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
185 exact hstage
186 _ =
187 completedGroupAlgebraCanonicalAugmentation R G x := by
188 exact (completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := G)
189 (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x).symm
191/-- Canonical augmentation after a functorial completed map agrees with canonical augmentation. -/
192@[simp]
194 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
195 (completedGroupAlgebraCanonicalAugmentation R H).comp
196 (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ) =
198 apply RingHom.ext
199 intro x
200 exact completedGroupAlgebraCanonicalAugmentation_map (R := R) (G := G) (H := H) hG φ hφ x
202/-- The canonical augmentation sends every completed group-like element to one. -/
203@[simp]
204theorem completedGroupAlgebraCanonicalAugmentation_of (g : G) :
205 completedGroupAlgebraCanonicalAugmentation R G (completedGroupAlgebraOf R G g) = 1 := by
208 simp only [MonoidAlgebra.of_apply, groupAlgebraAugmentation_single]
210/-- The canonical completed augmentation is surjective. -/
212 Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G) := by
213 intro r
214 refine ⟨toCompletedGroupAlgebra R G (algebraMap R (MonoidAlgebra R G) r), ?_⟩
216 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
219/-- The canonical completed augmentation is continuous. -/
221 Continuous (completedGroupAlgebraCanonicalAugmentation R G) := by
222 let U := terminalCompletedGroupAlgebraIndex G
223 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
224 (completedGroupAlgebraSystem R G).topologicalSpace U
225 change Continuous fun x : Carrier R G =>
226 completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)
227 exact (finiteGroupAlgebra_augmentation_continuous R (CompletedGroupAlgebraQuotient G U)).comp
228 ((completedGroupAlgebraSystem R G).continuous_projection U)
230end