Source: ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.CanonicalAugmentation
1import ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.StageAugmentation
3/-!
4# Completed Group Algebra / All Finite Augmentation / Canonical Augmentation
6This module defines the all-finite canonical augmentation as the composition of a terminal
7finite-stage augmentation with the canonical bundled projection, and proves that it can be
8computed at every finite stage.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
20open ProCGroups.Completion
22universe u v w
24variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
25variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
26variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
28/-- The completed augmentation evaluated at a finite stage. -/
29def completedGroupAlgebraAugmentationAt (R : Type u) (G : Type v) [CommRing R]
30 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
31 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
32 CompletedGroupAlgebraCarrier R G → R :=
33 fun x => completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)
35/--
36The coordinate defining the completed augmentation is independent of the chosen sufficiently
37terminal index.
38-/
39@[simp]
40theorem completedGroupAlgebraAugmentationAt_eq_of_le
41 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (x : CompletedGroupAlgebraCarrier R G) :
42 completedGroupAlgebraAugmentationAt R G U x =
43 completedGroupAlgebraAugmentationAt R G V x := by
44 unfold completedGroupAlgebraAugmentationAt
45 have hcomp := congrFun
46 (congrArg DFunLike.coe
47 (completedGroupAlgebraStageAugmentation_compatible (R := R) (G := G)
48 (U := U) (V := V) hUV))
49 (completedGroupAlgebraProjection R G V x)
50 calc
51 completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)
52 =
53 completedGroupAlgebraStageAugmentation R G U
54 (completedGroupAlgebraTransition R G hUV (completedGroupAlgebraProjection R G V x)) := by
55 rw [← completedGroupAlgebraProjection_compatible (R := R) (G := G) x hUV]
56 _ = completedGroupAlgebraStageAugmentation R G V
57 (completedGroupAlgebraProjection R G V x) := hcomp
59/--
60The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is the ring homomorphism obtained
61by applying the finite-stage augmentation to any sufficiently terminal coordinate.
62-/
63def completedGroupAlgebraCanonicalAugmentation (R : Type u) (G : Type v) [CommRing R]
64 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
65 [IsTopologicalGroup G] :
66 CompletedGroupAlgebraCarrier R G →+* R :=
67 (completedGroupAlgebraStageAugmentation R G
68 (terminalCompletedGroupAlgebraIndex G)).comp
69 (completedGroupAlgebraProjection R G
70 (terminalCompletedGroupAlgebraIndex G))
72/-- The canonical completed augmentation is computed at any finite stage. -/
73@[simp]
74theorem completedGroupAlgebraCanonicalAugmentation_eq_at
75 (U : CompletedGroupAlgebraIndex G) (x : CompletedGroupAlgebraCarrier R G) :
76 completedGroupAlgebraCanonicalAugmentation R G x =
77 completedGroupAlgebraAugmentationAt R G U x :=
78 completedGroupAlgebraAugmentationAt_eq_of_le (R := R) (G := G)
79 (U := terminalCompletedGroupAlgebraIndex G) (V := U)
80 (terminalCompletedGroupAlgebraIndex_le (G := G) U) x
82/--
83For every finite quotient stage \(U\), projecting \(\widehat{R[G]}\) to \(R[G/U]\) and then
84applying the finite-stage augmentation gives the canonical augmentation on \(\widehat{R[G]}\).
85-/
86@[simp]
87theorem completedGroupAlgebraStageAugmentation_comp_projection
88 (U : CompletedGroupAlgebraIndex G) :
89 (completedGroupAlgebraStageAugmentation R G U).comp
90 (completedGroupAlgebraProjection R G U) =
91 completedGroupAlgebraCanonicalAugmentation R G := by
92 apply RingHom.ext
93 intro x
94 exact (completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := G) U x).symm
96/--
97The canonical augmentation extends the abstract group-algebra augmentation through the dense
98algebraic map.
99-/
100@[simp]
101theorem completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra
102 (x : MonoidAlgebra R G) :
103 completedGroupAlgebraCanonicalAugmentation R G (toCompletedGroupAlgebra R G x) =
104 groupAlgebraAugmentation R G x := by
105 change completedGroupAlgebraStageAugmentation R G (terminalCompletedGroupAlgebraIndex G)
106 (completedGroupAlgebraProjection R G (terminalCompletedGroupAlgebraIndex G)
107 (toCompletedGroupAlgebra R G x)) = groupAlgebraAugmentation R G x
108 rw [completedGroupAlgebraProjection_toCompletedGroupAlgebra]
109 exact congrFun
110 (congrArg DFunLike.coe
111 (completedGroupAlgebraStageAugmentation_comp_stageMap (R := R) (G := G)
112 (terminalCompletedGroupAlgebraIndex G)))
113 x
115/-- Composing the canonical augmentation with the dense map gives the abstract augmentation. -/
116@[simp]
117theorem completedGroupAlgebraCanonicalAugmentation_comp_toCompletedGroupAlgebra :
118 (completedGroupAlgebraCanonicalAugmentation R G).comp
119 (toCompletedGroupAlgebraRingHom R G) =
120 groupAlgebraAugmentation R G := by
121 apply RingHom.ext
122 intro x
123 exact completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra (R := R) (G := G) x
125/-- Canonical augmentation is natural in the coefficient ring. -/
126@[simp]
127theorem completedGroupAlgebraCanonicalAugmentation_comp_coeffMap
128 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
129 (f : R →+* S) :
130 (completedGroupAlgebraCanonicalAugmentation S G).comp
131 (completedGroupAlgebraCoeffMap (R := R) (G := G) S f) =
132 f.comp (completedGroupAlgebraCanonicalAugmentation R G) := by
133 apply RingHom.ext
134 intro x
135 change
136 completedGroupAlgebraStageAugmentation S G (terminalCompletedGroupAlgebraIndex G)
137 (completedGroupAlgebraProjection S G (terminalCompletedGroupAlgebraIndex G)
138 (completedGroupAlgebraCoeffMap (R := R) (G := G) S f x)) =
139 f (completedGroupAlgebraStageAugmentation R G (terminalCompletedGroupAlgebraIndex G)
140 (completedGroupAlgebraProjection R G (terminalCompletedGroupAlgebraIndex G) x))
141 rw [completedGroupAlgebraProjection_coeffMap]
142 exact congrFun
143 (congrArg DFunLike.coe
144 (completedGroupAlgebraStageAugmentation_comp_stageCoeffMap
145 (R := R) (G := G) S f (terminalCompletedGroupAlgebraIndex G)))
146 (completedGroupAlgebraProjection R G (terminalCompletedGroupAlgebraIndex G) x)
148/-- Canonical augmentation is natural with respect to functorial completed group-algebra maps. -/
149@[simp 900]
150theorem completedGroupAlgebraCanonicalAugmentation_map
151 (φ : G →* H) (hφ : Continuous φ)
152 (x : CompletedGroupAlgebraCarrier R G) :
153 completedGroupAlgebraCanonicalAugmentation R H
154 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x) =
155 completedGroupAlgebraCanonicalAugmentation R G x := by
156 let V : CompletedGroupAlgebraIndex H := terminalCompletedGroupAlgebraIndex H
157 calc
158 completedGroupAlgebraCanonicalAugmentation R H
159 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x)
160 =
161 completedGroupAlgebraAugmentationAt R H V
162 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x) := by
163 exact completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := H) V
164 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x)
165 _ =
166 completedGroupAlgebraStageAugmentation R H V
167 (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V
168 (completedGroupAlgebraProjection R G
169 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x)) := by
170 rw [completedGroupAlgebraAugmentationAt, completedGroupAlgebraProjection_map]
171 _ =
172 completedGroupAlgebraStageAugmentation R G
173 (completedGroupAlgebraComapIndex (G := G) φ hφ V)
174 (completedGroupAlgebraProjection R G
175 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x) := by
176 have hstage := congrFun
177 (congrArg DFunLike.coe
178 (completedGroupAlgebraStageAugmentation_comp_functorialStageMap
179 (R := R) (G := G) (H := H) φ hφ V))
180 (completedGroupAlgebraProjection R G
181 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x)
182 exact hstage
183 _ =
184 completedGroupAlgebraCanonicalAugmentation R G x := by
185 exact (completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := G)
186 (completedGroupAlgebraComapIndex (G := G) φ hφ V) x).symm
188/-- Canonical augmentation after the functorial completed map agrees with canonical augmentation. -/
189@[simp]
190theorem completedGroupAlgebraCanonicalAugmentation_comp_map
191 (φ : G →* H) (hφ : Continuous φ) :
192 (completedGroupAlgebraCanonicalAugmentation R H).comp
193 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ) =
194 completedGroupAlgebraCanonicalAugmentation R G := by
195 apply RingHom.ext
196 intro x
197 exact completedGroupAlgebraCanonicalAugmentation_map (R := R) (G := G) (H := H) φ hφ x
199/-- The canonical augmentation sends every completed group-like element to one. -/
200@[simp]
201theorem completedGroupAlgebraCanonicalAugmentation_of (g : G) :
202 completedGroupAlgebraCanonicalAugmentation R G (completedGroupAlgebraOf R G g) = 1 := by
203 rw [completedGroupAlgebraOf,
204 completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra]
205 simp only [MonoidAlgebra.of_apply, groupAlgebraAugmentation_single]
207/-- The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is surjective. -/
208theorem completedGroupAlgebraCanonicalAugmentation_surjective :
209 Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G) := by
210 intro r
211 refine ⟨toCompletedGroupAlgebra R G (algebraMap R (MonoidAlgebra R G) r), ?_⟩
212 rw [completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra]
213 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id,
214 Function.comp_apply, id_eq,
215 groupAlgebraAugmentation_single]
217/--
218The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is continuous for the
219inverse-limit topology on \(\widehat{R[G]}\).
220-/
221theorem continuous_completedGroupAlgebraCanonicalAugmentation :
222 Continuous (completedGroupAlgebraCanonicalAugmentation R G) := by
223 let U := terminalCompletedGroupAlgebraIndex G
224 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
225 (completedGroupAlgebraSystem R G).topologicalSpace U
226 change Continuous fun x : CompletedGroupAlgebraCarrier R G =>
227 completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)
228 exact (finiteGroupAlgebra_augmentation_continuous R (CompletedGroupAlgebraQuotient G U)).comp
229 ((completedGroupAlgebraSystem R G).continuous_projection U)
231end
233end CompletedGroupAlgebra