FoxDifferential/Discrete/FreeExpansion.lean
1import FoxDifferential.Discrete.FoxCalculus.Universal
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/FreeExpansion.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete group-ring Fox calculus
14Ordinary Fox derivatives over group rings are developed through augmentation, relative differential modules, coordinates, Jacobians, and chain rules.
15-/
16namespace FoxDifferential
18noncomputable section
20namespace FoxCalculus
22open scoped BigOperators
24universe u v w
26variable {H : Type v} [Group H]
28variable {X : Type u} [DecidableEq X] [Fintype X]
29variable (ψ : FreeGroup X →* H) (basisValue : X → A)
31/-- The Fox-coordinate expansion determined by prescribed values on the free generators. -/
32def freeCrossedDifferentialExpansion (w : FreeGroup X) : A :=
33 ∑ x : X,
34 relativeFreeGroupFoxDerivative (H := H) X ψ w x • basisValue x
36/-- The Fox-coordinate expansion of the identity word is zero. -/
37@[simp]
38theorem freeCrossedDifferentialExpansion_one :
39 freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue 1 = 0 := by
40 simp only [freeCrossedDifferentialExpansion, relativeFreeGroupFoxDerivative_one, Pi.zero_apply, zero_smul,
41 Finset.sum_const_zero]
43/-- The Fox-coordinate expansion of a free generator returns its prescribed basis value. -/
44@[simp]
45theorem freeCrossedDifferentialExpansion_of (x : X) :
46 freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue (FreeGroup.of x) =
47 basisValue x := by
50 rw [Finset.sum_eq_single x]
51 · simp only [Pi.single_eq_same, one_smul]
52 · intro y _ hy
53 simp only [Pi.single_eq_of_ne hy, zero_smul]
54 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
56/-- The Fox-coordinate expansion is a crossed differential. -/
58 IsDifferentialMap (A := A) ψ
59 (freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue) := by
60 intro u v
62 change
63 (∑ x : X,
64 relativeFreeGroupFoxDerivative (H := H) X ψ (u * v) x • basisValue x) =
65 (∑ x : X,
66 relativeFreeGroupFoxDerivative (H := H) X ψ u x • basisValue x) +
68 (∑ x : X,
69 relativeFreeGroupFoxDerivative (H := H) X ψ v x • basisValue x)
71 simp only [MonoidAlgebra.of_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul, add_smul, Finset.sum_add_distrib,
72 Finset.smul_sum, smul_smul]
74/-- The coefficient-generic free crossed differential over a group ring is the Fox-coordinate
76theorem freeCrossedDifferentialWithCoeff_groupRingScalar_eq_expansion (w : FreeGroup X) :
77 freeCrossedDifferentialWithCoeff (A := A) (groupRingScalar ψ) basisValue w =
78 freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue w := by
79 have h :=
80 freeCrossedDifferentialWithCoeff_unique (A := A) (groupRingScalar ψ) basisValue
81 (freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue)
82 (freeCrossedDifferentialExpansion_isDifferentialMap (H := H) (A := A) ψ basisValue)
83 (freeCrossedDifferentialExpansion_of (H := H) (A := A) ψ basisValue)
84 exact congrFun h.symm w
86omit [Fintype X] in
87/-- The coefficient-generic coordinate crossed differential specializes to the usual relative
88Fox derivative over a group ring. -/
90 (w : FreeGroup X) :
92 (X := X) (groupRingScalar ψ) w =
93 relativeFreeGroupFoxDerivative (H := H) X ψ w := by
94 exact congrFun (relativeFreeGroupFoxDerivative_unique (H := H) X ψ
95 (freeCrossedDifferentialWithCoeffCoordinates (X := X) (groupRingScalar ψ))
97 (X := X) (groupRingScalar ψ))
99 (X := X) (groupRingScalar ψ))) w
101variable {Y : Type w}
103/-- Abstract Fox chain rule for an arbitrary crossed differential. -/
105 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
106 (delta : FreeGroup Y → A) (hdelta : IsDifferentialMap (A := A) ψ delta)
107 (w : FreeGroup X) :
108 delta (φ w) =
109 ∑ x : X,
110 relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x •
111 delta (φ (FreeGroup.of x)) := by
112 calc
113 delta (φ w) =
115 (X := X) (groupRingScalar (ψ.comp φ))
116 (fun x : X => delta (φ (FreeGroup.of x))) w := by
118 (X := X) (Y := Y) (B := A)
119 (groupRingScalar ψ) φ delta hdelta w
120 _ =
121 ∑ x : X,
122 relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x •
123 delta (φ (FreeGroup.of x)) := by
127 (H := H) (X := X) (ψ.comp φ) w]
129end FoxCalculus
131end
133end FoxDifferential