FoxDifferential/Discrete/FoxCalculus/Universal.lean
1import FoxDifferential.Discrete.FoxCalculus.Derivative
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/FoxCalculus/Universal.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
27variable {H : Type v} [Group H]
28variable (X : Type u)
30variable [DecidableEq X]
31variable (ψ : FreeGroup X →* H)
33/-- The universal map `A_ψ → ℤ[H]^X` induced by the relative Fox derivative. -/
35 DifferentialModule ψ →ₗ[GroupRing H] RelativeFreeFoxCoordinates (H := H) X :=
36 lift
37 (A := RelativeFreeFoxCoordinates (H := H) X)
38 ψ
39 (relativeFreeGroupFoxDerivative (H := H) X ψ)
40 (relativeFreeGroupFoxDerivative_isDifferentialMap (H := H) X ψ)
42/-- The coordinate map out of the universal differential module sends `universalDifferential w` to the Fox derivative
43of `w`. -/
44@[simp]
45theorem relativeDifferentialToFreeFoxCoordinates_d (w : FreeGroup X) :
46 relativeDifferentialToFreeFoxCoordinates (H := H) X ψ (universalDifferential ψ w) =
47 relativeFreeGroupFoxDerivative (H := H) X ψ w := by
48 simpa [relativeDifferentialToFreeFoxCoordinates] using
50 (A := RelativeFreeFoxCoordinates (H := H) X)
51 ψ
52 (relativeFreeGroupFoxDerivative (H := H) X ψ)
53 (relativeFreeGroupFoxDerivative_isDifferentialMap (H := H) X ψ)
54 w
56variable [Fintype X]
58/-- The linear map from pushed-forward Fox-coordinate vectors to `A_ψ`, sending the coordinate
59basis vector at `x` to `universalDifferentialψ(x)`. -/
61 RelativeFreeFoxCoordinates (H := H) X →ₗ[GroupRing H] DifferentialModule ψ :=
62 { toFun := fun a =>
63 ∑ x : X, a x • universalDifferential ψ (FreeGroup.of x)
64 map_add' := by
65 intro a b
66 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Pi.add_apply, add_smul,
67 Finset.sum_add_distrib]
68 map_smul' := by
69 intro r a
70 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Pi.smul_apply, smul_eq_mul,
71 RingHom.id_apply, Finset.smul_sum, smul_smul]}
73/-- The coordinate-to-differential map sends a coordinate basis vector to the corresponding
75@[simp]
76theorem relativeFreeFoxCoordinatesLinearMap_single (x : X) :
77 relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
79 universalDifferential ψ (FreeGroup.of x) := by
80 change (∑ y : X,
81 ((Pi.single x (1 : GroupRing H) : RelativeFreeFoxCoordinates (H := H) X) y) •
82 universalDifferential ψ (FreeGroup.of y)) =
83 universalDifferential ψ (FreeGroup.of x)
84 rw [Finset.sum_eq_single x]
85 · simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Pi.single_eq_same, one_smul]
86 · intro y _ hy
87 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Pi.single_eq_of_ne hy, zero_smul]
88 · simp only [Finset.mem_univ, not_true_eq_false, relationSubmodule_eq_crossedDifferentialRelationSubmodule,
89 Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
91omit [DecidableEq X] [Fintype X] in
92/-- The universal relative differential on a free group satisfies the inverse rule. -/
93theorem relativeFreeGroupDifferential_inv (w : FreeGroup X) :
94 universalDifferential ψ w⁻¹ =
95 -((MonoidAlgebra.of ℤ H (ψ w⁻¹) : GroupRing H) • universalDifferential ψ w) := by
96 have h := universalDifferential_mul_inv_right ψ w⁻¹
97 rw [eq_neg_iff_add_eq_zero]
98 simpa using h
100/-- The relative Fox-coordinate formula recovers the universal differential in `A_ψ`. -/
101theorem relativeFreeFoxCoordinatesLinearMap_derivative (w : FreeGroup X) :
102 relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
103 (relativeFreeGroupFoxDerivative (H := H) X ψ w) =
104 universalDifferential ψ w := by
105 induction w using FreeGroup.induction_on with
106 | C1 =>
107 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, relativeFreeGroupFoxDerivative_one,
109 | of x =>
110 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, relativeFreeGroupFoxDerivative_of,
112 | inv_of x hx =>
113 rw [relativeFreeGroupFoxDerivative_inv, map_neg, map_smul, hx]
114 exact (relativeFreeGroupDifferential_inv (H := H) X ψ (FreeGroup.of x)).symm
115 | mul x y hx hy =>
116 rw [relativeFreeGroupFoxDerivative_mul, map_add, map_smul, hx, hy]
117 simpa using (universalDifferential_mul ψ x y).symm
119end FoxCalculus
121end
123end FoxDifferential