FoxDifferential/Completed/ProCIntegerCoefficients/FreeGroup/Coordinates.lean
1import FoxDifferential.Common.FoxBoundary
2import FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Derivative
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients/FreeGroup/Coordinates.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Completed group algebra coefficients
15This module gives the free-group formulas for pro-\(C\) integer coefficients, used to compare completed Fox derivatives with ordinary finite-stage derivatives.
16-/
17namespace FoxDifferential
19noncomputable section
21open scoped BigOperators
23universe u v
26variable (C : ProCGroups.FiniteGroupClass.{v})
27variable {X : Type u} [DecidableEq X]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30section FiniteBasis
32variable [Fintype X]
34/-- The completed Fox boundary/Euler map
35`v ↦ ∑ i, v_i * ([ψ x_i] - 1)`. -/
36def zcFreeGroupFoxBoundary (ψ : FreeGroup X →* H) :
37 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
38 ZCCompletedGroupAlgebra C H where
39 toFun v := ∑ i : X, v i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)
40 map_add' := by
41 intro v w
42 simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
43 map_smul' := by
44 intro r v
45 simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, RingHom.id_apply, Finset.mul_sum]
47omit [DecidableEq X] in
48/-- Evaluation formula for the completed Fox boundary/Euler map. -/
49theorem zcFreeGroupFoxBoundary_apply
50 (ψ : FreeGroup X →* H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
51 zcFreeGroupFoxBoundary C ψ v =
52 ∑ i : X, v i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) :=
53 rfl
55omit [DecidableEq X] in
56/-- The completed Fox boundary is the generic finite Fox boundary map specialized to
57`x ↦ [ψ x] - 1`. -/
59 (ψ : FreeGroup X →* H) :
60 zcFreeGroupFoxBoundary C ψ =
62 (fun i : X =>
63 coefficientFoxBoundary (zcCompletedGroupAlgebraScalar C ψ) (FreeGroup.of i)) := by
64 ext v
65 rfl
67/-- The completed Fox boundary sends a coordinate basis vector to the corresponding completed
68augmentation generator. -/
69@[simp]
70theorem zcFreeGroupFoxBoundary_single (ψ : FreeGroup X →* H) (i : X) :
72 (Pi.single i (1 : ZCCompletedGroupAlgebra C H)) =
73 zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of i) := by
75 rw [Finset.sum_eq_single i]
76 · simp only [Pi.single_eq_same, one_mul, zcCompletedGroupAlgebraBoundary]
77 · intro j _ hji
78 simp only [Pi.single_eq_of_ne hji, zero_mul]
79 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_mul, IsEmpty.forall_iff]
81/-- The linear map from the completed universal module to completed Fox-coordinate vectors. -/
82def zcDifferentialToFreeFoxCoordinates (ψ : FreeGroup X →* H) :
83 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
84 ZCFreeFoxCoordinates C (X := X) (H := H) :=
87omit [Fintype X] in
88/-- The completed coordinate map sends a universal differential to the completed Fox derivative
89vector. -/
90@[simp]
92 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
94 (zcUniversalDifferential C ψ w) =
95 zcFreeGroupFoxDerivativeVector C ψ w := by
96 exact zcFreeGroupFoxDerivativeVectorLinearMap_universal C ψ w
98/-- The linear map from completed Fox-coordinate vectors to the completed universal module,
99sending the coordinate basis at `x` to `d[ψ](x)`. -/
100def zcFreeFoxCoordinatesLinearMap (ψ : FreeGroup X →* H) :
101 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
102 ZCCompletedDifferentialModule C ψ where
103 toFun v := ∑ x : X, v x • zcUniversalDifferential C ψ (FreeGroup.of x)
104 map_add' := by
105 intro v w
106 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
107 map_smul' := by
108 intro r v
109 simp only [Pi.smul_apply, RingHom.id_apply, smul_eq_mul, Finset.smul_sum, smul_smul]
111/-- The coordinate-to-differential map sends a coordinate basis vector to the corresponding
112universal completed differential. -/
113@[simp]
114theorem zcFreeFoxCoordinatesLinearMap_single (ψ : FreeGroup X →* H) (x : X) :
116 (Pi.single x (1 : ZCCompletedGroupAlgebra C H)) =
117 zcUniversalDifferential C ψ (FreeGroup.of x) := by
118 change (∑ y : X,
119 ((Pi.single x (1 : ZCCompletedGroupAlgebra C H) :
120 ZCFreeFoxCoordinates C (X := X) (H := H)) y) •
121 zcUniversalDifferential C ψ (FreeGroup.of y)) =
122 zcUniversalDifferential C ψ (FreeGroup.of x)
123 rw [Finset.sum_eq_single x]
124 · simp only [Pi.single_eq_same, one_smul]
125 · intro y _ hy
126 simp only [Pi.single_eq_of_ne hy, zero_smul]
127 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
129/-- The coordinate-to-differential map recovers the universal completed differential from the
130completed derivative vector. -/
132 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
134 (zcFreeGroupFoxDerivativeVector C ψ w) =
135 zcUniversalDifferential C ψ w := by
136 let beta : FreeGroup X → ZCCompletedDifferentialModule C ψ :=
137 fun w => zcFreeFoxCoordinatesLinearMap C ψ (zcFreeGroupFoxDerivativeVector C ψ w)
138 have hbeta :
139 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) beta :=
140 IsCrossedDifferential.map_linear
143 have hbasis :
144 ∀ x : X, beta (FreeGroup.of x) =
145 zcUniversalDifferential C ψ (FreeGroup.of x) := by
146 intro x
147 simp only [zcFreeGroupFoxDerivativeVector_of, zcFreeFoxCoordinatesLinearMap_single, beta]
148 have hbeta_eq :
149 beta =
151 (A := ZCCompletedDifferentialModule C ψ)
153 (fun x => zcUniversalDifferential C ψ (FreeGroup.of x)) := by
155 (A := ZCCompletedDifferentialModule C ψ)
157 (fun x => zcUniversalDifferential C ψ (FreeGroup.of x))
158 beta hbeta hbasis
159 have huniv_eq :
160 zcUniversalDifferential C ψ =
162 (A := ZCCompletedDifferentialModule C ψ)
164 (fun x => zcUniversalDifferential C ψ (FreeGroup.of x)) := by
166 (A := ZCCompletedDifferentialModule C ψ)
168 (fun x => zcUniversalDifferential C ψ (FreeGroup.of x))
169 (zcUniversalDifferential C ψ)
171 (by intro x; rfl)
172 exact congrFun (hbeta_eq.trans huniv_eq.symm) w
174/-- The coordinate map is a left inverse to the coordinate-to-differential map. -/
176 (ψ : FreeGroup X →* H) :
177 (zcDifferentialToFreeFoxCoordinates C ψ).comp
178 (zcFreeFoxCoordinatesLinearMap C ψ) =
179 LinearMap.id := by
180 apply LinearMap.ext
181 intro v
182 rw [LinearMap.comp_apply]
183 change zcDifferentialToFreeFoxCoordinates C ψ
184 (∑ y : X, v y • zcUniversalDifferential C ψ (FreeGroup.of y)) = v
185 rw [map_sum]
186 simp only [map_smul, zcDifferentialToFreeFoxCoordinates_universal]
187 funext x
188 change ((∑ y : X,
189 v y • zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of y)) :
190 ZCFreeFoxCoordinates C (X := X) (H := H)) x = v x
191 rw [Finset.sum_apply]
192 rw [Finset.sum_eq_single x]
193 · simp only [zcFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one]
194 · intro y _ hy
195 have hxy : x ≠ y := fun h => hy h.symm
196 simp only [zcFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_of_ne hxy, smul_eq_mul, mul_zero]
197 · simp only [Finset.mem_univ, not_true_eq_false, zcFreeGroupFoxDerivativeVector_of, Pi.smul_apply,
198 Pi.single_eq_same, smul_eq_mul, mul_one, IsEmpty.forall_iff]
200/-- The coordinate-to-differential map is a left inverse to the completed coordinate map. -/
202 (ψ : FreeGroup X →* H) :
203 (zcFreeFoxCoordinatesLinearMap C ψ).comp
205 LinearMap.id := by
206 apply zcCompletedDifferentialModuleHom_ext C ψ
207 intro w
208 simp only [LinearMap.comp_apply, zcDifferentialToFreeFoxCoordinates_universal,
209 zcFreeFoxCoordinatesLinearMap_derivativeVector, LinearMap.id_coe, id_eq]
211/-- The linear equivalence between completed Fox coordinates and the completed universal
214 (ψ : FreeGroup X →* H) :
215 ZCFreeFoxCoordinates C (X := X) (H := H) ≃ₗ[ZCCompletedGroupAlgebra C H]
216 ZCCompletedDifferentialModule C ψ := by
217 refine LinearEquiv.ofLinear
220 ?_ ?_
225end FiniteBasis
228end
230end FoxDifferential