FoxDifferential/Discrete/Naturality.lean
1import FoxDifferential.Discrete.FreeExpansion
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/Naturality.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
22universe u v w
24variable {H : Type v} {K : Type w} [Group H] [Group K]
25variable {X : Type u} [DecidableEq X]
26variable (ψ : FreeGroup X →* H) (φ : H →* K)
28/-- Push forward a relative Fox-coordinate vector along a homomorphism of coefficient groups. -/
30 RelativeFreeFoxCoordinates (H := H) X → RelativeFreeFoxCoordinates (H := K) X :=
31 fun a x => groupRingMap φ (a x)
33omit [DecidableEq X] in
34/-- Evaluation formula for pushing forward a relative Fox-coordinate vector. -/
35@[simp]
37 (a : RelativeFreeFoxCoordinates (H := H) X) (x : X) :
38 relativeFreeFoxCoordinatesMap (X := X) φ a x = groupRingMap φ (a x) :=
39 rfl
41/-- Relative Fox derivatives are natural under coefficient push-forward. -/
42theorem relativeFreeGroupFoxDerivative_mapDomain (w : FreeGroup X) :
43 relativeFreeGroupFoxDerivative (H := K) X (φ.comp ψ) w =
44 relativeFreeFoxCoordinatesMap (X := X) φ
45 (relativeFreeGroupFoxDerivative (H := H) X ψ w) := by
46 let delta : FreeGroup X → RelativeFreeFoxCoordinates (H := K) X :=
47 fun w => relativeFreeFoxCoordinatesMap (X := X) φ
48 (relativeFreeGroupFoxDerivative (H := H) X ψ w)
49 have hdelta :
51 (A := RelativeFreeFoxCoordinates (H := K) X) (φ.comp ψ) delta := by
52 intro u v
53 funext x
54 simp only [relativeFreeFoxCoordinatesMap_apply, relativeFreeGroupFoxDerivative_mul, MonoidAlgebra.of_apply,
55 Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_add, map_mul, groupRingMap_single, groupRingScalar,
56 MonoidHom.coe_comp, Function.comp_apply, relativeFreeFoxCoordinatesMap, delta]
57 have hbasis :
59 intro x
60 funext y
61 by_cases hxy : x = y
62 · subst y
63 simp only [relativeFreeFoxCoordinatesMap_apply, relativeFreeGroupFoxDerivative_of, Pi.single_eq_same, map_one,
64 delta]
65 · simp only [relativeFreeFoxCoordinatesMap_apply, relativeFreeGroupFoxDerivative_of, ne_eq, hxy,
67 exact (congrFun
68 (relativeFreeGroupFoxDerivative_unique (H := K) X (φ.comp ψ) delta hdelta hbasis) w).symm
70/-- Component form of coefficient-push-forward naturality. -/
71theorem relativeFreeGroupFoxDerivative_mapDomain_apply (w : FreeGroup X) (x : X) :
72 relativeFreeGroupFoxDerivative (H := K) X (φ.comp ψ) w x =
73 groupRingMap φ (relativeFreeGroupFoxDerivative (H := H) X ψ w x) := by
74 have h := congrFun
75 (relativeFreeGroupFoxDerivative_mapDomain (H := H) (K := K) ψ φ w) x
76 simpa [relativeFreeFoxCoordinatesMap] using h
78end FoxCalculus
80end
82end FoxDifferential