FoxDifferential/Completed/Comparison/DiscreteCompletion.lean
1import FoxDifferential.Discrete.Naturality
2import FoxDifferential.Completed.Comparison.FiniteStage
3import ProCGroups.Completion.ProCIntegerPrimePower
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/Comparison/DiscreteCompletion.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Discrete-completed comparison
16Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
17-/
18namespace FoxDifferential
20noncomputable section
22open scoped BigOperators
24universe u
26section DiscreteCompletion
28variable {X : Type u} [DecidableEq X]
29variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
31/-- Coefficient reduction from the integral group ring `Z[F/N]` to the finite-stage target
32group algebra `(Z/nZ)[F/N]`. -/
34 GroupRing (finiteFoxStageTargetQuotient (X := X) N) →+*
35 finiteFoxStageTargetGroupAlgebra (X := X) N n :=
36 MonoidAlgebra.mapRangeRingHom
37 (finiteFoxStageTargetQuotient (X := X) N)
38 (Int.castRingHom (ModNCompletedCoeff n))
40omit [DecidableEq X] in
41/-- The finite-stage group-ring reduction sends a group-like basis element to the same quotient
42basis element with reduced coefficient. -/
43@[simp]
45 (q : finiteFoxStageTargetQuotient (X := X) N) :
46 finiteFoxStageGroupRingReduction (X := X) N n
47 (MonoidAlgebra.of ℤ (finiteFoxStageTargetQuotient (X := X) N) q) =
48 MonoidAlgebra.of (ModNCompletedCoeff n)
49 (finiteFoxStageTargetQuotient (X := X) N) q := by
50 simp only [finiteFoxStageGroupRingReduction, MonoidAlgebra.of_apply, MonoidAlgebra.mapRangeRingHom_single,
51 eq_intCast, Int.cast_one]
53omit [DecidableEq X] in
54/-- Coefficients of the finite-stage group-ring reduction are ordinary reduction modulo `n`. -/
55@[simp]
57 (x : GroupRing (finiteFoxStageTargetQuotient (X := X) N))
58 (q : finiteFoxStageTargetQuotient (X := X) N) :
59 finiteFoxStageGroupRingReduction (X := X) N n x q =
60 (x q : ModNCompletedCoeff n) := by
61 rw [finiteFoxStageGroupRingReduction, MonoidAlgebra.mapRangeRingHom_apply]
62 rfl
64/-- An integer whose image in every positive residue ring is zero is zero. -/
66 (z : ℤ) (hz : ∀ n : ℕ, 0 < n → (z : ZMod n) = 0) :
67 z = 0 := by
68 by_contra hzne
69 let n : ℕ := z.natAbs + 1
70 have hn : 0 < n := Nat.succ_pos z.natAbs
71 have hzmod : (z : ZMod n) = 0 := hz n hn
72 have hdvdInt : (n : ℤ) ∣ z := by
73 exact (ZMod.intCast_zmod_eq_zero_iff_dvd z n).mp hzmod
74 have hdvdNat : n ∣ z.natAbs := (Int.natCast_dvd).1 hdvdInt
75 have hzabs_pos : 0 < z.natAbs := Int.natAbs_pos.mpr hzne
76 have hle : n ≤ z.natAbs := Nat.le_of_dvd hzabs_pos hdvdNat
77 exact Nat.not_succ_le_self z.natAbs hle
79/-- An integer whose image in every `p^k` residue ring is zero is zero. -/
81 (p : ℕ) [Fact (Nat.Prime p)] (z : ℤ)
82 (hz : ∀ k : ℕ, (z : ZMod (p ^ k)) = 0) :
83 z = 0 := by
84 by_contra hzne
85 let k : ℕ := Nat.log p z.natAbs + 1
86 have hp1 : 1 < p := (Fact.out : Nat.Prime p).one_lt
87 have hlt : z.natAbs < p ^ k := by
88 simpa [k, Nat.succ_eq_add_one] using
89 Nat.lt_pow_succ_log_self hp1 z.natAbs
90 have hzmod : (z : ZMod (p ^ k)) = 0 := hz k
91 have hdvdInt : ((p ^ k : ℕ) : ℤ) ∣ z := by
92 exact (ZMod.intCast_zmod_eq_zero_iff_dvd z (p ^ k)).mp hzmod
93 have hdvdNat : p ^ k ∣ z.natAbs := (Int.natCast_dvd).1 hdvdInt
94 have hzabs_pos : 0 < z.natAbs := Int.natAbs_pos.mpr hzne
95 have hle : p ^ k ≤ z.natAbs := Nat.le_of_dvd hzabs_pos hdvdNat
96 exact (not_lt_of_ge hle) hlt
98omit [DecidableEq X] in
99/-- Integral group rings are torsion-free for positive natural scalar multiplication. -/
102 (hx : n • x = 0) :
103 x = 0 := by
104 ext m
105 have hcoeff : n • x m = 0 := by
107 have hmul : (n : ℤ) * x m = 0 := by
108 rw [← nsmul_eq_mul]
109 exact hcoeff
110 exact (Int.mul_eq_zero.mp hmul).resolve_left (by exact_mod_cast (Nat.ne_of_gt hn))
112omit [DecidableEq X] in
113/-- A finite-support integral group-ring element is zero if all of its positive residue
114reductions are zero. -/
116 (x : GroupRing (finiteFoxStageTargetQuotient (X := X) N))
117 (hx : ∀ n : ℕ, 0 < n →
118 finiteFoxStageGroupRingReduction (X := X) N n x = 0) :
119 x = 0 := by
120 ext q
122 intro n hn
123 have hcoeff := congrArg (fun y => y q) (hx n hn)
124 simpa using hcoeff
126omit [DecidableEq X] in
127/-- A finite-support integral group-ring element is zero if all of its `p^k` residue reductions
128are zero. -/
130 (p : ℕ) [Fact (Nat.Prime p)]
131 (x : GroupRing (finiteFoxStageTargetQuotient (X := X) N))
132 (hx : ∀ k : ℕ,
133 finiteFoxStageGroupRingReduction (X := X) N (p ^ k) x = 0) :
134 x = 0 := by
135 ext q
137 intro k
138 have hcoeff := congrArg (fun y => y q) (hx k)
139 simpa using hcoeff
141omit [DecidableEq X] in
142/-- A finite-stage residue-zero integral group-ring element is divisible by the chosen
143coefficient modulus. -/
145 {n : ℕ} (_hn : 0 < n)
146 (x : GroupRing (finiteFoxStageTargetQuotient (X := X) N))
147 (hx : finiteFoxStageGroupRingReduction (X := X) N n x = 0) :
148 ∃ y : GroupRing (finiteFoxStageTargetQuotient (X := X) N), x = n • y := by
149 classical
150 let Q := finiteFoxStageTargetQuotient (X := X) N
151 have hdvd : ∀ q : Q, (n : ℤ) ∣ x q := by
152 intro q
153 exact (ZMod.intCast_zmod_eq_zero_iff_dvd (x q) n).mp (by
154 have hcoeff :=
155 congrArg
156 (fun y : finiteFoxStageTargetGroupAlgebra (X := X) N n => y q) hx
157 simpa using hcoeff)
158 let coeff : Q → ℤ := fun q =>
159 if x q = 0 then 0 else Classical.choose (hdvd q)
160 have hcoeff_support : ∀ q : Q, coeff q ≠ 0 → q ∈ x.support := by
161 intro q hq
162 rw [Finsupp.mem_support_iff]
163 intro hxq
164 have hzero : coeff q = 0 := by
165 dsimp [coeff]
166 rw [if_pos hxq]
167 exact hq hzero
168 let y : Q →₀ ℤ := Finsupp.onFinset x.support coeff hcoeff_support
169 refine ⟨y, ?_⟩
170 ext q
171 change x q = n • coeff q
172 by_cases hxq : x q = 0
173 · simp only [hxq, ↓reduceIte, nsmul_zero, coeff]
174 · have hchoose := Classical.choose_spec (hdvd q)
175 simpa [coeff, hxq, nsmul_eq_mul] using hchoose
177/-- The finite-stage derivative vector is the image of the ordinary relative Fox derivative under
178coefficient reduction from `Z[F/N]` to `(Z/nZ)[F/N]`. -/
180 (w : FreeGroup X) :
181 finiteFoxStageDerivativeVector (X := X) N n w =
182 fun i : X =>
183 finiteFoxStageGroupRingReduction (X := X) N n
184 (FoxCalculus.relativeFreeGroupFoxDerivative
185 (H := finiteFoxStageTargetQuotient (X := X) N)
186 X (QuotientGroup.mk' N) w i) := by
187 let delta : FreeGroup X → finiteFoxStageCoordinateVector (X := X) N n :=
188 fun w i =>
189 finiteFoxStageGroupRingReduction (X := X) N n
190 (FoxCalculus.relativeFreeGroupFoxDerivative
191 (H := finiteFoxStageTargetQuotient (X := X) N)
192 X (QuotientGroup.mk' N) w i)
193 have hdelta :
194 IsCrossedDifferential (finiteFoxStageCoefficient (X := X) N n) delta := by
195 intro u v
196 funext i
197 change finiteFoxStageGroupRingReduction (X := X) N n
198 (FoxCalculus.relativeFreeGroupFoxDerivative
199 (H := finiteFoxStageTargetQuotient (X := X) N)
200 X (QuotientGroup.mk' N) (u * v) i) =
201 finiteFoxStageGroupRingReduction (X := X) N n
202 (FoxCalculus.relativeFreeGroupFoxDerivative
203 (H := finiteFoxStageTargetQuotient (X := X) N)
204 X (QuotientGroup.mk' N) u i) +
205 finiteFoxStageCoefficient (X := X) N n u *
206 finiteFoxStageGroupRingReduction (X := X) N n
207 (FoxCalculus.relativeFreeGroupFoxDerivative
208 (H := finiteFoxStageTargetQuotient (X := X) N)
209 X (QuotientGroup.mk' N) v i)
210 rw [show
211 FoxCalculus.relativeFreeGroupFoxDerivative
212 (H := finiteFoxStageTargetQuotient (X := X) N)
213 X (QuotientGroup.mk' N) (u * v) i =
214 FoxCalculus.relativeFreeGroupFoxDerivative
215 (H := finiteFoxStageTargetQuotient (X := X) N)
216 X (QuotientGroup.mk' N) u i +
217 (MonoidAlgebra.of ℤ (finiteFoxStageTargetQuotient (X := X) N)
218 (QuotientGroup.mk' N u) :
219 FoxDifferential.GroupRing (finiteFoxStageTargetQuotient (X := X) N)) *
220 FoxCalculus.relativeFreeGroupFoxDerivative
221 (H := finiteFoxStageTargetQuotient (X := X) N)
222 X (QuotientGroup.mk' N) v i by
223 simpa [Pi.add_apply, Pi.smul_apply, smul_eq_mul] using
224 congrFun
225 (FoxCalculus.relativeFreeGroupFoxDerivative_mul
226 (H := finiteFoxStageTargetQuotient (X := X) N)
227 X (QuotientGroup.mk' N) u v) i]
229 rfl
230 have hbasis :
231 ∀ x : X, delta (FreeGroup.of x) =
232 Pi.single x (1 : finiteFoxStageTargetGroupAlgebra (X := X) N n) := by
233 intro x
234 funext i
235 by_cases hix : i = x
236 · subst i
238 · simp only [FoxCalculus.relativeFreeGroupFoxDerivative_of, Pi.single_eq_of_ne hix, map_zero, delta]
239 have hdelta_eq :
240 delta = finiteFoxStageDerivativeVector (X := X) N n :=
241 finiteFoxStageDerivativeVector_unique (X := X) N n delta hdelta hbasis
242 exact (congrFun hdelta_eq w).symm
244/-- Component form of the comparison between the finite-stage derivative and the ordinary
245relative Fox derivative. -/
247 (i : X) (w : FreeGroup X) :
248 finiteFoxStageDerivative (X := X) N n i w =
249 finiteFoxStageGroupRingReduction (X := X) N n
250 (FoxCalculus.relativeFreeGroupFoxDerivative
251 (H := finiteFoxStageTargetQuotient (X := X) N)
252 X (QuotientGroup.mk' N) w i) := by
253 have h := congrFun
254 (finiteFoxStageDerivativeVector_eq_discreteReduction (X := X) N n w) i
255 simpa [finiteFoxStageDerivative] using h
257/-- One finite-stage derivative-vector vanishing says that the ordinary integral relative Fox
258derivative vector is divisible by the coefficient modulus. -/
260 {n : ℕ} (hn : 0 < n) (w : FreeGroup X)
261 (hder : finiteFoxStageDerivativeVector (X := X) N n w = 0) :
262 ∃ y : X → GroupRing (finiteFoxStageTargetQuotient (X := X) N),
263 FoxCalculus.relativeFreeGroupFoxDerivative
264 (H := finiteFoxStageTargetQuotient (X := X) N)
265 X (QuotientGroup.mk' N) w = n • y := by
266 classical
267 have hred :
268 ∀ i : X,
269 finiteFoxStageGroupRingReduction (X := X) N n
270 (FoxCalculus.relativeFreeGroupFoxDerivative
271 (H := finiteFoxStageTargetQuotient (X := X) N)
272 X (QuotientGroup.mk' N) w i) = 0 := by
273 intro i
274 have hcomp :=
275 congrFun (finiteFoxStageDerivativeVector_eq_discreteReduction (X := X) N n w) i
276 have hzero := congrFun hder i
277 exact hcomp.symm.trans hzero
278 choose y hy using fun i =>
280 (FoxCalculus.relativeFreeGroupFoxDerivative
281 (H := finiteFoxStageTargetQuotient (X := X) N)
282 X (QuotientGroup.mk' N) w i)
283 (hred i)
284 refine ⟨y, ?_⟩
285 funext i
286 exact hy i
288/-- Residue-universal version of one-modulus divisibility for the ordinary integral relative
289Fox derivative vector. -/
291 [Fintype X] {n : ℕ} (hn : 0 < n) (w : FreeGroup X)
292 (hres : residueUniversalDifferential n (QuotientGroup.mk' N) w = 0) :
293 ∃ y : X → GroupRing (finiteFoxStageTargetQuotient (X := X) N),
294 FoxCalculus.relativeFreeGroupFoxDerivative
295 (H := finiteFoxStageTargetQuotient (X := X) N)
296 X (QuotientGroup.mk' N) w = n • y := by
297 exact
299 (X := X) N hn w
301 (X := X) N n w).2 hres)
303/-- If every positive finite-stage derivative vanishes, then the ordinary integral relative Fox
304derivative vanishes. -/
306 (w : FreeGroup X)
307 (hder :
308 ∀ n : ℕ, 0 < n →
309 ∀ i : X, finiteFoxStageDerivative (X := X) N n i w = 0) :
310 FoxCalculus.relativeFreeGroupFoxDerivative
311 (H := finiteFoxStageTargetQuotient (X := X) N)
312 X (QuotientGroup.mk' N) w = 0 := by
313 funext i
315 (X := X) N
316 intro n hn
317 exact
318 (finiteFoxStageDerivative_eq_discreteReduction (X := X) N n i w).symm.trans
319 (hder n hn i)
321/-- If every `p^k` finite-stage derivative vanishes, then the ordinary integral relative Fox
322derivative vanishes. -/
324 (p : ℕ) [Fact (Nat.Prime p)] (w : FreeGroup X)
325 (hder :
326 ∀ k : ℕ,
327 ∀ i : X, finiteFoxStageDerivative (X := X) N (p ^ k) i w = 0) :
328 FoxCalculus.relativeFreeGroupFoxDerivative
329 (H := finiteFoxStageTargetQuotient (X := X) N)
330 X (QuotientGroup.mk' N) w = 0 := by
331 funext i
333 (X := X) N p
334 intro k
335 exact
336 (finiteFoxStageDerivative_eq_discreteReduction (X := X) N (p ^ k) i w).symm.trans
337 (hder k i)
339section CompletedProjection
341variable (C : ProCGroups.FiniteGroupClass.{u})
342variable [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
343variable [IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
345/-- Projecting the completed `Z_C` derivative to a finite pro-`C` target stage gives the stage
346map applied to the reduced ordinary relative Fox derivative. -/
348 (i : X) (w : FreeGroup X)
349 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
351 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
352 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
353 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
354 (zcFiniteStageTarget X N) C j.2
355 (finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
356 (FoxCalculus.relativeFreeGroupFoxDerivative
357 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) := by
358 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
359 rw [zcFreeGroupFoxDerivative_finiteStageProjection C N j i w]
360 rw [finiteFoxStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]
362/-- Vector form of the discrete-to-completed projection comparison. -/
364 (w : FreeGroup X)
365 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
366 (fun i : X =>
368 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
369 fun i : X =>
370 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
371 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
372 (zcFiniteStageTarget X N) C j.2
373 (finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
374 (FoxCalculus.relativeFreeGroupFoxDerivative
375 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by
376 funext i
378 (C := C) (X := X) N i w j
380/-- The completed `Z_C` component derivative is uniquely determined by the finite-stage projections
381of the ordinary relative Fox derivative after coefficient reduction. -/
383 (i : X)
384 (delta : FreeGroup X →
386 (hprojection : ∀ w
387 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
388 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta w) =
389 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
390 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
391 (zcFiniteStageTarget X N) C j.2
392 (finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
393 (FoxCalculus.relativeFreeGroupFoxDerivative
394 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)))) :
395 delta = zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i := by
397 (C := C) (X := X) N i delta ?_
398 intro w j
399 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
400 rw [hprojection w j]
401 rw [← finiteFoxStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]
403/-- Existence and uniqueness of the completed `Z_C` component derivative characterized by the
406 (i : X) :
407 ∃! delta : FreeGroup X →
409 ∀ w
410 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
411 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta w) =
412 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
413 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
414 (zcFiniteStageTarget X N) C j.2
415 (finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
416 (FoxCalculus.relativeFreeGroupFoxDerivative
417 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) := by
418 refine ⟨zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i, ?_, ?_⟩
419 · intro w j
421 (C := C) (X := X) N i w j
422 · intro delta hprojection
424 (C := C) (X := X) N i delta hprojection
426/-- The completed `Z_C` derivative vector is uniquely determined by the finite-stage projections of
427the ordinary relative Fox derivative after coefficient reduction. -/
429 (delta : FreeGroup X →
430 ZCFreeFoxCoordinates C (X := X) (H := zcFiniteStageTarget X N))
431 (hprojection : ∀ w
432 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
433 (fun i : X =>
434 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta w i)) =
435 fun i : X =>
436 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
437 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
438 (zcFiniteStageTarget X N) C j.2
439 (finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
440 (FoxCalculus.relativeFreeGroupFoxDerivative
441 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) :
442 delta = zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) := by
444 (C := C) (X := X) N delta ?_
445 intro w j
446 funext i
447 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
448 have hcoord := congrFun (hprojection w j) i
449 rw [hcoord]
450 rw [← finiteFoxStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]
452/-- Existence and uniqueness of the completed `Z_C` derivative vector characterized by the
455 ∃! delta : FreeGroup X →
456 ZCFreeFoxCoordinates C (X := X) (H := zcFiniteStageTarget X N),
457 ∀ w
458 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
459 (fun i : X =>
461 (delta w i)) =
462 fun i : X =>
463 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
464 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
465 (zcFiniteStageTarget X N) C j.2
466 (finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
467 (FoxCalculus.relativeFreeGroupFoxDerivative
468 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by
469 refine ⟨zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N), ?_, ?_⟩
470 · intro w j
472 (C := C) (X := X) N w j
473 · intro delta hprojection
475 (C := C) (X := X) N delta hprojection
477/-- Projecting the completed Fox-Euler formula and reducing the coefficients identifies the
478derivative coordinates with the ordinary relative Fox derivative. -/
480 [Fintype X]
481 (w : FreeGroup X)
482 (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
484 (zcCompletedGroupAlgebraBoundary C (QuotientGroup.mk' N) w) =
485 ∑ i : X,
486 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
487 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
488 (zcFiniteStageTarget X N) C j.2
489 (finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
490 (FoxCalculus.relativeFreeGroupFoxDerivative
491 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) *
493 (zcGroupLike C (zcFiniteStageTarget X N)
494 (QuotientGroup.mk' N (FreeGroup.of i)) - 1) := by
496 (C := C) (X := X) N w j]
497 apply Finset.sum_congr rfl
498 intro i hi
499 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
500 rw [finiteFoxStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]
502/-- Over the all-finite coefficient class, a zero completed derivative vector on the finite
503quotient map already forces the ordinary integral relative Fox derivative to vanish. -/
505 [DiscreteTopology (finiteFoxStageTargetQuotient (X := X) N)]
506 [Finite (finiteFoxStageTargetQuotient (X := X) N)]
507 (w : FreeGroup X)
508 (hw :
510 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
511 (QuotientGroup.mk' N) w = 0) :
512 FoxCalculus.relativeFreeGroupFoxDerivative
513 (H := finiteFoxStageTargetQuotient (X := X) N)
514 X (QuotientGroup.mk' N) w = 0 := by
516 (X := X) N w
517 intro n hn i
519 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}) :=
521 have hjmod : j.modulus = n := rfl
522 have hCtarget :
523 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
524 (finiteFoxStageTargetQuotient (X := X) N) := by
525 exact (inferInstance :
526 Finite (finiteFoxStageTargetQuotient (X := X) N))
527 have hcomponent :
529 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
530 (QuotientGroup.mk' N) i w = 0 := by
531 simpa [zcFreeGroupFoxDerivative] using congrFun hw i
532 simpa [j, hjmod] using
534 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
535 (X := X) N
537 (hCtarget := hCtarget)
538 j i hcomponent
540/-- Over the all-finite coefficient class, a zero completed universal differential on the finite
541quotient map already forces the ordinary integral relative Fox derivative to vanish. -/
543 [DiscreteTopology (finiteFoxStageTargetQuotient (X := X) N)]
544 [Finite (finiteFoxStageTargetQuotient (X := X) N)]
545 (w : FreeGroup X)
546 (hw :
548 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
549 (QuotientGroup.mk' N) w = 0) :
550 FoxCalculus.relativeFreeGroupFoxDerivative
551 (H := finiteFoxStageTargetQuotient (X := X) N)
552 X (QuotientGroup.mk' N) w = 0 := by
553 exact
555 (X := X) N w
557 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
558 (QuotientGroup.mk' N) hw)
560/-- Over the finite `p`-group coefficient class, a zero completed derivative vector on the finite
561quotient map forces the ordinary integral relative Fox derivative to vanish, using only the
562prime-power coefficient stages. -/
564 (p : ℕ) [Fact (Nat.Prime p)]
565 [DiscreteTopology (finiteFoxStageTargetQuotient (X := X) N)]
566 (hCtarget :
568 (finiteFoxStageTargetQuotient (X := X) N))
569 (w : FreeGroup X)
570 (hw :
572 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
573 (QuotientGroup.mk' N) w = 0) :
574 FoxCalculus.relativeFreeGroupFoxDerivative
575 (H := finiteFoxStageTargetQuotient (X := X) N)
576 X (QuotientGroup.mk' N) w = 0 := by
578 (X := X) N p w
579 intro k i
581 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}) :=
583 have hjmod : j.modulus = p ^ k := rfl
584 have hcomponent :
586 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
587 (QuotientGroup.mk' N) i w = 0 := by
588 simpa [zcFreeGroupFoxDerivative] using congrFun hw i
589 simpa [j, hjmod] using
591 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
592 (X := X) N
593 (hIso := (ProCGroups.FiniteGroupClass.pGroup_formation p).isomClosed)
594 (hCtarget := hCtarget)
595 j i hcomponent
597/-- Over the finite `p`-group coefficient class, a zero completed universal differential on the
598finite quotient map already forces the ordinary integral relative Fox derivative to vanish, using
599only the prime-power coefficient stages. -/
601 (p : ℕ) [Fact (Nat.Prime p)]
602 [DiscreteTopology (finiteFoxStageTargetQuotient (X := X) N)]
603 (hCtarget :
605 (finiteFoxStageTargetQuotient (X := X) N))
606 (w : FreeGroup X)
607 (hw :
609 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
610 (QuotientGroup.mk' N) w = 0) :
611 FoxCalculus.relativeFreeGroupFoxDerivative
612 (H := finiteFoxStageTargetQuotient (X := X) N)
613 X (QuotientGroup.mk' N) w = 0 := by
614 exact
616 (X := X) N p hCtarget w
618 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
619 (QuotientGroup.mk' N) hw)
621end CompletedProjection
623end DiscreteCompletion
625section FiniteTarget
627variable {X : Type u} [DecidableEq X]
628variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
630/-- All-finite coefficient separation for an arbitrary finite discrete target map.
632The quotient-map version is applied after identifying the target with
635 [DiscreteTopology H] [Finite H]
636 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
637 (w : FreeGroup X)
638 (hw :
640 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
641 ψ w = 0) :
642 FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0 := by
643 let N : Subgroup (FreeGroup X) := ψ.ker
644 let Q : Type u := finiteFoxStageTargetQuotient (X := X) N
645 letI : TopologicalSpace Q := ⊥
646 letI : DiscreteTopology Q := ⟨rfl⟩
647 letI : IsTopologicalGroup Q := inferInstance
648 let e : Q ≃* H := QuotientGroup.quotientKerEquivOfSurjective ψ hψ
649 letI : Finite Q := Finite.of_injective e e.injective
650 let q : FreeGroup X →* Q := QuotientGroup.mk' N
651 have he_apply (g : FreeGroup X) : e (q g) = ψ g := by
652 change QuotientGroup.quotientKerEquivOfSurjective ψ hψ
653 (QuotientGroup.mk' ψ.ker g) = ψ g
654 rfl
655 let eSymm : H →ₜ* Q :=
656 { toMonoidHom := e.symm.toMonoidHom
657 continuous_toFun := continuous_of_discreteTopology }
658 have hcompSymm : eSymm.toMonoidHom.comp ψ = q := by
659 apply MonoidHom.ext
660 intro g
661 apply e.injective
662 change e (e.symm (ψ g)) = e (q g)
663 simpa using (he_apply g).symm
664 have hvecQ :
666 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
667 q w = 0 := by
668 have htarget :=
670 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
672 rw [hcompSymm] at htarget
673 rw [htarget, hw]
674 rfl
675 have hq :
676 FoxCalculus.relativeFreeGroupFoxDerivative (H := Q) X q w = 0 :=
678 (X := X) N w hvecQ
679 have hcomp : e.toMonoidHom.comp q = ψ := by
680 apply MonoidHom.ext
681 intro g
682 exact he_apply g
683 have hnat :=
684 FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain
685 (H := Q) (K := H) q e.toMonoidHom w
686 rw [hcomp] at hnat
687 rw [hnat, hq]
688 rfl
690/-- Over the all-finite coefficient class, a zero completed universal differential on an
691arbitrary finite discrete target map already forces the ordinary integral relative Fox derivative
692to vanish. -/
694 [DiscreteTopology H] [Finite H]
695 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
696 (w : FreeGroup X)
697 (hw :
699 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
700 ψ w = 0) :
701 FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0 :=
703 (X := X) ψ hψ w
705 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u}))
706 ψ hw)
708/-- Prime-power coefficient separation for an arbitrary finite discrete `p`-group target map.
710The quotient-map version is applied after identifying the target with
713 (p : ℕ) [Fact (Nat.Prime p)]
714 [DiscreteTopology H]
715 (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
716 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
717 (w : FreeGroup X)
718 (hw :
720 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
721 ψ w = 0) :
722 FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0 := by
723 let N : Subgroup (FreeGroup X) := ψ.ker
724 let Q : Type u := finiteFoxStageTargetQuotient (X := X) N
725 letI : TopologicalSpace Q := ⊥
726 letI : DiscreteTopology Q := ⟨rfl⟩
727 letI : IsTopologicalGroup Q := inferInstance
728 let e : Q ≃* H := QuotientGroup.quotientKerEquivOfSurjective ψ hψ
729 let q : FreeGroup X →* Q := QuotientGroup.mk' N
730 have he_apply (g : FreeGroup X) : e (q g) = ψ g := by
731 change QuotientGroup.quotientKerEquivOfSurjective ψ hψ
732 (QuotientGroup.mk' ψ.ker g) = ψ g
733 rfl
734 let eSymm : H →ₜ* Q :=
735 { toMonoidHom := e.symm.toMonoidHom
736 continuous_toFun := continuous_of_discreteTopology }
737 have hcompSymm : eSymm.toMonoidHom.comp ψ = q := by
738 apply MonoidHom.ext
739 intro g
740 apply e.injective
741 change e (e.symm (ψ g)) = e (q g)
742 simpa using (he_apply g).symm
743 have hQtarget :
746 (ProCGroups.FiniteGroupClass.pGroup_formation p).isomClosed
747 e.symm hCtarget
748 have hvecQ :
750 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
751 q w = 0 := by
752 have htarget :=
754 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
755 (ProCGroups.FiniteGroupClass.pGroup_hereditary p) ψ eSymm w
756 rw [hcompSymm] at htarget
757 rw [htarget, hw]
758 rfl
759 have hq :
760 FoxCalculus.relativeFreeGroupFoxDerivative (H := Q) X q w = 0 :=
762 (X := X) N p hQtarget w hvecQ
763 have hcomp : e.toMonoidHom.comp q = ψ := by
764 apply MonoidHom.ext
765 intro g
766 exact he_apply g
767 have hnat :=
768 FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain
769 (H := Q) (K := H) q e.toMonoidHom w
770 rw [hcomp] at hnat
771 rw [hnat, hq]
772 rfl
774/-- Over the finite `p`-group coefficient class, a zero completed universal differential on an
776derivative to vanish. -/
778 (p : ℕ) [Fact (Nat.Prime p)]
779 [DiscreteTopology H]
780 (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
781 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
782 (w : FreeGroup X)
783 (hw :
785 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
786 ψ w = 0) :
787 FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0 :=
789 (X := X) p hCtarget ψ hψ w
791 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u}))
792 ψ hw)
794end FiniteTarget
796end
798end FoxDifferential