Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.Augmentation.CanonicalAugmentation
ProCGroups/CompletedGroupAlgebra/Augmentation/CanonicalAugmentation/Source

Source: ProCGroups.CompletedGroupAlgebra.Augmentation.CanonicalAugmentation

1import ProCGroups.CompletedGroupAlgebra.Augmentation.StageAugmentation
3/-!
4# Canonical augmentation of the in-class completion
6Compatible finite-stage augmentations assemble into the canonical augmentation of the in-class
7completed group algebra. This file proves its projection, coefficient-map, continuity, and
8surjectivity properties.
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 \(C\)-indexed completed augmentation evaluated at a finite stage. -/
29def completedGroupAlgebraAugmentationAtInClass
30 (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
31 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
32 [IsTopologicalGroup G]
33 (U : CompletedGroupAlgebraIndexInClass G C) :
34 CompletedGroupAlgebraInClass C R G → R :=
35 fun x => completedGroupAlgebraStageAugmentationInClass C R G U
36 (completedGroupAlgebraProjectionInClass C R G U x)
38/-- The augmentation value read at a finer in-class stage agrees after transition. -/
39@[simp 900]
40theorem completedGroupAlgebraAugmentationAtInClass_eq_of_le
41 (C : ProCGroups.FiniteGroupClass.{v})
42 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
43 (x : CompletedGroupAlgebraInClass C R G) :
44 completedGroupAlgebraAugmentationAtInClass C R G U x =
45 completedGroupAlgebraAugmentationAtInClass C R G V x := by
46 unfold completedGroupAlgebraAugmentationAtInClass
47 have hcomp := congrFun
48 (congrArg DFunLike.coe
49 (completedGroupAlgebraStageAugmentationInClass_compatible
50 (R := R) (G := G) C (U := U) (V := V) hUV))
51 (completedGroupAlgebraProjectionInClass C R G V x)
52 calc
53 completedGroupAlgebraStageAugmentationInClass C R G U
54 (completedGroupAlgebraProjectionInClass C R G U x)
55 =
56 completedGroupAlgebraStageAugmentationInClass C R G U
57 (completedGroupAlgebraTransitionInClass C R G hUV
58 (completedGroupAlgebraProjectionInClass C R G V x)) := by
59 rw [← completedGroupAlgebraProjectionInClass_compatible
60 (R := R) (G := G) C hUV x]
61 _ =
62 completedGroupAlgebraStageAugmentationInClass C R G V
63 (completedGroupAlgebraProjectionInClass C R G V x) := hcomp
65/-- The canonical augmentation on the \(C\)-indexed completed group algebra. -/
66def completedGroupAlgebraCanonicalAugmentationInClass
67 (C : ProCGroups.FiniteGroupClass.{v})
69 CompletedGroupAlgebraInClass C R G →+* R :=
70 (completedGroupAlgebraStageAugmentationInClass C R G
71 (terminalCompletedGroupAlgebraIndexInClass (G := G) C)).comp
72 (completedGroupAlgebraProjectionInClass C R G
73 (terminalCompletedGroupAlgebraIndexInClass (G := G) C))
75/-- The in-class canonical augmentation can be computed at any in-class stage. -/
76@[simp]
77theorem completedGroupAlgebraCanonicalAugmentationInClass_eq_at
78 (C : ProCGroups.FiniteGroupClass.{v})
80 (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C R G) :
81 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x =
82 completedGroupAlgebraAugmentationAtInClass C R G U x :=
83 completedGroupAlgebraAugmentationAtInClass_eq_of_le (R := R) (G := G) C
84 (U := terminalCompletedGroupAlgebraIndexInClass (G := G) C) (V := U)
85 (terminalCompletedGroupAlgebraIndexInClass_le (G := G) C U) x
87/-- Stage augmentation after projection is the in-class canonical augmentation. -/
88@[simp]
89theorem completedGroupAlgebraStageAugmentationInClass_comp_projectionInClass
90 (C : ProCGroups.FiniteGroupClass.{v})
92 (U : CompletedGroupAlgebraIndexInClass G C) :
93 (completedGroupAlgebraStageAugmentationInClass C R G U).comp
94 (completedGroupAlgebraProjectionInClass C R G U) =
95 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C := by
96 apply RingHom.ext
97 intro x
98 exact (completedGroupAlgebraCanonicalAugmentationInClass_eq_at
99 (R := R) (G := G) C U x).symm
101/--
102The in-class canonical augmentation extends the abstract augmentation on the dense algebraic
103map.
104-/
105@[simp]
106theorem canonicalAugmentationInClass_toCompleted
107 (C : ProCGroups.FiniteGroupClass.{v})
109 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
110 (toCompletedGroupAlgebraInClass C R G x) =
111 groupAlgebraAugmentation R G x := by
112 change completedGroupAlgebraStageAugmentationInClass C R G
113 (terminalCompletedGroupAlgebraIndexInClass (G := G) C)
114 (completedGroupAlgebraProjectionInClass C R G
115 (terminalCompletedGroupAlgebraIndexInClass (G := G) C)
116 (toCompletedGroupAlgebraInClass C R G x)) =
117 groupAlgebraAugmentation R G x
118 rw [completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass]
119 exact congrFun
120 (congrArg DFunLike.coe
121 (completedGroupAlgebraStageAugmentationInClass_comp_stageMapInClass
122 (R := R) (G := G) C (terminalCompletedGroupAlgebraIndexInClass (G := G) C)))
123 x
125/-- Composing the dense in-class map with canonical augmentation gives abstract augmentation. -/
126@[simp]
127theorem completedGACanonicalAugmentationInClass_comp_toCompletedGAInClass
128 (C : ProCGroups.FiniteGroupClass.{v})
130 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ).comp
131 (toCompletedGroupAlgebraInClassRingHom C R G) =
132 groupAlgebraAugmentation R G := by
133 apply RingHom.ext
134 intro x
135 exact canonicalAugmentationInClass_toCompleted
136 (R := R) (G := G) C x
138/-- In-class canonical augmentation is natural in the coefficient ring. -/
139@[simp 900]
140theorem completedGroupAlgebraCanonicalAugmentationInClass_comp_coeffMapInClass
141 (C : ProCGroups.FiniteGroupClass.{v})
143 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
144 (f : R →+* S) :
145 (completedGroupAlgebraCanonicalAugmentationInClass (R := S) (G := G) C ).comp
146 (completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C S f) =
147 f.comp (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ) := by
148 apply RingHom.ext
149 intro x
150 let U := terminalCompletedGroupAlgebraIndexInClass (G := G) C
151 change
152 completedGroupAlgebraStageAugmentationInClass C S G U
153 (completedGroupAlgebraProjectionInClass C S G U
154 (completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C S f x)) =
155 f (completedGroupAlgebraStageAugmentationInClass C R G U
156 (completedGroupAlgebraProjectionInClass C R G U x))
157 rw [completedGroupAlgebraProjectionInClass_coeffMap]
158 exact congrFun
159 (congrArg DFunLike.coe
160 (completedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMapInClass
161 (R := R) (G := G) C S f U))
162 (completedGroupAlgebraProjectionInClass C R G U x)
164/-- The in-class canonical augmentation sends scalar algebra-map elements to their scalar. -/
165@[simp 900]
166theorem completedGroupAlgebraCanonicalAugmentationInClass_algebraMap
167 (C : ProCGroups.FiniteGroupClass.{v})
169 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
170 (algebraMap R (CompletedGroupAlgebraInClass C R G) r) = r := by
171 let U := terminalCompletedGroupAlgebraIndexInClass (G := G) C
172 calc
173 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
174 (algebraMap R (CompletedGroupAlgebraInClass C R G) r)
175 =
176 completedGroupAlgebraStageAugmentationInClass C R G U
177 (completedGroupAlgebraProjectionInClass C R G U
178 (algebraMap R (CompletedGroupAlgebraInClass C R G) r)) := rfl
179 _ =
180 completedGroupAlgebraStageAugmentationInClass C R G U
181 (algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r) := by
182 change completedGroupAlgebraStageAugmentationInClass C R G U
183 (completedGroupAlgebraProjectionInClass C R G U
184 (completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C r)) =
185 completedGroupAlgebraStageAugmentationInClass C R G U
186 (algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r)
187 exact congrArg (completedGroupAlgebraStageAugmentationInClass C R G U)
188 (completedGroupAlgebraProjectionInClass_algebraMap
189 (R := R) (G := G) C U r)
190 _ = r := by
191 simp only [completedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.coe_algebraMap,
192 Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
193 groupAlgebraAugmentation_single]
195/--
196The \(C\)-indexed canonical augmentation \(\varepsilon_C:\widehat{R[G]}_C\to R\) is surjective.
197-/
198theorem completedGroupAlgebraCanonicalAugmentationInClass_surjective
199 (C : ProCGroups.FiniteGroupClass.{v})
201 Function.Surjective
202 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ) := by
203 intro r
204 refine ⟨algebraMap R (CompletedGroupAlgebraInClass C R G) r, ?_⟩
205 simp only [completedGroupAlgebraCanonicalAugmentationInClass_algebraMap]
207/--
208The \(C\)-indexed canonical augmentation is continuous for the inverse-limit topology on
209\(\widehat{R[G]}_C\).
210-/
211theorem continuous_completedGroupAlgebraCanonicalAugmentationInClass
212 (C : ProCGroups.FiniteGroupClass.{v})
214 Continuous (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ) := by
215 let U := terminalCompletedGroupAlgebraIndexInClass (G := G) C
216 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
217 finite_completedGroupAlgebraQuotientInClass G C U
218 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
219 (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
220 change Continuous fun x : CompletedGroupAlgebraInClass C R G =>
221 completedGroupAlgebraStageAugmentationInClass C R G U
222 (completedGroupAlgebraProjectionInClass C R G U x)
223 exact (finiteGroupAlgebra_augmentation_continuous R
224 (CompletedGroupAlgebraQuotientInClass G C U)).comp
225 ((completedGroupAlgebraSystemInClass C R G).continuous_projection U)
227/--
228The \(C\)-indexed completed group algebra carries the standard model-independent augmentation
229package.
230-/
231theorem completedGroupAlgebraInClass_hasCompletedGroupAlgebraAugmentation
232 (C : ProCGroups.FiniteGroupClass.{v})
234 hasCompletedGroupAlgebraAugmentation R G (CompletedGroupAlgebraInClass C R G)
235 (toCompletedGroupAlgebraInClassRingHom C R G) := by
236 refine ⟨completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C , ?_, ?_⟩
237 · exact completedGACanonicalAugmentationInClass_comp_toCompletedGAInClass
238 (R := R) (G := G) C
239 · exact continuous_completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
241end
243end CompletedGroupAlgebra