FoxDifferential/Completed/Residue/FreeGroup/Fundamental.lean
1import FoxDifferential.Completed.Residue.FreeGroup.Boundary
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Residue/FreeGroup/Fundamental.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Residue coefficient stages
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20open scoped BigOperators
22universe u v
25variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
27section FiniteBasis
29variable [Fintype X]
31/-- Boundary-map form of the residue Fox fundamental formula. -/
33 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
35 (residueFreeGroupFoxDerivativeVector n ψ w) =
36 residueGroupRingBoundary n ψ w := by
37 let beta : FreeGroup X → ResidueGroupRing n H :=
38 fun w => residueFreeGroupFoxBoundary n ψ (residueFreeGroupFoxDerivativeVector n ψ w)
39 have hbeta :
40 IsCrossedDifferential (residueGroupRingScalar n ψ) beta :=
41 IsCrossedDifferential.map_linear
44 have hbasis :
45 ∀ x : X, beta (FreeGroup.of x) =
46 residueGroupRingBoundary n ψ (FreeGroup.of x) := by
47 intro x
48 simp only [residueFreeGroupFoxDerivativeVector_of, residueFreeGroupFoxBoundary_single, beta]
49 have hbeta_eq :
50 beta =
52 (A := ResidueGroupRing n H)
53 (residueGroupRingScalar n ψ)
54 (fun x => residueGroupRingBoundary n ψ (FreeGroup.of x)) := by
56 (A := ResidueGroupRing n H)
57 (residueGroupRingScalar n ψ)
58 (fun x => residueGroupRingBoundary n ψ (FreeGroup.of x))
59 beta hbeta hbasis
60 have hboundary_eq :
61 residueGroupRingBoundary n ψ =
63 (A := ResidueGroupRing n H)
64 (residueGroupRingScalar n ψ)
65 (fun x => residueGroupRingBoundary n ψ (FreeGroup.of x)) := by
67 (A := ResidueGroupRing n H)
68 (residueGroupRingScalar n ψ)
69 (fun x => residueGroupRingBoundary n ψ (FreeGroup.of x))
70 (residueGroupRingBoundary n ψ)
72 (by intro x; rfl)
73 exact congrFun (hbeta_eq.trans hboundary_eq.symm) w
75/-- Conditional residue Fox boundary formula. Any residue crossed differential on a free group
76with the standard basis values satisfies the residue Fox boundary formula. -/
78 (n : ℕ) (ψ : FreeGroup X →* H)
79 (delta : FreeGroup X → ResidueFreeFoxCoordinates n H X)
80 (hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta)
81 (hbasis :
82 ∀ x : X, delta (FreeGroup.of x) =
83 Pi.single x (1 : ResidueGroupRing n H))
84 (w : FreeGroup X) :
85 residueFreeGroupFoxBoundary n ψ (delta w) =
86 residueGroupRingBoundary n ψ w := by
87 have hdelta_eq :
88 delta = residueFreeGroupFoxDerivativeVector n ψ :=
89 residueFreeGroupFoxDerivativeVector_unique n ψ delta hdelta hbasis
90 rw [hdelta_eq]
91 exact residueFreeGroupFoxBoundary_derivativeVector n ψ w
93/-- Conditional residue Fox fundamental formula. The residue Fox-Euler sum computed from any
94residue crossed differential with standard basis values is `[ψ(w)] - 1`. -/
96 (n : ℕ) (ψ : FreeGroup X →* H)
97 (delta : FreeGroup X → ResidueFreeFoxCoordinates n H X)
98 (hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta)
99 (hbasis :
100 ∀ x : X, delta (FreeGroup.of x) =
101 Pi.single x (1 : ResidueGroupRing n H))
102 (w : FreeGroup X) :
103 residueGroupRingBoundary n ψ w =
104 ∑ i : X,
105 delta w i *
106 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) := by
107 simpa [residueFreeGroupFoxBoundary_apply] using
108 (residueFreeGroupFoxBoundary_of_crossedDifferential n ψ delta hdelta hbasis w).symm
110/-- Explicit `[ψ(w)] - 1` form of the conditional residue Fox-Euler formula. -/
112 (n : ℕ) (ψ : FreeGroup X →* H)
113 (delta : FreeGroup X → ResidueFreeFoxCoordinates n H X)
114 (hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta)
115 (hbasis :
116 ∀ x : X, delta (FreeGroup.of x) =
117 Pi.single x (1 : ResidueGroupRing n H))
118 (w : FreeGroup X) :
119 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) : ResidueGroupRing n H) - 1 =
120 ∑ i : X,
121 delta w i *
122 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) := by
123 simpa [residueGroupRingBoundary] using
125 n ψ delta hdelta hbasis w
127/-- Residue Fox fundamental formula, also known as the residue Fox-Euler formula:
128`[ψ(w)] - 1 = ∑ i, (∂w/∂x_i) ([ψ(x_i)] - 1)`. -/
130 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
131 residueGroupRingBoundary n ψ w =
132 ∑ i : X,
133 residueFreeGroupFoxDerivative n ψ i w *
134 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) := by
135 simpa [residueFreeGroupFoxBoundary_apply, residueFreeGroupFoxDerivative] using
136 (residueFreeGroupFoxBoundary_derivativeVector n ψ w).symm
138/-- Explicit `[ψ(w)] - 1` form of the residue Fox-Euler formula. -/
140 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
141 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) : ResidueGroupRing n H) - 1 =
142 ∑ i : X,
143 residueFreeGroupFoxDerivative n ψ i w *
144 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) := by
145 simpa [residueGroupRingBoundary] using
148end FiniteBasis
151end
153end FoxDifferential