FoxDifferential/Discrete/FoxCalculus/Coordinates.lean
1import FoxDifferential.Discrete.FoxCalculus.Boundary
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/FoxCalculus/Coordinates.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)
33variable [Fintype X]
35/-- The coordinate map is a left inverse to the coordinate-to-differential map. -/
37 (relativeDifferentialToFreeFoxCoordinates (H := H) X ψ).comp
38 (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ) =
39 LinearMap.id := by
40 apply LinearMap.ext
41 intro a
42 rw [LinearMap.comp_apply]
43 change relativeDifferentialToFreeFoxCoordinates (H := H) X ψ
44 (∑ y : X, a y • universalDifferential ψ (FreeGroup.of y)) = a
45 rw [map_sum]
46 simp only [map_smul, relativeDifferentialToFreeFoxCoordinates_d]
47 funext x
48 change ((∑ y : X,
49 a y • relativeFreeGroupFoxDerivative (H := H) X ψ (FreeGroup.of y)) :
50 RelativeFreeFoxCoordinates (H := H) X) x = a x
51 rw [Finset.sum_apply]
52 rw [Finset.sum_eq_single x]
53 · simp only [relativeFreeGroupFoxDerivative_of, Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one]
54 · intro y _ hy
55 have hxy : x ≠ y := fun h => hy h.symm
56 simp only [relativeFreeGroupFoxDerivative_of, Pi.smul_apply, Pi.single_eq_of_ne hxy, smul_eq_mul, mul_zero]
57 · simp only [Finset.mem_univ, not_true_eq_false, relativeFreeGroupFoxDerivative_of, Pi.smul_apply,
58 Pi.single_eq_same, smul_eq_mul, mul_one, IsEmpty.forall_iff]
60/-- The coordinate-to-differential map is a left inverse to the differential-to-coordinate map. -/
62 (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ).comp
63 (relativeDifferentialToFreeFoxCoordinates (H := H) X ψ) =
64 LinearMap.id := by
65 apply hom_ext ψ
66 intro w
67 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, LinearMap.coe_comp, Function.comp_apply,
68 relativeDifferentialToFreeFoxCoordinates_d, relativeFreeFoxCoordinatesLinearMap_derivative, LinearMap.id_coe, id_eq]
70/-- The linear equivalence between pushed-forward Fox coordinates and the universal differential
73 RelativeFreeFoxCoordinates (H := H) X ≃ₗ[GroupRing H] DifferentialModule ψ := by
74 refine LinearEquiv.ofLinear
75 (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ)
76 (relativeDifferentialToFreeFoxCoordinates (H := H) X ψ)
77 ?_ ?_
79 (H := H) X ψ
81 (H := H) X ψ
83end FoxCalculus
85end
87end FoxDifferential