Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation
ProCGroups/FoxDifferential/Completed/ProCIntegerCoefficients/Augmentation/Source

Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation

1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation
2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic
3import Mathlib.Algebra.Exact.Basic
4import Mathlib.RingTheory.Ideal.Maps
6/-!
7# Fox differential: completed — \(\mathbb{Z}_C\) coefficients — augmentation
9The principal declarations in this module are:
11- `zcCompletedGroupAlgebraTopIndex`
12 The canonical trivial group quotient used to read the completed augmentation.
13- `zcCompletedGroupAlgebraAugmentationFamily`
14 The finite coefficient coordinate of the completed augmentation \(\mathbb{Z}_C\llbracket
15 H\rrbracket \to \mathbb{Z}_C\).
16- `zcCompletedGroupAlgebraTopIndex_le`
17 The canonical trivial quotient is below every finite quotient index.
18- `zcCompletedGroupAlgebraAugmentationFamily_compatible`
19 The finite coefficient coordinates of the completed augmentation are compatible.
20-/
22namespace FoxDifferential
24noncomputable section
26open ProCGroups.Completion
27open ProCGroups.ProC
29universe u
31section Augmentation
33variable (C : ProCGroups.FiniteGroupClass.{u})
35variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
37/-- The canonical trivial group quotient used to read the completed augmentation. -/
38abbrev zcCompletedGroupAlgebraTopIndex : CompletedGroupAlgebraIndexInClass H C :=
39 OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := H))
41omit [IsTopologicalGroup H] in
42/-- The canonical trivial quotient is below every finite quotient index. -/
43theorem zcCompletedGroupAlgebraTopIndex_le
44 (U : CompletedGroupAlgebraIndexInClass H C) :
45 zcCompletedGroupAlgebraTopIndex C H ≤ U := by
46 change ((OrderDual.ofDual U).1 : Subgroup H) ≤ (⊤ : Subgroup H)
47 exact le_top
49/--
50The finite coefficient coordinate of the completed augmentation \(\mathbb{Z}_C\llbracket
51H\rrbracket \to \mathbb{Z}_C\).
52-/
53def zcCompletedGroupAlgebraAugmentationFamily
54 (x : ZCCompletedGroupAlgebra C H) (i : ProCIntegerIndex C) :
55 ProCIntegerStage C i := by
56 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
57 exact
58 modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C
59 (zcCompletedGroupAlgebraTopIndex C H)
60 (zcCompletedGroupAlgebraProjection C H
61 (i, zcCompletedGroupAlgebraTopIndex C H) x)
63/-- The finite coefficient coordinates of the completed augmentation are compatible. -/
64theorem zcCompletedGroupAlgebraAugmentationFamily_compatible
65 (x : ZCCompletedGroupAlgebra C H) {i j : ProCIntegerIndex C} (hij : i ≤ j) :
66 proCIntegerTransition (C := C) hij
67 (zcCompletedGroupAlgebraAugmentationFamily C H x j) =
68 zcCompletedGroupAlgebraAugmentationFamily C H x i := by
69 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
70 letI : Fact (0 < j.modulus) := ⟨j.positive⟩
71 let U := zcCompletedGroupAlgebraTopIndex C H
72 have hx := x.2 (i, U) (j, U) ⟨hij, le_rfl⟩
73 dsimp [zcCompletedGroupAlgebraAugmentationFamily]
74 change
75 modNCompletedCoeffMap (n := i.modulus) (m := j.modulus) hij
76 ((modNCompletedGroupAlgebraStageAugmentationInClass j.modulus H C U)
77 (x.1 (j, U))) =
78 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C U)
79 (x.1 (i, U))
80 rw [← hx]
81 simp only [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
82 modNCompletedGroupAlgebraTransitionInClass_id, RingHom.id_apply]
83 change
84 modNCompletedCoeffMap (n := i.modulus) (m := j.modulus) hij
85 ((modNCompletedGroupAlgebraStageAugmentationInClass j.modulus H C U)
86 (x.1 (j, U))) =
87 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C U)
88 ((modNCompletedGroupAlgebraStageCoeffMapInClass
89 (n := i.modulus) (m := j.modulus) (G := H) C U hij)
90 (x.1 (j, U)))
91 exact
92 (congrFun
93 (congrArg DFunLike.coe
94 (modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap
95 (n := i.modulus) (G := H) C U (m := j.modulus) hij))
96 (x.1 (j, U))).symm
98/--
99The completed augmentation \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\), obtained by
100augmenting every finite stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\) at the canonical trivial
101quotient of \(H\).
102-/
103def zcCompletedGroupAlgebraAugmentation :
104 ZCCompletedGroupAlgebra C H →+* ZCCoeff C where
105 toFun x :=
106 Subtype.mk
107 (zcCompletedGroupAlgebraAugmentationFamily C H x)
108 (by
109 intro i j hij
110 exact zcCompletedGroupAlgebraAugmentationFamily_compatible C H x hij)
111 map_zero' := by
112 ext i
113 change zcCompletedGroupAlgebraAugmentationFamily C H
114 (0 : ZCCompletedGroupAlgebra C H) i = 0
115 simp only [zcCompletedGroupAlgebraAugmentationFamily,
116 zcCompletedGroupAlgebraProjection_zero, map_zero]
117 map_one' := by
118 ext i
119 change zcCompletedGroupAlgebraAugmentationFamily C H
120 (1 : ZCCompletedGroupAlgebra C H) i = 1
121 simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_one,
122 map_one]
123 map_add' x y := by
124 ext i
125 change zcCompletedGroupAlgebraAugmentationFamily C H (x + y) i =
126 zcCompletedGroupAlgebraAugmentationFamily C H x i +
127 zcCompletedGroupAlgebraAugmentationFamily C H y i
128 simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_add,
129 map_add]
130 map_mul' x y := by
131 ext i
132 change zcCompletedGroupAlgebraAugmentationFamily C H (x * y) i =
133 zcCompletedGroupAlgebraAugmentationFamily C H x i *
134 zcCompletedGroupAlgebraAugmentationFamily C H y i
135 simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_mul,
136 map_mul]
138/-- Projecting the completed augmentation gives the corresponding finite-stage augmentation. -/
139@[simp]
140theorem proCIntegerProj_zcCompletedGroupAlgebraAugmentation
141 (i : ProCIntegerIndex C) (x : ZCCompletedGroupAlgebra C H) :
142 proCIntegerProj (C := C) i (zcCompletedGroupAlgebraAugmentation C H x) =
143 zcCompletedGroupAlgebraAugmentationFamily C H x i :=
144 rfl
146/--
147The completed augmentation can be read after projecting to any finite group quotient stage, not
148only the canonical trivial quotient used in its definition.
149-/
150theorem proCIntegerProj_zcCompletedGroupAlgebraAugmentation_eq_stage
151 (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
152 proCIntegerProj (C := C) i.1 (zcCompletedGroupAlgebraAugmentation C H x) =
153 modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C i.2
154 (zcCompletedGroupAlgebraProjection C H i x) := by
155 let T := zcCompletedGroupAlgebraTopIndex C H
156 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
157 have hT : T ≤ i.2 := zcCompletedGroupAlgebraTopIndex_le C H i.2
158 have hx := x.2 (i.1, T) i ⟨le_rfl, hT⟩
159 dsimp [zcCompletedGroupAlgebraAugmentationFamily]
160 change
161 (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C T) (x.1 (i.1, T)) =
162 (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C i.2) (x.1 i)
163 rw [← hx]
164 simp only [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
165 modNCompletedGroupAlgebraStageCoeffMapInClass_rfl, RingHom.id_apply]
166 exact congrFun
167 (congrArg DFunLike.coe
168 (modNCompletedGroupAlgebraStageAugmentationInClass_compatible
169 (n := i.1.modulus) (G := H) C hT)) (x.1 i)
171/-- The completed augmentation sends every group-like element to \(1\). -/
172@[simp]
173theorem zcCompletedGroupAlgebraAugmentation_groupLike (h : H) :
174 zcCompletedGroupAlgebraAugmentation C H (zcGroupLike C H h) = 1 := by
175 ext i
176 simp only [proCIntegerProj_zcCompletedGroupAlgebraAugmentation,
177 zcCompletedGroupAlgebraAugmentationFamily,
178 zcCompletedGroupAlgebraProjection_groupLike, OrderDual.ofDual_toDual, MonoidAlgebra.of_apply,
179 modNCompletedGroupAlgebraStageAugmentationInClass_single, proCIntegerProj_one]
181/-- The completed Fox boundary has augmentation zero. -/
182@[simp]
183theorem zcCompletedGroupAlgebraAugmentation_boundary
184 {G : Type u} [Group G] (ψ : G →* H) (g : G) :
185 zcCompletedGroupAlgebraAugmentation C H
186 (zcCompletedGroupAlgebraBoundary C ψ g) = 0 := by
187 change zcCompletedGroupAlgebraAugmentation C H
188 (zcGroupLike C H (ψ g) - 1) = 0
189 simp only [map_sub, zcCompletedGroupAlgebraAugmentation_groupLike, map_one, sub_self]
191/--
192The completed augmentation ideal, defined as the kernel of \(\mathbb{Z}_C\llbracket H\rrbracket
193\to \mathbb{Z}_C\).
194-/
195def zcCompletedGroupAlgebraAugmentationIdeal :
196 Ideal (ZCCompletedGroupAlgebra C H) :=
197 RingHom.ker (zcCompletedGroupAlgebraAugmentation C H)
199/-- The completed augmentation ideal is bundled as a subtype. -/
200abbrev ZCCompletedGroupAlgebraAugmentationIdeal : Type u :=
201 zcCompletedGroupAlgebraAugmentationIdeal C H
203/--
204A completed integer group-algebra element lies in the completed augmentation ideal iff the
205completed augmentation sends it to zero.
206-/
207@[simp]
208theorem mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
209 {C : ProCGroups.FiniteGroupClass.{u}}
211 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
212 {x : ZCCompletedGroupAlgebra C H} :
213 x ∈ zcCompletedGroupAlgebraAugmentationIdeal C H ↔
214 zcCompletedGroupAlgebraAugmentation C H x = 0 := by
215 rw [zcCompletedGroupAlgebraAugmentationIdeal, RingHom.mem_ker]
217/-- The algebraic standard-generator ideal is contained in the completed augmentation ideal. -/
218theorem zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal :
219 zcCompletedGroupAlgebraStandardAugmentationIdeal C H ≤
220 zcCompletedGroupAlgebraAugmentationIdeal C H := by
221 rw [zcCompletedGroupAlgebraStandardAugmentationIdeal]
222 refine Ideal.span_le.2 ?_
223 rintro x ⟨h, rfl⟩
224 change zcGroupLike C H h - 1 ∈ zcCompletedGroupAlgebraAugmentationIdeal C H
225 rw [mem_zcCompletedGroupAlgebraAugmentationIdeal_iff]
226 simp only [map_sub, zcCompletedGroupAlgebraAugmentation_groupLike, map_one, sub_self]
228/-- The completed Fox boundary lies in the completed augmentation ideal. -/
229theorem zcCompletedGroupAlgebraBoundary_mem_augmentationIdeal
230 {G : Type u} [Group G] (ψ : G →* H) (g : G) :
231 zcCompletedGroupAlgebraBoundary C ψ g ∈
232 zcCompletedGroupAlgebraAugmentationIdeal C H := by
233 rw [mem_zcCompletedGroupAlgebraAugmentationIdeal_iff]
234 simp only [zcCompletedGroupAlgebraAugmentation_boundary]
236/--
237If the completed augmentation kernel is the algebraic standard-generator ideal, then a
238surjective completed Fox boundary gives exactness at \(\mathbb{Z}_C\llbracket H\rrbracket\).
239-/
240theorem exact_zcToCompletedGA_of_surj_of_standardAugmentationIdeal_eq_augmentationIdeal
241 {G : Type u} [Group G] (ψ : G →* H) (hψ : Function.Surjective ψ)
242 (hstandard :
243 zcCompletedGroupAlgebraStandardAugmentationIdeal C H =
244 zcCompletedGroupAlgebraAugmentationIdeal C H) :
245 Function.Exact
246 (zcToCompletedGroupAlgebra C ψ :
247 ZCCompletedDifferentialModule C ψ → ZCCompletedGroupAlgebra C H)
248 (zcCompletedGroupAlgebraAugmentation C H :
249 ZCCompletedGroupAlgebra C H → ZCCoeff C) := by
250 intro z
251 constructor
252 · intro hz
253 have hzmem :
254 z ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H := by
255 rw [hstandard]
256 exact (mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
257 (C := C) (H := H) (x := z)).2 hz
258 have hzrange :
259 z ∈ LinearMap.range (zcToCompletedGroupAlgebra C ψ) := by
260 rw [zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective
261 C H ψ hψ]
262 exact hzmem
263 exact hzrange
264 · rintro ⟨m, rfl⟩
265 have hmem :
266 zcToCompletedGroupAlgebra C ψ m ∈
267 zcCompletedGroupAlgebraAugmentationIdeal C H :=
268 zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal C H
269 (zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal C H ψ m)
270 exact (mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
271 (C := C) (H := H) (x := zcToCompletedGroupAlgebra C ψ m)).1 hmem
273/--
274For a surjective coefficient group map, exactness of the algebraic completed Fox tail is
275equivalent to the algebraic standard-generator ideal already being the completed augmentation
276ideal. This isolates the closed-range obstruction for infinite completed group algebras.
277-/
278theorem exact_zcToCompletedGA_iff_standardAugmentationIdeal_eq_augmentationIdeal_of_surj
279 {C : ProCGroups.FiniteGroupClass.{u}}
281 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
282 {G : Type u} [Group G] (ψ : G →* H) (hψ : Function.Surjective ψ) :
283 Function.Exact
284 (zcToCompletedGroupAlgebra C ψ :
285 ZCCompletedDifferentialModule C ψ → ZCCompletedGroupAlgebra C H)
286 (zcCompletedGroupAlgebraAugmentation C H :
287 ZCCompletedGroupAlgebra C H → ZCCoeff C) ↔
288 zcCompletedGroupAlgebraStandardAugmentationIdeal C H =
289 zcCompletedGroupAlgebraAugmentationIdeal C H := by
290 constructor
291 · intro hexact
292 apply le_antisymm
293 · exact zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal C H
294 · intro z hz
295 have hz0 :
296 zcCompletedGroupAlgebraAugmentation C H z = 0 :=
297 (mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
298 (C := C) (H := H) (x := z)).1 hz
299 rcases (hexact z).1 hz0 with ⟨m, hm⟩
300 have hzrange :
301 z ∈ LinearMap.range (zcToCompletedGroupAlgebra C ψ) := ⟨m, hm⟩
302 rwa [zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective
303 C H ψ hψ] at hzrange
304 · intro hstandard
305 exact
306 exact_zcToCompletedGA_of_surj_of_standardAugmentationIdeal_eq_augmentationIdeal
307 C H ψ hψ hstandard
309/--
310The completed augmentation \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\) is
311surjective.
312-/
313theorem zcCompletedGroupAlgebraAugmentation_surjective :
314 Function.Surjective (zcCompletedGroupAlgebraAugmentation C H) := by
315 intro a
316 refine ⟨⟨fun i => ?_, ?_⟩, ?_⟩
317 · letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
318 exact MonoidAlgebra.single
319 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
320 (proCIntegerProj (C := C) i.1 a)
321 · intro i j hij
322 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
323 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
324 have ha :
325 modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1
326 (proCIntegerProj (C := C) j.1 a) =
327 proCIntegerProj (C := C) i.1 a :=
328 proCIntegerProj_transition (C := C) hij.1 a
329 have hmap :
330 modNCompletedGroupAlgebraTransitionInClass j.1.modulus H C hij.2
331 (algebraMap (ModNCompletedCoeff j.1.modulus)
332 (ZCCompletedGroupAlgebraStage C H j)
333 (proCIntegerProj (C := C) j.1 a)) =
334 algebraMap (ModNCompletedCoeff j.1.modulus)
335 (ModNCompletedGroupAlgebraStageInClass j.1.modulus H C i.2)
336 (proCIntegerProj (C := C) j.1 a) := by
337 change MonoidAlgebra.mapDomain _
338 (algebraMap (ModNCompletedCoeff j.1.modulus)
339 (ZCCompletedGroupAlgebraStage C H j)
340 (proCIntegerProj (C := C) j.1 a)) =
341 algebraMap (ModNCompletedCoeff j.1.modulus)
342 (ModNCompletedGroupAlgebraStageInClass j.1.modulus H C i.2)
343 (proCIntegerProj (C := C) j.1 a)
344 rw [MonoidAlgebra.mapDomain_algebraMap]
345 change
346 modNCompletedGroupAlgebraStageCoeffMapInClass
347 (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1
348 (modNCompletedGroupAlgebraTransitionInClass j.1.modulus H C hij.2
349 (algebraMap (ModNCompletedCoeff j.1.modulus)
350 (ZCCompletedGroupAlgebraStage C H j)
351 (proCIntegerProj (C := C) j.1 a))) =
352 MonoidAlgebra.single
353 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
354 (proCIntegerProj (C := C) i.1 a)
355 rw [hmap]
356 change
357 modNCompletedGroupAlgebraStageCoeffMapInClass
358 (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1
359 (MonoidAlgebra.single
360 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
361 (proCIntegerProj (C := C) j.1 a)) =
362 MonoidAlgebra.single
363 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
364 (proCIntegerProj (C := C) i.1 a)
365 rw [modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply, ha]
366 · ext i
367 let T := zcCompletedGroupAlgebraTopIndex C H
368 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
369 change
370 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C T)
371 (MonoidAlgebra.single
372 (1 : CompletedGroupAlgebraQuotientInClass H C T)
373 (proCIntegerProj (C := C) i a)) =
374 proCIntegerProj (C := C) i a
375 simp only [modNCompletedGroupAlgebraStageAugmentationInClass_single]
377end Augmentation
379end
381end FoxDifferential