FoxDifferential/Common/FoxBoundary.lean
1import FoxDifferential.Common.FreeCrossedDifferential
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Common/FoxBoundary.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Universal Fox calculus
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
24section CoefficientBoundary
26variable {R : Type u} [Ring R]
27variable {G : Type v} [Group G]
29/-- The Fox boundary crossed differential attached to a coefficient homomorphism:
30`g ↦ coeff g - 1`. -/
31def coefficientFoxBoundary (coeff : G →* R) (g : G) : R :=
32 coeff g - 1
34/-- The coefficient Fox boundary sends the identity to zero. -/
35@[simp]
36theorem coefficientFoxBoundary_one (coeff : G →* R) :
37 coefficientFoxBoundary coeff 1 = 0 := by
38 simp only [coefficientFoxBoundary, map_one, sub_self]
40/-- Product rule for the coefficient Fox boundary `g ↦ coeff g - 1`. -/
41theorem coefficientFoxBoundary_mul (coeff : G →* R) (g h : G) :
42 coefficientFoxBoundary coeff (g * h) =
43 coefficientFoxBoundary coeff g + coeff g • coefficientFoxBoundary coeff h := by
45 change coeff g * coeff h - 1 = coeff g - 1 + coeff g * (coeff h - 1)
46 rw [sub_eq_add_neg, sub_eq_add_neg, sub_eq_add_neg, mul_add, mul_neg, mul_one]
47 rw [show coeff g + -1 + (coeff g * coeff h + -coeff g) =
48 coeff g + -coeff g + (coeff g * coeff h + -1) by ac_rfl]
49 simp only [add_neg_cancel, zero_add]
51/-- The coefficient Fox boundary is a crossed differential. -/
52theorem coefficientFoxBoundary_isCrossedDifferential (coeff : G →* R) :
53 IsCrossedDifferential coeff (coefficientFoxBoundary coeff) := by
54 intro g h
55 exact coefficientFoxBoundary_mul coeff g h
57end CoefficientBoundary
59section BoundaryMap
61variable {R : Type u} [Ring R]
62variable {X : Type v} [Fintype X]
64/-- The finite Fox boundary map with prescribed generator boundary values.
66It sends a coordinate vector `v : X → R` to `∑ x, v x * generatorBoundary x`. -/
67def foxBoundaryMap (generatorBoundary : X → R) : (X → R) →ₗ[R] R where
68 toFun v := ∑ x : X, v x * generatorBoundary x
69 map_add' v w := by
70 simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
71 map_smul' r v := by
72 simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, RingHom.id_apply, Finset.mul_sum]
74/-- Evaluation formula for the finite Fox boundary map. -/
75theorem foxBoundaryMap_apply (generatorBoundary : X → R) (v : X → R) :
76 foxBoundaryMap generatorBoundary v =
77 ∑ x : X, v x * generatorBoundary x :=
78 rfl
80variable [DecidableEq X]
82/-- The finite Fox boundary map sends a coordinate basis vector to the corresponding
84@[simp]
85theorem foxBoundaryMap_single (generatorBoundary : X → R) (x : X) :
86 foxBoundaryMap generatorBoundary (Pi.single x (1 : R)) = generatorBoundary x := by
87 rw [foxBoundaryMap_apply]
88 rw [Finset.sum_eq_single x]
89 · simp only [Pi.single_eq_same, one_mul]
90 · intro y _ hy
91 simp only [Pi.single_eq_of_ne hy, zero_mul]
92 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_mul, IsEmpty.forall_iff]
94end BoundaryMap
96section FreeGroup
98variable {R : Type u} [Ring R]
99variable {X : Type v} [Fintype X] [DecidableEq X]
100variable (coeff : FreeGroup X →* R)
101variable (generatorBoundary : X → R)
103/-- Boundary-map form of the generic free-group Fox formula.
106Fox boundary of the free crossed differential with standard coordinate values recovers
107`boundary`. -/
109 (boundary : FreeGroup X → R)
110 (hboundary : IsCrossedDifferential coeff boundary)
111 (hgenerator :
112 ∀ x : X, boundary (FreeGroup.of x) = generatorBoundary x)
113 (w : FreeGroup X) :
114 foxBoundaryMap generatorBoundary
116 (A := X → R) coeff (fun x : X => Pi.single x (1 : R)) w) =
117 boundary w := by
118 let delta : FreeGroup X → R := fun w =>
119 foxBoundaryMap generatorBoundary
121 (A := X → R) coeff (fun x : X => Pi.single x (1 : R)) w)
122 have hdelta : IsCrossedDifferential coeff delta :=
123 IsCrossedDifferential.map_linear
125 (A := X → R) coeff (fun x : X => Pi.single x (1 : R)))
126 (foxBoundaryMap generatorBoundary)
127 have hdelta_generator :
128 ∀ x : X, delta (FreeGroup.of x) = generatorBoundary x := by
129 intro x
130 simp only [freeCrossedDifferentialWithCoeff_of, foxBoundaryMap_single, delta]
131 have hdelta_eq :
132 delta = freeCrossedDifferentialWithCoeff (A := R) coeff generatorBoundary :=
134 (A := R) coeff generatorBoundary delta hdelta hdelta_generator
135 have hboundary_eq :
136 boundary = freeCrossedDifferentialWithCoeff (A := R) coeff generatorBoundary :=
138 (A := R) coeff generatorBoundary boundary hboundary hgenerator
139 change delta w = boundary w
140 rw [hdelta_eq, hboundary_eq]
142/-- Conditional boundary-map form of the generic free-group Fox formula.
144Any crossed differential with standard coordinate values satisfies the same boundary formula as
145the canonical free crossed differential. -/
147 (delta : FreeGroup X → X → R)
148 (hdelta : IsCrossedDifferential coeff delta)
149 (hdelta_generator :
150 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : R))
151 (boundary : FreeGroup X → R)
152 (hboundary : IsCrossedDifferential coeff boundary)
153 (hboundary_generator :
154 ∀ x : X, boundary (FreeGroup.of x) = generatorBoundary x)
155 (w : FreeGroup X) :
156 foxBoundaryMap generatorBoundary (delta w) = boundary w := by
157 have hdelta_eq :
158 delta =
160 (A := X → R) coeff (fun x : X => Pi.single x (1 : R)) :=
162 (A := X → R) coeff (fun x : X => Pi.single x (1 : R))
163 delta hdelta hdelta_generator
164 rw [hdelta_eq]
166 coeff generatorBoundary boundary hboundary hboundary_generator w
168/-- Explicit finite-sum form of the generic Fox--Euler formula for any crossed differential with
169standard coordinate values:
170`coeff w - 1 = ∑ x, delta w x * (coeff x - 1)`. -/
172 (delta : FreeGroup X → X → R)
173 (hdelta : IsCrossedDifferential coeff delta)
174 (hdelta_generator :
175 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : R))
176 (w : FreeGroup X) :
177 coeff w - 1 =
178 ∑ x : X, delta w x * (coeff (FreeGroup.of x) - 1) := by
179 have hboundary :=
181 coeff
182 (fun x : X => coefficientFoxBoundary coeff (FreeGroup.of x))
183 delta hdelta hdelta_generator
184 (coefficientFoxBoundary coeff)
186 (by intro x; rfl)
187 w
188 simpa [coefficientFoxBoundary, foxBoundaryMap_apply] using hboundary.symm
190end FreeGroup
192end
194end FoxDifferential