Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation
3/-!
4# Fox differential: completed — coefficient rings — mod-\(n\) completed group algebra — augmentation ideal
6The principal declarations in this module are:
8- `modNCompletedGroupAlgebraStageAugmentationIdeal`
9 The augmentation ideal on one residue-coefficient finite stage.
10- `modNCompletedGroupAlgebraAugmentationKernel`
11 The kernel of the canonical augmentation on the residue-coefficient completed group algebra.
12- `mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff`
13 Membership in a mod-\(N\) finite-stage augmentation ideal is equivalent to vanishing under the
14 stage augmentation map.
15- `mem_modNCompletedGroupAlgebraAugmentationKernel_iff`
16 Membership in the relevant augmentation kernel or augmentation ideal is equivalent to the
17 corresponding vanishing condition.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
25open ProCGroups.ProC
27universe u
30variable (n : ℕ) [Fact (0 < n)]
31variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33section AugmentationIdeal
35variable (n : ℕ) [Fact (0 < n)]
36variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
38/-- The augmentation ideal on one residue-coefficient finite stage. -/
39def modNCompletedGroupAlgebraStageAugmentationIdeal (U :
40 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
41 Ideal (ModNCompletedGroupAlgebraStage n G U) :=
42 RingHom.ker (modNCompletedGroupAlgebraStageAugmentation n G U)
44/-- The kernel of the canonical augmentation on the residue-coefficient completed group algebra. -/
45def modNCompletedGroupAlgebraAugmentationKernel :
46 Set (ModNCompletedGroupAlgebra n G) :=
47 {x | modNCompletedGroupAlgebraAugmentation n G x = 0}
49/-- The kernel of the canonical augmentation is viewed as a subtype. -/
50abbrev ModNCompletedGroupAlgebraAugmentationKernel :=
51 {x : ModNCompletedGroupAlgebra n G // x ∈ modNCompletedGroupAlgebraAugmentationKernel n G}
53omit [Fact (0 < n)] in
54variable {n G} in
55/--
56Membership in a mod-\(N\) finite-stage augmentation ideal is equivalent to vanishing under the
57stage augmentation map.
58-/
59@[simp]
60theorem mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff
61 {U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} {x :
62 ModNCompletedGroupAlgebraStage n G U} :
63 x ∈ modNCompletedGroupAlgebraStageAugmentationIdeal n G U ↔
64 modNCompletedGroupAlgebraStageAugmentation n G U x = 0 := by
65 rw [modNCompletedGroupAlgebraStageAugmentationIdeal, RingHom.mem_ker]
67omit [Fact (0 < n)] in
68variable {n G} in
69/--
70Membership in the relevant augmentation kernel or augmentation ideal is equivalent to the
71corresponding vanishing condition.
72-/
73@[simp]
74theorem mem_modNCompletedGroupAlgebraAugmentationKernel_iff
75 {x : ModNCompletedGroupAlgebra n G} :
76 x ∈ modNCompletedGroupAlgebraAugmentationKernel n G ↔
77 modNCompletedGroupAlgebraAugmentation n G x = 0 := by
78 rfl
80omit [Fact (0 < n)] in
81variable {n G} in
82/--
83A mod-\(N\) completed group-algebra element projects into the stage augmentation ideal iff it
84lies in the completed augmentation kernel.
85-/
86@[simp]
87theorem mem_modNCompletedGroupAlgebraProjection_stageAugmentationIdeal_iff
88 {U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} {x :
89 ModNCompletedGroupAlgebra n G} :
90 modNCompletedGroupAlgebraProjection n G U x ∈
91 modNCompletedGroupAlgebraStageAugmentationIdeal n G U ↔
92 x ∈ modNCompletedGroupAlgebraAugmentationKernel n G := by
93 rw [mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff,
94 mem_modNCompletedGroupAlgebraAugmentationKernel_iff]
95 change modNCompletedGroupAlgebraAugmentationAt n G U x = 0 ↔
96 modNCompletedGroupAlgebraAugmentation n G x = 0
97 rw [modNCompletedGroupAlgebraAugmentation_eq_at (n := n) (G := G) U x]
99/-- The transition maps on the residue-coefficient finite-stage augmentation ideals. -/
100def modNCompletedGroupAlgebraStageAugmentationIdealTransition
101 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
102 modNCompletedGroupAlgebraStageAugmentationIdeal n G V →
103 modNCompletedGroupAlgebraStageAugmentationIdeal n G U :=
104 fun x => ⟨modNCompletedGroupAlgebraTransition n G hUV x.1, by
105 rw [mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff]
106 have hcomp := congrFun
107 (congrArg DFunLike.coe
108 (modNCompletedGroupAlgebraStageAugmentation_compatible
109 (n := n) (G := G) (U := U) (V := V) hUV))
110 x.1
111 rw [RingHom.comp_apply] at hcomp
112 exact hcomp.trans
113 ((mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff
114 (n := n) (G := G) (U := V) (x := x.1)).1 x.2)⟩
116omit [Fact (0 < n)] in
117/--
118The transition map between finite-stage augmentation ideals is evaluated by the corresponding
119stage transition.
120-/
121@[simp]
122theorem modNCompletedGroupAlgebraStageAugmentationIdealTransition_val
123 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
124 (x : modNCompletedGroupAlgebraStageAugmentationIdeal n G V) :
125 ((modNCompletedGroupAlgebraStageAugmentationIdealTransition
126 (n := n) (G := G) hUV x : modNCompletedGroupAlgebraStageAugmentationIdeal n G U) :
127 ModNCompletedGroupAlgebraStage n G U) =
128 modNCompletedGroupAlgebraTransition n G hUV x.1 := rfl
130/-- The inverse system of residue-coefficient finite-stage augmentation ideals. -/
131def modNCompletedGroupAlgebraAugmentationIdealSystem :
132 InverseSystem (I := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) where
133 X := fun U => ↥(modNCompletedGroupAlgebraStageAugmentationIdeal n G U)
134 topologicalSpace := fun _ => ⊥
135 map := fun {U V} hUV => modNCompletedGroupAlgebraStageAugmentationIdealTransition
136 (n := n) (G := G) hUV
137 continuous_map := by
138 intro U V hUV
139 letI : TopologicalSpace (modNCompletedGroupAlgebraStageAugmentationIdeal n G U) := ⊥
140 letI : TopologicalSpace (modNCompletedGroupAlgebraStageAugmentationIdeal n G V) := ⊥
141 letI : DiscreteTopology (modNCompletedGroupAlgebraStageAugmentationIdeal n G V) := ⟨rfl⟩
142 exact continuous_of_discreteTopology
143 map_id := by
144 intro U
145 funext x
146 apply Subtype.ext
147 exact congrFun
148 (congrArg DFunLike.coe (modNCompletedGroupAlgebraTransition_id (n := n) (G := G) U))
149 x.1
150 map_comp := by
151 intro U V W hUV hVW
152 funext x
153 apply Subtype.ext
154 exact congrFun
155 (congrArg DFunLike.coe
156 (modNCompletedGroupAlgebraTransition_comp (n := n) (G := G) hUV hVW))
157 x.1
159/-- The inverse-limit object of the residue-coefficient finite-stage augmentation ideals. -/
160abbrev ModNCompletedGroupAlgebraAugmentationIdeal :=
161 (modNCompletedGroupAlgebraAugmentationIdealSystem n G).inverseLimit
163/-- The projection from the residue-coefficient augmentation-ideal inverse limit to one stage. -/
164abbrev modNCompletedGroupAlgebraAugmentationIdealProjection (U :
165 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
166 ModNCompletedGroupAlgebraAugmentationIdeal n G →
167 modNCompletedGroupAlgebraStageAugmentationIdeal n G U :=
168 (modNCompletedGroupAlgebraAugmentationIdealSystem n G).projection U
170/--
171A residue-coefficient augmentation-kernel point determines a compatible family in the
172finite-stage augmentation ideals.
173-/
174def toModNCompletedGroupAlgebraAugmentationIdeal :
175 ModNCompletedGroupAlgebraAugmentationKernel n G →
176 ModNCompletedGroupAlgebraAugmentationIdeal n G := by
177 intro x
178 refine ⟨fun U => ⟨modNCompletedGroupAlgebraProjection n G U x.1, ?_⟩, ?_⟩
179 · exact (mem_modNCompletedGroupAlgebraProjection_stageAugmentationIdeal_iff
180 (n := n) (G := G) (U := U) (x := x.1)).2
181 ((mem_modNCompletedGroupAlgebraAugmentationKernel_iff
182 (n := n) (G := G) (x := x.1)).1 x.2)
183 · intro U V hUV
184 apply Subtype.ext
185 exact (modNCompletedGroupAlgebraSystem n G).projection_compatible x.1 U V hUV
187omit [Fact (0 < n)] in
188/--
189The projection-to-stage map is one direction of the completed augmentation-ideal stage
190equivalence.
191-/
192@[simp]
193theorem modNCompletedGroupAlgebraAugmentationIdealProjection_to
194 (x : ModNCompletedGroupAlgebraAugmentationKernel n G) (U :
195 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
196 ((modNCompletedGroupAlgebraAugmentationIdealProjection (n := n) (G := G) U
197 (toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x)) :
198 ModNCompletedGroupAlgebraStage n G U) =
199 modNCompletedGroupAlgebraProjection n G U x.1 := rfl
201/--
202A compatible family of finite-stage augmentation-ideal elements determines a residue-coefficient
203completed augmentation-kernel point.
204-/
205def ofModNCompletedGroupAlgebraAugmentationIdeal :
206 ModNCompletedGroupAlgebraAugmentationIdeal n G →
207 ModNCompletedGroupAlgebraAugmentationKernel n G := by
208 intro x
209 let y : ModNCompletedGroupAlgebra n G := ⟨fun U => (x.1 U).1, by
210 intro U V hUV
211 exact congrArg Subtype.val (x.2 U V hUV)⟩
212 refine ⟨y, ?_⟩
213 have hterm :
214 modNCompletedGroupAlgebraProjection n G
215 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) y ∈
216 modNCompletedGroupAlgebraStageAugmentationIdeal n G
217 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) := by
218 change (x.1 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)).1 ∈
219 modNCompletedGroupAlgebraStageAugmentationIdeal n G
220 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)
221 exact (x.1 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)).2
222 exact (mem_modNCompletedGroupAlgebraAugmentationKernel_iff (n := n) (G := G) (x := y)).2
223 ((mem_modNCompletedGroupAlgebraProjection_stageAugmentationIdeal_iff
224 (n := n) (G := G) (U := _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)
225 (x := y)).1 hterm)
227omit [Fact (0 < n)] in
228/--
229Projecting an element of the completed augmentation ideal gives its corresponding finite-stage
230augmentation-ideal coordinate.
231-/
232@[simp]
233theorem modNCompletedGroupAlgebraProjection_ofAugmentationIdeal
234 (x : ModNCompletedGroupAlgebraAugmentationIdeal n G) (U :
235 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
236 modNCompletedGroupAlgebraProjection n G U
237 (ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x).1 =
238 ((modNCompletedGroupAlgebraAugmentationIdealProjection (n := n) (G := G) U x) :
239 ModNCompletedGroupAlgebraStage n G U) := rfl
241omit [Fact (0 < n)] in
242/--
243The completion-to-stage map is one direction of the completed augmentation-ideal stage
244equivalence.
245-/
246@[simp]
247theorem ofModNCompletedGroupAlgebraAugmentationIdeal_to
248 (x : ModNCompletedGroupAlgebraAugmentationKernel n G) :
249 ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
250 (toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x) = x := by
251 apply Subtype.ext
252 apply (modNCompletedGroupAlgebraSystem n G).ext
253 intro U
254 rfl
256omit [Fact (0 < n)] in
257/--
258The stage-to-completion map is one direction of the completed augmentation-ideal stage
259equivalence.
260-/
261@[simp]
262theorem toModNCompletedGroupAlgebraAugmentationIdeal_of
263 (x : ModNCompletedGroupAlgebraAugmentationIdeal n G) :
264 toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
265 (ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x) = x := by
266 apply (modNCompletedGroupAlgebraAugmentationIdealSystem n G).ext
267 intro U
268 apply Subtype.ext
269 rfl
271/--
272The residue-coefficient completed augmentation kernel is canonically equivalent to the inverse
273limit of the finite-stage augmentation ideals.
274-/
275def modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit :
276 ModNCompletedGroupAlgebraAugmentationKernel n G ≃
277 ModNCompletedGroupAlgebraAugmentationIdeal n G where
278 toFun := toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
279 invFun := ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
280 left_inv := ofModNCompletedGroupAlgebraAugmentationIdeal_to (n := n) (G := G)
281 right_inv := toModNCompletedGroupAlgebraAugmentationIdeal_of (n := n) (G := G)
283omit [Fact (0 < n)] in
284/--
285The forward mod-\(n\) augmentation-kernel equivalence is the canonical map to the inverse-limit
286augmentation ideal.
287-/
288@[simp]
289theorem modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply
290 (x : ModNCompletedGroupAlgebraAugmentationKernel n G) :
291 modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit (n := n) (G := G) x =
292 toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x := rfl
294omit [Fact (0 < n)] in
295/--
296The inverse mod-\(n\) augmentation-kernel equivalence reconstructs a kernel element from an
297inverse-limit augmentation-ideal element.
298-/
299@[simp]
300theorem modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply
301 (x : ModNCompletedGroupAlgebraAugmentationIdeal n G) :
302 (modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit (n := n) (G := G)).symm x =
303 ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x := rfl
305end AugmentationIdeal
307end
309end FoxDifferential