FoxDifferential/Completed/Residue/FreeGroup/Coordinates.lean
1import FoxDifferential.Completed.Residue.FreeGroup.Universal
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Residue/FreeGroup/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# Residue coefficient stages
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20open scoped BigOperators
22universe u v
25variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
27section FiniteBasis
29variable [Fintype X]
31/-- The linear map from the residue universal module to residue Fox-coordinate vectors. -/
32def residueDifferentialToFreeFoxCoordinates (n : ℕ) (ψ : FreeGroup X →* H) :
33 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
34 ResidueFreeFoxCoordinates n H X :=
37omit [Fintype X] in
38/-- The residue coordinate map sends a universal differential to the residue Fox derivative
39vector. -/
40@[simp]
42 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
44 (residueUniversalDifferential n ψ w) =
45 residueFreeGroupFoxDerivativeVector n ψ w := by
48/-- The linear map from residue Fox-coordinate vectors to the residue universal module, sending
49the coordinate basis at `x` to `d[ψ](x)`. -/
50def residueFreeFoxCoordinatesLinearMap (n : ℕ) (ψ : FreeGroup X →* H) :
51 ResidueFreeFoxCoordinates n H X →ₗ[ResidueGroupRing n H]
52 ResidueDifferentialModule n ψ where
53 toFun v := ∑ x : X, v x • residueUniversalDifferential n ψ (FreeGroup.of x)
54 map_add' := by
55 intro v w
56 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
57 map_smul' := by
58 intro r v
59 simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]
61/-- The coordinate-to-differential map sends a coordinate basis vector to the corresponding
62universal residue differential. -/
63@[simp]
65 (n : ℕ) (ψ : FreeGroup X →* H) (x : X) :
67 (Pi.single x (1 : ResidueGroupRing n H)) =
68 residueUniversalDifferential n ψ (FreeGroup.of x) := by
69 change (∑ y : X,
70 ((Pi.single x (1 : ResidueGroupRing n H) : ResidueFreeFoxCoordinates n H X) y) •
71 residueUniversalDifferential n ψ (FreeGroup.of y)) =
72 residueUniversalDifferential n ψ (FreeGroup.of x)
73 rw [Finset.sum_eq_single x]
74 · simp only [Pi.single_eq_same, one_smul]
75 · intro y _ hy
76 simp only [Pi.single_eq_of_ne hy, zero_smul]
77 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
79/-- The coordinate-to-differential map recovers the universal residue differential from the
80residue derivative vector. -/
82 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
84 (residueFreeGroupFoxDerivativeVector n ψ w) =
85 residueUniversalDifferential n ψ w := by
86 let beta : FreeGroup X → ResidueDifferentialModule n ψ :=
87 fun w => residueFreeFoxCoordinatesLinearMap n ψ
89 have hbeta :
90 IsCrossedDifferential (residueGroupRingScalar n ψ) beta :=
91 IsCrossedDifferential.map_linear
94 have hbasis :
95 ∀ x : X, beta (FreeGroup.of x) =
96 residueUniversalDifferential n ψ (FreeGroup.of x) := by
97 intro x
98 simp only [residueFreeGroupFoxDerivativeVector_of, residueFreeFoxCoordinatesLinearMap_single, beta]
99 have hbeta_eq :
100 beta =
102 (A := ResidueDifferentialModule n ψ)
103 (residueGroupRingScalar n ψ)
104 (fun x => residueUniversalDifferential n ψ (FreeGroup.of x)) := by
106 (A := ResidueDifferentialModule n ψ)
107 (residueGroupRingScalar n ψ)
108 (fun x => residueUniversalDifferential n ψ (FreeGroup.of x))
109 beta hbeta hbasis
110 have huniv_eq :
113 (A := ResidueDifferentialModule n ψ)
114 (residueGroupRingScalar n ψ)
115 (fun x => residueUniversalDifferential n ψ (FreeGroup.of x)) := by
117 (A := ResidueDifferentialModule n ψ)
118 (residueGroupRingScalar n ψ)
119 (fun x => residueUniversalDifferential n ψ (FreeGroup.of x))
122 (by intro x; rfl)
123 exact congrFun (hbeta_eq.trans huniv_eq.symm) w
125/-- The coordinate map is a left inverse to the coordinate-to-differential map. -/
127 (n : ℕ) (ψ : FreeGroup X →* H) :
128 (residueDifferentialToFreeFoxCoordinates n ψ).comp
130 LinearMap.id := by
131 apply LinearMap.ext
132 intro v
133 rw [LinearMap.comp_apply]
134 change residueDifferentialToFreeFoxCoordinates n ψ
135 (∑ y : X, v y • residueUniversalDifferential n ψ (FreeGroup.of y)) = v
136 rw [map_sum]
137 simp only [map_smul, residueDifferentialToFreeFoxCoordinates_universal]
138 funext x
139 change ((∑ y : X,
140 v y • residueFreeGroupFoxDerivativeVector n ψ (FreeGroup.of y)) :
141 ResidueFreeFoxCoordinates n H X) x = v x
142 rw [Finset.sum_apply]
143 rw [Finset.sum_eq_single x]
144 · simp only [residueFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one]
145 · intro y _ hy
146 have hxy : x ≠ y := fun h => hy h.symm
147 simp only [residueFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_of_ne hxy, smul_eq_mul,
148 mul_zero]
149 · simp only [Finset.mem_univ, not_true_eq_false, residueFreeGroupFoxDerivativeVector_of, Pi.smul_apply,
150 Pi.single_eq_same, smul_eq_mul, mul_one, IsEmpty.forall_iff]
152/-- The coordinate-to-differential map is a left inverse to the residue coordinate map. -/
154 (n : ℕ) (ψ : FreeGroup X →* H) :
155 (residueFreeFoxCoordinatesLinearMap n ψ).comp
157 LinearMap.id := by
158 apply residueDifferentialModuleHom_ext n ψ
159 intro w
160 simp only [LinearMap.comp_apply, residueDifferentialToFreeFoxCoordinates_universal,
161 residueFreeFoxCoordinatesLinearMap_derivativeVector, LinearMap.id_coe, id_eq]
163/-- The linear equivalence between residue Fox coordinates and the residue universal
166 (n : ℕ) (ψ : FreeGroup X →* H) :
167 ResidueFreeFoxCoordinates n H X ≃ₗ[ResidueGroupRing n H]
168 ResidueDifferentialModule n ψ := by
169 refine LinearEquiv.ofLinear
172 ?_ ?_
174 n ψ
176 n ψ
178end FiniteBasis
181end
183end FoxDifferential