Yamaguchi Lean 4 Library
FoxDifferential/Completed/Comparison/FiniteStage.lean
FoxDifferential/Completed/Comparison/FiniteStage/Source

FoxDifferential/Completed/Comparison/FiniteStage.lean

1import FoxDifferential.Completed.DifferentialModule.Identity
2import FoxDifferential.Completed.FiniteStage.MagnusQuotient
3import FoxDifferential.Completed.ProCIntegerCoefficients.Naturality
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/Comparison/FiniteStage.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
16Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.
17-/
18namespace FoxDifferential
20noncomputable section
22open scoped BigOperators
24universe u
26section FiniteStageCompletedComparison
28variable (C : ProCGroups.FiniteGroupClass.{u})
29variable {X : Type u} [DecidableEq X]
30variable (N : Subgroup (FreeGroup X)) [N.Normal]
31variable [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
32variable [IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
34abbrev zcFiniteStageTarget (X : Type u) [DecidableEq X]
35 (N : Subgroup (FreeGroup X)) [N.Normal] :=
38/-- The coefficient homomorphism obtained by projecting the completed `Z_C[[F/N]]`
39coefficient homomorphism to one finite pro-`C` stage. -/
42 FreeGroup X →* ZCCompletedGroupAlgebraStage C (zcFiniteStageTarget X N) j where
43 toFun w :=
45 (zcCompletedGroupAlgebraScalar C (QuotientGroup.mk' N) w)
46 map_one' := by
48 map_mul' u v := by
49 simp only [zcCompletedGroupAlgebraScalar, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
51 MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
53/-- Projecting the completed coefficient homomorphism agrees with the finite-stage quotient map
54applied to the ordinary finite Fox coefficient homomorphism at the same modulus. -/
55@[simp]
58 (w : FreeGroup X) :
60 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
63 (finiteFoxStageCoefficient (X := X) N j.1.modulus w)) := by
64 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
66 rfl
68/-- The projected completed Fox derivative vector is a crossed differential at one finite
69pro-`C` stage. -/
74 (fun w : FreeGroup X =>
75 fun i : X =>
77 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) := by
78 intro u v
79 funext i
80 have h :=
81 congrArg
83 (congrFun
84 (zcFreeGroupFoxDerivativeVector_mul C (QuotientGroup.mk' N) u v) i)
85 simpa only [Pi.add_apply, Pi.smul_apply, smul_eq_mul, zcCompletedGroupAlgebraScalarStage,
88/-- The finite-stage Fox derivative vector, pushed to one pro-`C` quotient stage of the target,
89is a crossed differential with the projected completed coefficient homomorphism. -/
94 (fun w : FreeGroup X =>
95 fun i : X =>
96 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
99 (finiteFoxStageDerivative (X := X) N j.1.modulus i w)) := by
100 intro u v
101 funext i
102 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
103 have h :=
104 congrArg
107 (finiteFoxStageDerivative_mul (X := X) N j.1.modulus i u v)
108 simpa only [Pi.add_apply, Pi.smul_apply, smul_eq_mul, finiteFoxStageDerivative,
111/-- Projecting the completed derivative vector to a finite pro-`C` stage recovers the finite
112Fox derivative vector, mapped to that stage. -/
115 (w : FreeGroup X) :
116 (fun i : X =>
118 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
119 fun i : X =>
120 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
123 (finiteFoxStageDerivative (X := X) N j.1.modulus i w) := by
124 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
125 let projected : FreeGroup X →
127 fun w i =>
129 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)
130 let staged : FreeGroup X →
132 fun w i =>
135 (finiteFoxStageDerivative (X := X) N j.1.modulus i w)
136 have hprojected :
137 projected =
141 (fun x : X =>
142 Pi.single x
147 (fun x : X =>
148 Pi.single x
150 projected ?_ ?_
151 · simpa [projected] using
153 · intro x
154 funext i
155 by_cases hi : i = x
156 · subst i
158 projected]
160 projected]
161 have hstaged :
162 staged =
166 (fun x : X =>
167 Pi.single x
172 (fun x : X =>
173 Pi.single x
175 staged ?_ ?_
176 · simpa [staged] using
178 · intro x
179 funext i
180 have h :=
181 congrFun (finiteFoxStageDerivativeVector_of (X := X) N j.1.modulus x) i
182 change
185 (finiteFoxStageDerivativeVector (X := X) N j.1.modulus
186 (FreeGroup.of x) i) =
187 ((Pi.single x
190 rw [h]
191 by_cases hi : i = x
192 · subst i
193 simp only [Pi.single_eq_same, map_one]
194 · simp only [Pi.single_eq_of_ne hi, map_zero]
195 exact congrFun (hprojected.trans hstaged.symm) w
197/-- Component form of `zcFreeGroupFoxDerivativeVector_finiteStageProjection`. -/
198@[simp]
201 (i : X) (w : FreeGroup X) :
203 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
204 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
207 (finiteFoxStageDerivative (X := X) N j.1.modulus i w)) := by
208 have h := congrFun
212/-- If the universal completed differential of a word is zero, then every finite `Z_C` stage
213projection of its finite Fox derivative vanishes. -/
216 (i : X) {w : FreeGroup X}
217 (hw : zcUniversalDifferential C (QuotientGroup.mk' N) w = 0) :
218 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
221 (finiteFoxStageDerivative (X := X) N j.1.modulus i w)) = 0 := by
222 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
223 have hcompleted :
224 zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w = 0 :=
226 (C := C) (QuotientGroup.mk' N) i hw
227 have hprojection :
229 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) = 0 := by
230 simpa using
231 congrArg
233 hcompleted
234 exact
235 (zcFreeGroupFoxDerivative_finiteStageProjection C N j i w).symm.trans hprojection
237/-- Vector form of
241 {w : FreeGroup X}
242 (hw : zcUniversalDifferential C (QuotientGroup.mk' N) w = 0) :
243 (fun i : X =>
244 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
247 (finiteFoxStageDerivative (X := X) N j.1.modulus i w)) = 0 := by
248 funext i
249 exact
251 (C := C) (X := X) N j i hw
253/-- At the identity quotient stage, a zero universal completed differential forces the finite Fox
254derivative itself to vanish modulo every allowed pro-`C` coefficient modulus. -/
256 [DiscreteTopology (zcFiniteStageTarget X N)]
258 (hCtarget : C.pred (zcFiniteStageTarget X N))
260 (i : X) {w : FreeGroup X}
261 (hw : zcUniversalDifferential C (QuotientGroup.mk' N) w = 0) :
262 finiteFoxStageDerivative (X := X) N j.modulus i w = 0 := by
263 letI : Fact (0 < j.modulus) := ⟨j.positive⟩
264 let U : CompletedGroupAlgebraIndexInClass (zcFiniteStageTarget X N) C :=
266 have hstage :
269 (finiteFoxStageDerivative (X := X) N j.modulus i w) = 0 := by
270 simpa [U] using
272 (C := C) (X := X) N (j, U) i hw
273 exact
275 j.modulus C (zcFiniteStageTarget X N) hIso hCtarget) hstage
277/-- Vector form of
280 [DiscreteTopology (zcFiniteStageTarget X N)]
282 (hCtarget : C.pred (zcFiniteStageTarget X N))
284 {w : FreeGroup X}
285 (hw : zcUniversalDifferential C (QuotientGroup.mk' N) w = 0) :
286 finiteFoxStageDerivativeVector (X := X) N j.modulus w = 0 := by
287 funext i
288 exact
290 (C := C) (X := X) N hIso hCtarget j i hw
292/-- At the identity quotient stage, a zero completed component derivative forces the finite Fox
293derivative itself to vanish modulo the corresponding pro-`C` coefficient modulus. -/
295 [DiscreteTopology (zcFiniteStageTarget X N)]
297 (hCtarget : C.pred (zcFiniteStageTarget X N))
299 (i : X) {w : FreeGroup X}
300 (hw : zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w = 0) :
301 finiteFoxStageDerivative (X := X) N j.modulus i w = 0 := by
302 letI : Fact (0 < j.modulus) := ⟨j.positive⟩
303 let U : CompletedGroupAlgebraIndexInClass (zcFiniteStageTarget X N) C :=
305 have hstage :
308 (finiteFoxStageDerivative (X := X) N j.modulus i w) = 0 := by
309 have hprojection :
311 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) = 0 := by
312 simpa using
313 congrArg
315 hw
316 exact
318 hprojection
319 exact
321 j.modulus C (zcFiniteStageTarget X N) hIso hCtarget) hstage
323/-- Vector form of
326 [DiscreteTopology (zcFiniteStageTarget X N)]
328 (hCtarget : C.pred (zcFiniteStageTarget X N))
330 {w : FreeGroup X}
331 (hw : zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w = 0) :
332 finiteFoxStageDerivativeVector (X := X) N j.modulus w = 0 := by
333 funext i
334 have hcoord :
335 zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w = 0 := by
336 simpa [zcFreeGroupFoxDerivative] using congrFun hw i
337 exact
339 (C := C) (X := X) N hIso hCtarget j i hcoord
341/-- At the identity quotient stage, it is enough for the completed derivative vector to vanish
342after projection to the selected finite coefficient stage. -/
344 [DiscreteTopology (zcFiniteStageTarget X N)]
346 (hCtarget : C.pred (zcFiniteStageTarget X N))
348 {w : FreeGroup X}
349 (hw :
350 (fun i : X =>
353 C (zcFiniteStageTarget X N) hIso hCtarget)
354 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) = 0) :
355 finiteFoxStageDerivativeVector (X := X) N j.modulus w = 0 := by
356 funext i
357 letI : Fact (0 < j.modulus) := ⟨j.positive⟩
358 let U : CompletedGroupAlgebraIndexInClass (zcFiniteStageTarget X N) C :=
360 have hstage :
363 (finiteFoxStageDerivative (X := X) N j.modulus i w) = 0 := by
364 have hcoord := congrFun hw i
365 simpa [U] using
366 (zcFreeGroupFoxDerivative_finiteStageProjection C N (j, U) i w).symm.trans hcoord
367 exact
369 j.modulus C (zcFiniteStageTarget X N) hIso hCtarget) hstage
371/-- A completed component derivative is determined by all of its finite pro-`C` stage
372projections. -/
374 (i : X)
375 (delta : FreeGroup X → ZCCompletedGroupAlgebra C (zcFiniteStageTarget X N))
376 (hprojection : ∀ w
379 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
382 (finiteFoxStageDerivative (X := X) N j.1.modulus i w))) :
383 delta = zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i := by
384 funext w
385 apply Subtype.ext
386 funext j
389 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w)
390 rw [hprojection w j, zcFreeGroupFoxDerivative_finiteStageProjection C N j i w]
392/-- Existence and uniqueness of the completed component derivative characterized by all finite
393pro-`C` stage projection formulas. -/
395 (i : X) :
396 ∃! delta : FreeGroup X → ZCCompletedGroupAlgebra C (zcFiniteStageTarget X N),
399 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
402 (finiteFoxStageDerivative (X := X) N j.1.modulus i w)) := by
403 refine ⟨zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i, ?_, ?_⟩
404 · intro w j
406 · intro delta hprojection
409/-- The completed derivative vector is determined by all finite pro-`C` stage projection
410formulas. -/
412 (delta : FreeGroup X →
414 (hprojection : ∀ w
416 (fun i : X =>
418 (delta w i)) =
419 fun i : X =>
420 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
423 (finiteFoxStageDerivative (X := X) N j.1.modulus i w)) :
424 delta = zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) := by
425 funext w i
426 apply Subtype.ext
427 funext j
430 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)
431 have hcoord := congrFun (hprojection w j) i
432 rw [hcoord]
433 exact (by
437/-- Existence and uniqueness of the completed derivative vector characterized by all finite
438pro-`C` stage projection formulas. -/
440 ∃! delta : FreeGroup X →
443 (fun i : X =>
445 (delta w i)) =
446 fun i : X =>
447 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
450 (finiteFoxStageDerivative (X := X) N j.1.modulus i w) := by
451 refine ⟨zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N), ?_, ?_⟩
452 · intro w j
454 · intro delta hprojection
456 C N delta hprojection
458section FundamentalFormula
460variable [Fintype X]
462/-- The completed Fox-Euler formula for the quotient map `F -> F/N`. -/
464 (w : FreeGroup X) :
465 zcCompletedGroupAlgebraBoundary C (QuotientGroup.mk' N) w =
466 ∑ i : X,
467 zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w *
469 (QuotientGroup.mk' N (FreeGroup.of i)) - 1) := by
470 exact zcFreeGroupFoxDerivative_fundamental_formula C (QuotientGroup.mk' N) w
472/-- Projection of the completed Fox-Euler formula to one finite pro-`C` target stage. -/
474 (w : FreeGroup X)
477 (zcCompletedGroupAlgebraBoundary C (QuotientGroup.mk' N) w) =
478 ∑ i : X,
480 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) *
483 (QuotientGroup.mk' N (FreeGroup.of i)) - 1) := by
484 have h := congrArg
488 simpa using h
490/-- Projection of the completed Fox-Euler formula with derivative coordinates rewritten as
491finite Fox derivatives at the selected pro-`C` coefficient modulus. -/
493 (w : FreeGroup X)
496 (zcCompletedGroupAlgebraBoundary C (QuotientGroup.mk' N) w) =
497 ∑ i : X,
498 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
501 (finiteFoxStageDerivative (X := X) N j.1.modulus i w)) *
504 (QuotientGroup.mk' N (FreeGroup.of i)) - 1) := by
506 apply Finset.sum_congr rfl
507 intro i _
510end FundamentalFormula
512end FiniteStageCompletedComparison
514section FiniteTargetStageZero
516variable (C : ProCGroups.FiniteGroupClass.{u})
518variable {X : Type u} [DecidableEq X]
519variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
520variable [DiscreteTopology H]
522include hC
524/-- Surjective-target form of finite-stage zero from completed universal zero.
526The quotient-map theorem is applied after transporting the target along
527`FreeGroup X / ker ψ ≃* H`; this avoids redoing the quotient identification at Crowell use sites. -/
530 (hCH : C.pred H)
531 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
533 {w : FreeGroup X}
534 (hw : zcUniversalDifferential C ψ w = 0) :
535 finiteFoxStageDerivativeVector (X := X) ψ.ker j.modulus w = 0 := by
536 let N : Subgroup (FreeGroup X) := ψ.ker
537 let Q : Type u := finiteFoxStageTargetQuotient (X := X) N
538 letI : TopologicalSpace Q := ⊥
539 letI : DiscreteTopology Q := ⟨rfl⟩
540 letI : IsTopologicalGroup Q := inferInstance
541 let e : Q ≃* H := QuotientGroup.quotientKerEquivOfSurjective ψ hψ
542 let q : FreeGroup X →* Q := QuotientGroup.mk' N
543 have hQ : C.pred Q :=
545 have he_apply (g : FreeGroup X) : e (q g) = ψ g := by
546 change QuotientGroup.quotientKerEquivOfSurjective ψ hψ
547 (QuotientGroup.mk' ψ.ker g) = ψ g
548 rfl
549 let eSymm : H →ₜ* Q :=
550 { toMonoidHom := e.symm.toMonoidHom
551 continuous_toFun := continuous_of_discreteTopology }
552 have hcompSymm : eSymm.toMonoidHom.comp ψ = q := by
553 apply MonoidHom.ext
554 intro g
555 apply e.injective
556 change e (e.symm (ψ g)) = e (q g)
557 simpa using (he_apply g).symm
558 have hq :
560 have htarget :
561 zcUniversalDifferential C (eSymm.toMonoidHom.comp ψ) w = 0 :=
563 rwa [hcompSymm] at htarget
564 exact
566 (C := C) (X := X) N hIso hQ j hq
568/-- Finite-quotient commutator conclusion from completed universal zero, assuming only the
569finite-stage Magnus reverse inclusion at the pro-`C` coefficient moduli that kill the finite
570kernel.
572The coefficient modulus is not an extra hypothesis: under formation plus hereditary hypotheses,
573`ProCIntegerIndex.exists_index_kills_finite_group_of_mem` chooses an allowed modulus that kills
574`ker β`, and this is the only finite-stage Magnus input used below. -/
576 [Fintype X]
578 (hCH : C.pred H)
579 {Q : Type u} [Group Q]
580 (α : FreeGroup X →* Q) (hα : Function.Surjective α)
581 (β : Q →* H) (hβ : Function.Surjective β)
582 (hCker : C.pred β.ker)
583 (hmag :
585 (∀ k : β.ker, k ^ j.modulus = 1) →
586 ∀ w : FreeGroup X,
587 w ∈ (β.comp α).ker →
589 (QuotientGroup.mk' (β.comp α).ker) w = 0 →
591 (F := FreeGroup X) (β.comp α).ker j.modulus)
592 {w : FreeGroup X}
593 (hwker : w ∈ (β.comp α).ker)
594 (hzero : zcUniversalDifferential C (β.comp α) w = 0) :
595 (⟨α w, by
596 change β (α w) = 1
597 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
598 commutator β.ker := by
599 letI : Finite β.ker := hForm.finiteOnly hCker
601 (C := C) hForm hC hCker with ⟨j, hpow⟩
602 have hψ : Function.Surjective (β.comp α) := by
603 intro h
604 rcases hβ h with ⟨q, rfl⟩
605 rcases hα q with ⟨g, rfl⟩
606 exact ⟨g, rfl⟩
607 have hder :
608 finiteFoxStageDerivativeVector (X := X) (β.comp α).ker j.modulus w = 0 :=
610 (C := C) (X := X) hC hForm.isomClosed hCH
611 (β.comp α) hψ j hzero
612 have hres :
614 (QuotientGroup.mk' (β.comp α).ker) w = 0 :=
616 (X := X) (β.comp α).ker j.modulus w).1 hder
617 exact
619 (X := X) α β j.modulus hpow (hmag j hpow) hwker hres
621end FiniteTargetStageZero
623end
625end FoxDifferential