FoxDifferential/Discrete/FoxCalculus/Boundary.lean
1import FoxDifferential.Common.FoxBoundary
2import FoxDifferential.Discrete.DifferentialModule.Boundary
3import FoxDifferential.Discrete.FoxCalculus.Universal
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Discrete/FoxCalculus/Boundary.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 group-ring Fox calculus
16Ordinary Fox derivatives over group rings are developed through augmentation, relative differential modules, coordinates, Jacobians, and chain rules.
17-/
18namespace FoxDifferential
20noncomputable section
22namespace FoxCalculus
24open scoped BigOperators
26universe u v
29variable {H : Type v} [Group H]
30variable (X : Type u)
32variable [DecidableEq X]
33variable (ψ : FreeGroup X →* H)
35variable [Fintype X]
37/-- The pushed-forward Fox boundary
38`a ↦ ∑ x, a_x (ψ x - 1)`. -/
40 RelativeFreeFoxCoordinates (H := H) X →ₗ[GroupRing H] GroupRing H :=
41 { toFun := fun a =>
42 ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x))
43 map_add' := by
44 intro a b
45 simp only [Pi.add_apply, augmentationGenerator_eq_groupRingBoundary, add_mul, Finset.sum_add_distrib]
46 map_smul' := by
47 intro r a
48 simp only [Pi.smul_apply, smul_eq_mul, augmentationGenerator_eq_groupRingBoundary, mul_assoc,
49 RingHom.id_apply, Finset.mul_sum]}
51omit [DecidableEq X] in
52/-- Evaluation formula for the relative Fox boundary map. -/
54 (a : RelativeFreeFoxCoordinates (H := H) X) :
55 relativeFreeGroupFoxBoundary (H := H) X ψ a =
56 ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x)) :=
57 rfl
59/-- The relative Fox boundary sends a coordinate basis vector to the corresponding
60augmentation generator. -/
61@[simp]
62theorem relativeFreeGroupFoxBoundary_single (x : X) :
63 relativeFreeGroupFoxBoundary (H := H) X ψ
65 augmentationGenerator H (ψ (FreeGroup.of x)) := by
67 rw [Finset.sum_eq_single x]
68 · simp only [Pi.single_eq_same, augmentationGenerator_eq_groupRingBoundary, one_mul]
69 · intro y _ hy
70 simp only [Pi.single_eq_of_ne hy, augmentationGenerator_eq_groupRingBoundary, zero_mul]
71 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, augmentationGenerator_eq_groupRingBoundary,
72 one_mul, IsEmpty.forall_iff]
74omit [DecidableEq X] in
75/-- The universal boundary composed with the coordinate-to-differential map is the pushed-forward
76Fox boundary. -/
78 (toGroupRing ψ).comp
79 (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ) =
80 relativeFreeGroupFoxBoundary (H := H) X ψ := by
81 apply LinearMap.ext
82 intro a
83 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, relativeFreeFoxCoordinatesLinearMap,
84 LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, map_sum, map_smul, toGroupRing_d,
85 groupRingBoundary, MonoidAlgebra.of_apply, smul_eq_mul, relativeFreeGroupFoxBoundary, augmentationGenerator]
87/-- Relative Fox fundamental formula, also known as the Fox--Euler formula:
88`ψ(w) - 1 = ∑ x, (∂w/∂x) (ψ x - 1)`. -/
89theorem relativeFreeGroupFoxDerivative_fundamental_formula (w : FreeGroup X) :
90 groupRingBoundary ψ w =
91 ∑ x : X,
92 relativeFreeGroupFoxDerivative (H := H) X ψ w x *
93 augmentationGenerator H (ψ (FreeGroup.of x)) := by
94 have h :=
95 LinearMap.congr_fun
96 (toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap (H := H) X ψ)
97 (relativeFreeGroupFoxDerivative (H := H) X ψ w)
98 rw [LinearMap.comp_apply, relativeFreeFoxCoordinatesLinearMap_derivative,
99 toGroupRing_d] at h
100 simpa [relativeFreeGroupFoxBoundary] using h
102/-- Fox boundary form of the relative Fox fundamental formula. -/
103theorem relativeFreeGroupFoxBoundary_derivative (w : FreeGroup X) :
104 relativeFreeGroupFoxBoundary (H := H) X ψ
105 (relativeFreeGroupFoxDerivative (H := H) X ψ w) =
106 groupRingBoundary ψ w := by
107 simpa [relativeFreeGroupFoxBoundary_apply] using
108 (relativeFreeGroupFoxDerivative_fundamental_formula (H := H) X ψ w).symm
110/-- Conditional relative Fox boundary formula. Any differential map on a free group with the
111standard coordinate values satisfies the relative Fox boundary formula. -/
113 (delta : FreeGroup X → RelativeFreeFoxCoordinates (H := H) X)
114 (hdelta : IsDifferentialMap (A := RelativeFreeFoxCoordinates (H := H) X) ψ delta)
115 (hbasis :
116 ∀ x : X, delta (FreeGroup.of x) =
118 (w : FreeGroup X) :
119 relativeFreeGroupFoxBoundary (H := H) X ψ (delta w) =
120 groupRingBoundary ψ w := by
121 have hdelta_eq :
122 delta = relativeFreeGroupFoxDerivative (H := H) X ψ :=
123 relativeFreeGroupFoxDerivative_unique (H := H) X ψ delta hdelta hbasis
124 rw [hdelta_eq]
125 exact relativeFreeGroupFoxBoundary_derivative (H := H) X ψ w
127/-- Conditional relative Fox fundamental formula. The Fox-Euler sum computed from any
128differential map with standard coordinate values is `[ψ(w)] - 1`. -/
130 (delta : FreeGroup X → RelativeFreeFoxCoordinates (H := H) X)
131 (hdelta : IsDifferentialMap (A := RelativeFreeFoxCoordinates (H := H) X) ψ delta)
132 (hbasis :
133 ∀ x : X, delta (FreeGroup.of x) =
135 (w : FreeGroup X) :
136 groupRingBoundary ψ w =
137 ∑ x : X,
138 delta w x * augmentationGenerator H (ψ (FreeGroup.of x)) := by
139 simpa [relativeFreeGroupFoxBoundary_apply] using
141 (H := H) X ψ delta hdelta hbasis w).symm
143/-- Explicit `ψ(w) - 1` version of the conditional relative Fox-Euler formula. -/
145 (delta : FreeGroup X → RelativeFreeFoxCoordinates (H := H) X)
146 (hdelta : IsDifferentialMap (A := RelativeFreeFoxCoordinates (H := H) X) ψ delta)
147 (hbasis :
148 ∀ x : X, delta (FreeGroup.of x) =
150 (w : FreeGroup X) :
152 ∑ x : X,
153 delta w x * augmentationGenerator H (ψ (FreeGroup.of x)) := by
154 simpa [groupRingBoundary] using
156 (H := H) X ψ delta hdelta hbasis w
158/-- Explicit `ψ(w) - 1` version of the relative Fox--Euler formula. -/
159theorem relativeFreeGroupFoxDerivative_euler_formula (w : FreeGroup X) :
161 ∑ x : X,
162 relativeFreeGroupFoxDerivative (H := H) X ψ w x *
163 augmentationGenerator H (ψ (FreeGroup.of x)) := by
164 simpa [groupRingBoundary] using
165 relativeFreeGroupFoxDerivative_fundamental_formula (H := H) X ψ w
167end FoxCalculus
169end
171end FoxDifferential