Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Comparison.DiscreteCompletion
ProCGroups/FoxDifferential/Completed/Comparison/DiscreteCompletion/Source

Source: ProCGroups.FoxDifferential.Completed.Comparison.DiscreteCompletion

1import ProCGroups.FoxDifferential.Discrete.Naturality
2import ProCGroups.FoxDifferential.Completed.Comparison.FiniteStage
3import ProCGroups.Completion.ProCIntegerPrimePower
5/-!
6# Fox differential: completed — comparison — discrete completion
8The principal declarations in this module are:
10- `foxAlgebraicStageGroupRingReduction`
11 Coefficient reduction from the integral group ring \(\mathbb{Z}[F/N]\) to the finite-stage target
12 group algebra \((\mathbb{Z}/n\mathbb{Z})[F/N]\).
13- `foxAlgebraicStageGroupRingReduction_of`
14 The finite-stage group-ring reduction sends a group-like basis element to the same quotient basis
15 element with reduced coefficient.
16- `foxAlgebraicStageGroupRingReduction_apply`
17 Coefficients of the finite-stage group-ring reduction are ordinary reduction modulo \(n\).
18- `int_eq_zero_of_forall_zmod_cast_eq_zero`
19 An integer whose image in every positive residue ring is zero is zero.
20-/
22namespace FoxDifferential
24noncomputable section
26open scoped BigOperators
28universe u
30section DiscreteCompletion
32variable {X : Type u} [DecidableEq X]
33variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
35/--
36Coefficient reduction from the integral group ring \(\mathbb{Z}[F/N]\) to the finite-stage
37target group algebra \((\mathbb{Z}/n\mathbb{Z})[F/N]\).
38-/
39def foxAlgebraicStageGroupRingReduction :
40 GroupRing (foxAlgebraicStageTargetQuotient (X := X) N) →+*
41 foxAlgebraicStageTargetGroupAlgebra (X := X) N n :=
42 MonoidAlgebra.mapRingHom
43 (foxAlgebraicStageTargetQuotient (X := X) N)
44 (Int.castRingHom (ModNCompletedCoeff n))
46omit [DecidableEq X] in
47/--
48The finite-stage group-ring reduction sends a group-like basis element to the same quotient
49basis element with reduced coefficient.
50-/
51@[simp]
52theorem foxAlgebraicStageGroupRingReduction_of
53 (q : foxAlgebraicStageTargetQuotient (X := X) N) :
54 foxAlgebraicStageGroupRingReduction (X := X) N n
55 (MonoidAlgebra.of ℤ (foxAlgebraicStageTargetQuotient (X := X) N) q) =
56 MonoidAlgebra.of (ModNCompletedCoeff n)
57 (foxAlgebraicStageTargetQuotient (X := X) N) q := by
58 simp only [foxAlgebraicStageGroupRingReduction, MonoidAlgebra.of_apply,
59 MonoidAlgebra.mapRingHom_single, map_one]
61omit [DecidableEq X] in
62/-- Coefficients of the finite-stage group-ring reduction are ordinary reduction modulo \(n\). -/
63@[simp]
64theorem foxAlgebraicStageGroupRingReduction_apply
65 (x : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N))
66 (q : foxAlgebraicStageTargetQuotient (X := X) N) :
67 (foxAlgebraicStageGroupRingReduction (X := X) N n x).coeff q =
68 (x.coeff q : ModNCompletedCoeff n) := by
69 rw [foxAlgebraicStageGroupRingReduction]
70 exact MonoidAlgebra.coeff_mapRingHom
71 (Int.castRingHom (ModNCompletedCoeff n)) x q
73/-- An integer whose image in every positive residue ring is zero is zero. -/
74theorem int_eq_zero_of_forall_zmod_cast_eq_zero
75 (z : ℤ) (hz : ∀ n : ℕ, 0 < n → (z : ZMod n) = 0) :
76 z = 0 := by
77 by_contra hzne
78 let n : ℕ := z.natAbs + 1
79 have hn : 0 < n := Nat.succ_pos z.natAbs
80 have hzmod : (z : ZMod n) = 0 := hz n hn
81 have hdvdInt : (n : ℤ) ∣ z := by
82 exact (ZMod.intCast_zmod_eq_zero_iff_dvd z n).mp hzmod
83 have hdvdNat : n ∣ z.natAbs := (Int.natCast_dvd).1 hdvdInt
84 have hzabs_pos : 0 < z.natAbs := Int.natAbs_pos.mpr hzne
85 have hle : n ≤ z.natAbs := Nat.le_of_dvd hzabs_pos hdvdNat
86 exact Nat.not_succ_le_self z.natAbs hle
88/-- An integer whose image in every \(p^k\) residue ring is zero is zero. -/
89theorem int_eq_zero_of_forall_zmod_prime_pow_cast_eq_zero
90 (p : ℕ) [Fact (Nat.Prime p)] (z : ℤ)
91 (hz : ∀ k : ℕ, (z : ZMod (p ^ k)) = 0) :
92 z = 0 := by
93 by_contra hzne
94 let k : ℕ := Nat.log p z.natAbs + 1
95 have hp1 : 1 < p := (Fact.out : Nat.Prime p).one_lt
96 have hlt : z.natAbs < p ^ k := by
97 simpa [k, Nat.succ_eq_add_one] using
98 Nat.lt_pow_succ_log_self hp1 z.natAbs
99 have hzmod : (z : ZMod (p ^ k)) = 0 := hz k
100 have hdvdInt : ((p ^ k : ℕ) : ℤ) ∣ z := by
101 exact (ZMod.intCast_zmod_eq_zero_iff_dvd z (p ^ k)).mp hzmod
102 have hdvdNat : p ^ k ∣ z.natAbs := (Int.natCast_dvd).1 hdvdInt
103 have hzabs_pos : 0 < z.natAbs := Int.natAbs_pos.mpr hzne
104 have hle : p ^ k ≤ z.natAbs := Nat.le_of_dvd hzabs_pos hdvdNat
105 exact (not_lt_of_ge hle) hlt
107omit [DecidableEq X] in
108/-- Integral group rings are torsion-free for positive natural scalar multiplication. -/
109theorem groupRing_eq_zero_of_nsmul_eq_zero
110 {M : Type*} [Monoid M] {n : ℕ} (hn : 0 < n) (x : GroupRing M)
111 (hx : n • x = 0) :
112 x = 0 := by
113 ext m
114 have hcoeff : n • x.coeff m = 0 := by
115 exact congrArg (fun y : GroupRing M => y.coeff m) hx
116 have hmul : (n : ℤ) * x.coeff m = 0 := by
117 rw [← nsmul_eq_mul]
118 exact hcoeff
119 exact (Int.mul_eq_zero.mp hmul).resolve_left (by exact_mod_cast (Nat.ne_of_gt hn))
121omit [DecidableEq X] in
122/--
123A finite-support integral group-ring element is zero if all of its positive residue reductions
124are zero.
125-/
126theorem groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_eq_zero
127 (x : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N))
128 (hx : ∀ n : ℕ, 0 < n →
129 foxAlgebraicStageGroupRingReduction (X := X) N n x = 0) :
130 x = 0 := by
131 ext q
132 apply int_eq_zero_of_forall_zmod_cast_eq_zero
133 intro n hn
134 have hcoeff := congrArg (fun y => y.coeff q) (hx n hn)
135 simpa using hcoeff
137omit [DecidableEq X] in
138/--
139A finite-support integral group-ring element is zero if all of its \(p^k\) residue reductions
140are zero.
141-/
142theorem groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_primePow_eq_zero
143 (p : ℕ) [Fact (Nat.Prime p)]
144 (x : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N))
145 (hx : ∀ k : ℕ,
146 foxAlgebraicStageGroupRingReduction (X := X) N (p ^ k) x = 0) :
147 x = 0 := by
148 ext q
149 apply int_eq_zero_of_forall_zmod_prime_pow_cast_eq_zero p
150 intro k
151 have hcoeff := congrArg (fun y => y.coeff q) (hx k)
152 simpa using hcoeff
154omit [DecidableEq X] in
155/--
156A finite-stage residue-zero integral group-ring element is divisible by the chosen coefficient
157modulus.
158-/
159theorem exists_eq_nsmul_of_foxAlgebraicStageGroupRingReduction_eq_zero
160 {n : ℕ}
161 (x : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N))
162 (hx : foxAlgebraicStageGroupRingReduction (X := X) N n x = 0) :
163 ∃ y : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N), x = n • y := by
164 classical
165 let Q := foxAlgebraicStageTargetQuotient (X := X) N
166 have hdvd : ∀ q : Q, (n : ℤ) ∣ x.coeff q := by
167 intro q
168 exact (ZMod.intCast_zmod_eq_zero_iff_dvd (x.coeff q) n).mp (by
169 have hcoeff :=
170 congrArg
171 (fun y : foxAlgebraicStageTargetGroupAlgebra (X := X) N n =>
172 y.coeff q) hx
173 simpa using hcoeff)
174 let coeff : Q → ℤ := fun q =>
175 if x.coeff q = 0 then 0 else Classical.choose (hdvd q)
176 have hcoeff_support : ∀ q : Q, coeff q ≠ 0 → q ∈ x.coeff.support := by
177 intro q hq
178 rw [Finsupp.mem_support_iff]
179 intro hxq
180 have hzero : coeff q = 0 := by
181 dsimp [coeff]
182 rw [if_pos hxq]
183 exact hq hzero
184 let y : GroupRing Q :=
185 MonoidAlgebra.ofCoeff
186 (Finsupp.onFinset x.coeff.support coeff hcoeff_support)
187 refine ⟨y, ?_⟩
188 ext q
189 change x.coeff q = n • coeff q
190 by_cases hxq : x.coeff q = 0
191 · simp only [hxq, ↓reduceIte, nsmul_zero, coeff]
192 · have hchoose := Classical.choose_spec (hdvd q)
193 simpa [coeff, hxq, nsmul_eq_mul] using hchoose
195/--
196The finite-stage derivative vector is the image of the ordinary relative Fox derivative under
197coefficient reduction from \(\mathbb{Z}[F/N]\) to \((\mathbb{Z}/n\mathbb{Z})[F/N]\).
198-/
199theorem foxAlgebraicStageDerivativeVector_eq_discreteReduction
200 (w : FreeGroup X) :
201 foxAlgebraicStageDerivativeVector (X := X) N n w =
202 fun i : X =>
203 foxAlgebraicStageGroupRingReduction (X := X) N n
204 (FoxCalculus.relativeFreeGroupFoxDerivative
205 (H := foxAlgebraicStageTargetQuotient (X := X) N)
206 X (QuotientGroup.mk' N) w i) := by
207 let delta : ScalarCrossedHom
208 (foxAlgebraicStageCoefficient (X := X) N n)
209 (foxAlgebraicStageCoordinateVector (X := X) N n) :=
210 { toFun := fun w i =>
211 foxAlgebraicStageGroupRingReduction (X := X) N n
212 (FoxCalculus.relativeFreeGroupFoxDerivative
213 (H := foxAlgebraicStageTargetQuotient (X := X) N)
214 X (QuotientGroup.mk' N) w i)
215 map_mul' := by
216 intro u v
217 rw [scalarCrossedAction_apply]
218 funext i
219 change foxAlgebraicStageGroupRingReduction (X := X) N n
220 (FoxCalculus.relativeFreeGroupFoxDerivative
221 (H := foxAlgebraicStageTargetQuotient (X := X) N)
222 X (QuotientGroup.mk' N) (u * v) i) =
223 foxAlgebraicStageGroupRingReduction (X := X) N n
224 (FoxCalculus.relativeFreeGroupFoxDerivative
225 (H := foxAlgebraicStageTargetQuotient (X := X) N)
226 X (QuotientGroup.mk' N) u i) +
227 foxAlgebraicStageCoefficient (X := X) N n u *
228 foxAlgebraicStageGroupRingReduction (X := X) N n
229 (FoxCalculus.relativeFreeGroupFoxDerivative
230 (H := foxAlgebraicStageTargetQuotient (X := X) N)
231 X (QuotientGroup.mk' N) v i)
232 rw [show
233 FoxCalculus.relativeFreeGroupFoxDerivative
234 (H := foxAlgebraicStageTargetQuotient (X := X) N)
235 X (QuotientGroup.mk' N) (u * v) i =
236 FoxCalculus.relativeFreeGroupFoxDerivative
237 (H := foxAlgebraicStageTargetQuotient (X := X) N)
238 X (QuotientGroup.mk' N) u i +
239 (MonoidAlgebra.of ℤ (foxAlgebraicStageTargetQuotient (X := X) N)
240 (QuotientGroup.mk' N u) :
241 FoxDifferential.GroupRing (foxAlgebraicStageTargetQuotient (X := X) N)) *
242 FoxCalculus.relativeFreeGroupFoxDerivative
243 (H := foxAlgebraicStageTargetQuotient (X := X) N)
244 X (QuotientGroup.mk' N) v i by
245 simpa [Pi.add_apply, Pi.smul_apply, smul_eq_mul] using
246 congrFun
247 (FoxCalculus.relativeFreeGroupFoxDerivative_mul
248 (H := foxAlgebraicStageTargetQuotient (X := X) N)
249 X (QuotientGroup.mk' N) u v) i]
250 rw [map_add, map_mul, foxAlgebraicStageGroupRingReduction_of]
251 rfl }
252 have hbasis :
253 ∀ x : X, delta (FreeGroup.of x) =
254 Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n) := by
255 intro x
256 change (fun i : X =>
257 foxAlgebraicStageGroupRingReduction (X := X) N n
258 (FoxCalculus.relativeFreeGroupFoxDerivative
259 (H := foxAlgebraicStageTargetQuotient (X := X) N)
260 X (QuotientGroup.mk' N) (FreeGroup.of x) i)) =
261 Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
262 funext i
263 by_cases hix : i = x
264 · subst i
265 simp only [FoxCalculus.relativeFreeGroupFoxDerivative_of,
266 Pi.single_eq_same, map_one]
267 · simp only [FoxCalculus.relativeFreeGroupFoxDerivative_of,
268 Pi.single_eq_of_ne hix, map_zero]
269 have hdelta_eq :
270 delta = foxAlgebraicStageDerivativeVectorCrossedHom (X := X) N n :=
271 foxAlgebraicStageDerivativeVector_unique (X := X) N n delta hbasis
272 have hw := congrArg (fun d => d w) hdelta_eq
273 change
274 foxAlgebraicStageDerivativeVectorCrossedHom (X := X) N n w = delta w
275 exact hw.symm
277/--
278The comparison between the finite-stage derivative and the ordinary relative Fox derivative
279holds componentwise.
280-/
281theorem foxAlgebraicStageDerivative_eq_discreteReduction
282 (i : X) (w : FreeGroup X) :
283 foxAlgebraicStageDerivative (X := X) N n i w =
284 foxAlgebraicStageGroupRingReduction (X := X) N n
285 (FoxCalculus.relativeFreeGroupFoxDerivative
286 (H := foxAlgebraicStageTargetQuotient (X := X) N)
287 X (QuotientGroup.mk' N) w i) := by
288 have h := congrFun
289 (foxAlgebraicStageDerivativeVector_eq_discreteReduction (X := X) N n w) i
290 simpa [foxAlgebraicStageDerivative] using h
292/--
293One finite-stage derivative-vector vanishing says that the ordinary integral relative Fox
294derivative vector is divisible by the coefficient modulus.
295-/
296theorem exists_eq_nsmul_relFreeFoxDeriv_of_foxAlgebraicStageDerivativeVector_eq_zero
297 {n : ℕ} (w : FreeGroup X)
298 (hder : foxAlgebraicStageDerivativeVector (X := X) N n w = 0) :
299 ∃ y : X → GroupRing (foxAlgebraicStageTargetQuotient (X := X) N),
300 FoxCalculus.relativeFreeGroupFoxDerivative
301 (H := foxAlgebraicStageTargetQuotient (X := X) N)
302 X (QuotientGroup.mk' N) w = n • y := by
303 classical
304 have hred :
305 ∀ i : X,
306 foxAlgebraicStageGroupRingReduction (X := X) N n
307 (FoxCalculus.relativeFreeGroupFoxDerivative
308 (H := foxAlgebraicStageTargetQuotient (X := X) N)
309 X (QuotientGroup.mk' N) w i) = 0 := by
310 intro i
311 have hcomp :=
312 congrFun (foxAlgebraicStageDerivativeVector_eq_discreteReduction (X := X) N n w) i
313 have hzero := congrFun hder i
314 exact hcomp.symm.trans hzero
315 choose y hy using fun i =>
316 exists_eq_nsmul_of_foxAlgebraicStageGroupRingReduction_eq_zero (X := X) N
317 (FoxCalculus.relativeFreeGroupFoxDerivative
318 (H := foxAlgebraicStageTargetQuotient (X := X) N)
319 X (QuotientGroup.mk' N) w i)
320 (hred i)
321 refine ⟨y, ?_⟩
322 funext i
323 exact hy i
325/--
326Residue-universal version of one-modulus divisibility for the ordinary integral relative Fox
327derivative vector.
328-/
329theorem exists_eq_nsmul_relFreeFoxDeriv_of_residueUnivDiff_eq_zero
330 [Finite X]
331 {n : ℕ} (w : FreeGroup X)
332 (hres : residueUniversalDifferential n (QuotientGroup.mk' N) w = 0) :
333 ∃ y : X → GroupRing (foxAlgebraicStageTargetQuotient (X := X) N),
334 FoxCalculus.relativeFreeGroupFoxDerivative
335 (H := foxAlgebraicStageTargetQuotient (X := X) N)
336 X (QuotientGroup.mk' N) w = n • y := by
337 classical
338 letI : Fintype X := Fintype.ofFinite X
339 exact
340 exists_eq_nsmul_relFreeFoxDeriv_of_foxAlgebraicStageDerivativeVector_eq_zero
341 (X := X) N w
342 ((foxAlgebraicStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero
343 (X := X) (N := N) (n := n) (w := w)).2 hres)
345/--
346If every positive finite-stage derivative vanishes, then the ordinary integral relative Fox
347derivative vanishes.
348-/
349theorem relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_eq_zero
350 (w : FreeGroup X)
351 (hder :
352 ∀ n : ℕ, 0 < n →
353 ∀ i : X, foxAlgebraicStageDerivative (X := X) N n i w = 0) :
354 FoxCalculus.relativeFreeGroupFoxDerivative
355 (H := foxAlgebraicStageTargetQuotient (X := X) N)
356 X (QuotientGroup.mk' N) w = 0 := by
357 funext i
358 apply groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_eq_zero
359 (X := X) N
360 intro n hn
361 exact
362 (foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N n i w).symm.trans
363 (hder n hn i)
365/--
366If every \(p^k\) finite-stage derivative vanishes, then the ordinary integral relative Fox
367derivative vanishes.
368-/
369theorem relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_primePow_eq_zero
370 (p : ℕ) [Fact (Nat.Prime p)] (w : FreeGroup X)
371 (hder :
372 ∀ k : ℕ,
373 ∀ i : X, foxAlgebraicStageDerivative (X := X) N (p ^ k) i w = 0) :
374 FoxCalculus.relativeFreeGroupFoxDerivative
375 (H := foxAlgebraicStageTargetQuotient (X := X) N)
376 X (QuotientGroup.mk' N) w = 0 := by
377 funext i
378 apply groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_primePow_eq_zero
379 (X := X) N p
380 intro k
381 exact
382 (foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N (p ^ k) i w).symm.trans
383 (hder k i)
385section CompletedProjection
387variable (C : ProCGroups.FiniteGroupClass.{u})
388variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
389variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
391/--
392Projecting the completed \(\mathbb{Z}_C\) derivative to a finite pro-\(C\) target stage gives
393the stage map applied to the reduced ordinary relative Fox derivative.
394-/
395theorem zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
396 (i : X) (w : FreeGroup X)
397 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
398 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
399 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
400 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
401 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
402 (zcFiniteStageTarget X N) C j.2
403 (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
404 (FoxCalculus.relativeFreeGroupFoxDerivative
405 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) := by
406 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
407 rw [zcFreeGroupFoxDerivative_finiteStageProjection C N j i w]
408 rw [foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]
410/-- Vector-valued form of the discrete-to-completed projection comparison. -/
411theorem zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction
412 (w : FreeGroup X)
413 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
414 (fun i : X =>
415 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
416 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
417 fun i : X =>
418 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
419 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
420 (zcFiniteStageTarget X N) C j.2
421 (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
422 (FoxCalculus.relativeFreeGroupFoxDerivative
423 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by
424 funext i
425 exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
426 (C := C) (X := X) N i w j
428/--
429The completed \(\mathbb{Z}_C\) component derivative is uniquely determined by the finite-stage
430projections of the ordinary relative Fox derivative after coefficient reduction.
431-/
432theorem zcFreeGroupFoxDerivative_unique_finiteStageProjection_discreteReduction
433 (i : X)
434 (delta : FreeGroup X →
435 ZCCompletedGroupAlgebra C (zcFiniteStageTarget X N))
436 (hprojection : ∀ w
437 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
438 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta w) =
439 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
440 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
441 (zcFiniteStageTarget X N) C j.2
442 (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
443 (FoxCalculus.relativeFreeGroupFoxDerivative
444 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)))) :
445 delta = zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i := by
446 refine zcFreeGroupFoxDerivative_unique_finiteStageProjection
447 (C := C) (X := X) N i delta ?_
448 intro w j
449 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
450 rw [hprojection w j]
451 rw [← foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]
453/--
454Existence and uniqueness of the completed \(\mathbb{Z}_C\) component derivative characterized by
455the finite-stage projections of the reduced ordinary relative Fox derivative.
456-/
457theorem existsUnique_zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
458 (i : X) :
459 ∃! delta : FreeGroup X →
460 ZCCompletedGroupAlgebra C (zcFiniteStageTarget X N),
461 ∀ w
462 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
463 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta w) =
464 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
465 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
466 (zcFiniteStageTarget X N) C j.2
467 (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
468 (FoxCalculus.relativeFreeGroupFoxDerivative
469 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) := by
470 refine ⟨zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i, ?_, ?_⟩
471 · intro w j
472 exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
473 (C := C) (X := X) N i w j
474 · intro delta hprojection
475 exact zcFreeGroupFoxDerivative_unique_finiteStageProjection_discreteReduction
476 (C := C) (X := X) N i delta hprojection
478/--
479The completed \(\mathbb{Z}_C\) derivative vector is uniquely determined by the finite-stage
480projections of the ordinary relative Fox derivative after coefficient reduction.
481-/
482theorem zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection_discreteReduction
483 (delta : FreeGroup X →
484 ZCFreeFoxCoordinates C (X := X) (H := zcFiniteStageTarget X N))
485 (hprojection : ∀ w
486 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
487 (fun i : X =>
488 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta w i)) =
489 fun i : X =>
490 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
491 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
492 (zcFiniteStageTarget X N) C j.2
493 (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
494 (FoxCalculus.relativeFreeGroupFoxDerivative
495 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) :
496 delta = zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) := by
497 refine zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection
498 (C := C) (X := X) N delta ?_
499 intro w j
500 funext i
501 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
502 have hcoord := congrFun (hprojection w j) i
503 rw [hcoord]
504 rw [← foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]
506/--
507Existence and uniqueness of the completed \(\mathbb{Z}_C\) derivative vector characterized by
508the finite-stage projections of the reduced ordinary relative Fox derivative.
509-/
510theorem existsUnique_zcFreeFoxDerivVec_finiteStageProj_discreteReduction :
511 ∃! delta : FreeGroup X →
512 ZCFreeFoxCoordinates C (X := X) (H := zcFiniteStageTarget X N),
513 ∀ w
514 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
515 (fun i : X =>
516 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
517 (delta w i)) =
518 fun i : X =>
519 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
520 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
521 (zcFiniteStageTarget X N) C j.2
522 (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
523 (FoxCalculus.relativeFreeGroupFoxDerivative
524 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by
525 refine ⟨zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N), ?_, ?_⟩
526 · intro w j
527 exact zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction
528 (C := C) (X := X) N w j
529 · intro delta hprojection
530 exact zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection_discreteReduction
531 (C := C) (X := X) N delta hprojection
533/--
534Projecting the completed Fox-Euler formula and reducing the coefficients identifies the
535derivative coordinates with the ordinary relative Fox derivative.
536-/
537theorem zcFreeGroupFoxDerivative_fundFormula_finiteStageProj_discreteReduction
538 [Fintype X]
539 (w : FreeGroup X)
540 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
541 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
542 (zcCompletedGroupAlgebraBoundary C (QuotientGroup.mk' N) w) =
543 ∑ i : X,
544 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
545 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
546 (zcFiniteStageTarget X N) C j.2
547 (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
548 (FoxCalculus.relativeFreeGroupFoxDerivative
549 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) *
550 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
551 (zcGroupLike C (zcFiniteStageTarget X N)
552 (QuotientGroup.mk' N (FreeGroup.of i)) - 1) := by
553 rw [zcFreeGroupFoxDerivative_fundamental_formula_finiteStageProjection_stageMap
554 (C := C) (X := X) N w j]
555 apply Finset.sum_congr rfl
556 intro i hi
557 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
558 rw [foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]
560/--
561Over the all-finite coefficient class, a zero completed derivative vector on the finite quotient
562map already forces the ordinary integral relative Fox derivative to vanish.
563-/
564theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite
565 [DiscreteTopology (foxAlgebraicStageTargetQuotient (X := X) N)]
566 [Finite (foxAlgebraicStageTargetQuotient (X := X) N)]
567 (w : FreeGroup X)
568 (hw :
569 zcFreeGroupFoxDerivativeVector
570 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
571 (QuotientGroup.mk' N) w = 0) :
572 FoxCalculus.relativeFreeGroupFoxDerivative
573 (H := foxAlgebraicStageTargetQuotient (X := X) N)
574 X (QuotientGroup.mk' N) w = 0 := by
575 apply relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_eq_zero
576 (X := X) N w
577 intro n hn i
579 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}) :=
581 have hjmod : j.modulus = n := rfl
582 have hCtarget :
583 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
584 (foxAlgebraicStageTargetQuotient (X := X) N) := by
585 exact (inferInstance :
586 Finite (foxAlgebraicStageTargetQuotient (X := X) N))
587 have hcomponent :
588 zcFreeGroupFoxDerivative
589 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
590 (QuotientGroup.mk' N) i w = 0 := by
591 simpa [zcFreeGroupFoxDerivative] using congrFun hw i
592 have hstage :=
593 foxAlgebraicStageDerivative_eq_zero_of_zcFreeGroupFoxDerivative_eq_zero
594 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
595 (X := X) N
597 (hCtarget := hCtarget)
598 j i hcomponent
599 apply MonoidAlgebra.coeff_injective
600 apply Finsupp.ext
601 intro q
602 have hcoeff := congrArg (fun z => z.coeff q) hstage
603 change
604 (foxAlgebraicStageDerivative (X := X) N j.modulus i w).coeff q = 0
605 exact hcoeff.trans (by rfl)
607/--
608Over the all-finite coefficient class, a zero completed universal differential on the finite
609quotient map already forces the ordinary integral relative Fox derivative to vanish.
610-/
611theorem relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite
612 [DiscreteTopology (foxAlgebraicStageTargetQuotient (X := X) N)]
613 [Finite (foxAlgebraicStageTargetQuotient (X := X) N)]
614 (w : FreeGroup X)
615 (hw :
616 zcUniversalDifferential
617 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
618 (QuotientGroup.mk' N) w = 0) :
619 FoxCalculus.relativeFreeGroupFoxDerivative
620 (H := foxAlgebraicStageTargetQuotient (X := X) N)
621 X (QuotientGroup.mk' N) w = 0 := by
622 exact
623 relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite
624 (X := X) N w
625 (zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
626 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
627 (QuotientGroup.mk' N) hw)
629/--
630Over the finite \(p\)-group coefficient class, a zero completed derivative vector on the finite
631quotient map forces the ordinary integral relative Fox derivative to vanish, using only the
632prime-power coefficient stages.
633-/
634theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup
635 (p : ℕ) [Fact (Nat.Prime p)]
636 [DiscreteTopology (foxAlgebraicStageTargetQuotient (X := X) N)]
637 (hCtarget :
639 (foxAlgebraicStageTargetQuotient (X := X) N))
640 (w : FreeGroup X)
641 (hw :
642 zcFreeGroupFoxDerivativeVector
643 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
644 (QuotientGroup.mk' N) w = 0) :
645 FoxCalculus.relativeFreeGroupFoxDerivative
646 (H := foxAlgebraicStageTargetQuotient (X := X) N)
647 X (QuotientGroup.mk' N) w = 0 := by
648 apply relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_primePow_eq_zero
649 (X := X) N p w
650 intro k i
652 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}) :=
654 have hjmod : j.modulus = p ^ k := rfl
655 have hcomponent :
656 zcFreeGroupFoxDerivative
657 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
658 (QuotientGroup.mk' N) i w = 0 := by
659 simpa [zcFreeGroupFoxDerivative] using congrFun hw i
660 have hstage :=
661 foxAlgebraicStageDerivative_eq_zero_of_zcFreeGroupFoxDerivative_eq_zero
662 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
663 (X := X) N
665 (hCtarget := hCtarget)
666 j i hcomponent
667 apply MonoidAlgebra.coeff_injective
668 apply Finsupp.ext
669 intro q
670 have hcoeff := congrArg (fun z => z.coeff q) hstage
671 change
672 (foxAlgebraicStageDerivative (X := X) N j.modulus i w).coeff q = 0
673 exact hcoeff.trans (by rfl)
675/--
676Over the finite \(p\)-group coefficient class, a zero completed universal differential on the
677finite quotient map already forces the ordinary integral relative Fox derivative to vanish,
678using only the prime-power coefficient stages.
679-/
680theorem relativeFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero_pGroup
681 (p : ℕ) [Fact (Nat.Prime p)]
682 [DiscreteTopology (foxAlgebraicStageTargetQuotient (X := X) N)]
683 (hCtarget :
685 (foxAlgebraicStageTargetQuotient (X := X) N))
686 (w : FreeGroup X)
687 (hw :
688 zcUniversalDifferential
689 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
690 (QuotientGroup.mk' N) w = 0) :
691 FoxCalculus.relativeFreeGroupFoxDerivative
692 (H := foxAlgebraicStageTargetQuotient (X := X) N)
693 X (QuotientGroup.mk' N) w = 0 := by
694 exact
695 relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup
696 (X := X) N p hCtarget w
697 (zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
698 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
699 (QuotientGroup.mk' N) hw)
701end CompletedProjection
703end DiscreteCompletion
705section FiniteTarget
707variable {X : Type u} [DecidableEq X]
708variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
710/--
711All-finite coefficient separation holds for an arbitrary finite discrete target map. The
712quotient-map version is applied after identifying the target with \(\mathrm{FreeGroup}(X)/\ker
713\psi\), and completed derivative vectors are transported by target naturality.
714-/
715theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj
716 [DiscreteTopology H] [Finite H]
717 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
718 (w : FreeGroup X)
719 (hw :
720 zcFreeGroupFoxDerivativeVector
721 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
722 ψ w = 0) :
723 FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0 := by
724 let N : Subgroup (FreeGroup X) := ψ.ker
725 let Q : Type u := foxAlgebraicStageTargetQuotient (X := X) N
726 letI : TopologicalSpace Q := ⊥
727 letI : DiscreteTopology Q := ⟨rfl⟩
728 letI : IsTopologicalGroup Q := inferInstance
729 let e : Q ≃* H := QuotientGroup.quotientKerEquivOfSurjective ψ hψ
730 letI : Finite Q := Finite.of_injective e e.injective
731 let q : FreeGroup X →* Q := QuotientGroup.mk' N
732 have he_apply (g : FreeGroup X) : e (q g) = ψ g := by
733 change QuotientGroup.quotientKerEquivOfSurjective ψ hψ
734 (QuotientGroup.mk' ψ.ker g) = ψ g
735 rfl
736 let eSymm : H →ₜ* Q :=
737 { toMonoidHom := e.symm.toMonoidHom
738 continuous_toFun := continuous_of_discreteTopology }
739 have hcompSymm : eSymm.toMonoidHom.comp ψ = q := by
740 apply MonoidHom.ext
741 intro g
742 apply e.injective
743 change e (e.symm (ψ g)) = e (q g)
744 simpa using (he_apply g).symm
745 have hvecQ :
746 zcFreeGroupFoxDerivativeVector
747 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
748 q w = 0 := by
749 have htarget :=
750 zcFreeGroupFoxDerivativeVector_mapTarget
751 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
753 rw [hcompSymm] at htarget
754 rw [htarget, hw]
755 rfl
756 have hq :
757 FoxCalculus.relativeFreeGroupFoxDerivative (H := Q) X q w = 0 :=
758 relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite
759 (X := X) N w hvecQ
760 have hcomp : e.toMonoidHom.comp q = ψ := by
761 apply MonoidHom.ext
762 intro g
763 exact he_apply g
764 have hnat :=
765 FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain
766 (H := Q) (K := H) q e.toMonoidHom w
767 rw [hcomp] at hnat
768 rw [hnat, hq]
769 rfl
771/--
772Over the all-finite coefficient class, a zero completed universal differential on an arbitrary
773finite discrete target map already forces the ordinary integral relative Fox derivative to
774vanish.
775-/
776theorem relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite_of_surj
777 [DiscreteTopology H] [Finite H]
778 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
779 (w : FreeGroup X)
780 (hw :
781 zcUniversalDifferential
782 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
783 ψ w = 0) :
784 FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0 :=
785 relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj
786 (X := X) ψ hψ w
787 (zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
788 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
789 ψ hw)
791/--
792Prime-power coefficient separation for an arbitrary finite discrete \(p\)-group target map. The
793quotient-map version is applied after identifying the target with \(\mathrm{FreeGroup}(X)/\ker
794\psi\); completed derivative vectors are transported by target naturality.
795-/
796theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj
797 (p : ℕ) [Fact (Nat.Prime p)]
798 [DiscreteTopology H]
800 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
801 (w : FreeGroup X)
802 (hw :
803 zcFreeGroupFoxDerivativeVector
804 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
805 ψ w = 0) :
806 FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0 := by
807 let N : Subgroup (FreeGroup X) := ψ.ker
808 let Q : Type u := foxAlgebraicStageTargetQuotient (X := X) N
809 letI : TopologicalSpace Q := ⊥
810 letI : DiscreteTopology Q := ⟨rfl⟩
811 letI : IsTopologicalGroup Q := inferInstance
812 let e : Q ≃* H := QuotientGroup.quotientKerEquivOfSurjective ψ hψ
813 let q : FreeGroup X →* Q := QuotientGroup.mk' N
814 have he_apply (g : FreeGroup X) : e (q g) = ψ g := by
815 change QuotientGroup.quotientKerEquivOfSurjective ψ hψ
816 (QuotientGroup.mk' ψ.ker g) = ψ g
817 rfl
818 let eSymm : H →ₜ* Q :=
819 { toMonoidHom := e.symm.toMonoidHom
820 continuous_toFun := continuous_of_discreteTopology }
821 have hcompSymm : eSymm.toMonoidHom.comp ψ = q := by
822 apply MonoidHom.ext
823 intro g
824 apply e.injective
825 change e (e.symm (ψ g)) = e (q g)
826 simpa using (he_apply g).symm
827 have hQtarget :
831 e.symm hCtarget
832 have hvecQ :
833 zcFreeGroupFoxDerivativeVector
834 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
835 q w = 0 := by
836 have htarget :=
837 zcFreeGroupFoxDerivativeVector_mapTarget
838 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
840 rw [hcompSymm] at htarget
841 rw [htarget, hw]
842 rfl
843 have hq :
844 FoxCalculus.relativeFreeGroupFoxDerivative (H := Q) X q w = 0 :=
845 relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup
846 (X := X) N p hQtarget w hvecQ
847 have hcomp : e.toMonoidHom.comp q = ψ := by
848 apply MonoidHom.ext
849 intro g
850 exact he_apply g
851 have hnat :=
852 FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain
853 (H := Q) (K := H) q e.toMonoidHom w
854 rw [hcomp] at hnat
855 rw [hnat, hq]
856 rfl
858/--
859Over the finite \(p\)-group coefficient class, a zero completed universal differential on an
860arbitrary finite discrete \(p\)-group target map already forces the ordinary integral relative
861Fox derivative to vanish.
862-/
863theorem relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_pGroup_of_surj
864 (p : ℕ) [Fact (Nat.Prime p)]
865 [DiscreteTopology H]
867 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
868 (w : FreeGroup X)
869 (hw :
870 zcUniversalDifferential
871 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
872 ψ w = 0) :
873 FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0 :=
874 relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj
875 (X := X) p hCtarget ψ hψ w
876 (zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
877 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
878 ψ hw)
880end FiniteTarget
882end
884end FoxDifferential