FoxDifferential/Completed/Continuous/Automorphism.lean
1import FoxDifferential.Completed.Continuous.ChainRule.Iterated
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Continuous/Automorphism.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Continuous crossed differentials
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
24section AllFiniteAutomorphismJacobian
26variable {X F H : Type u}
27variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
28variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
29variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
32/-- The named inverse linear map for the completed Fox-Jacobian of a continuous automorphism. -/
34 {ι : X → F}
36 (ProC := ProCGroups.ProC.allFiniteProC) ι)
37 (e : F ≃* F) (φ : X → H) :
38 ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H]
39 ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) :=
41 (X := X) (Y := X) (F := F) (F' := F) hι e.symm.toMonoidHom
43 (X := X) (F := F) hι e.toMonoidHom φ ι)
44 ι
46/-- The named inverse matrix for the completed Fox-Jacobian of a continuous automorphism. -/
48 {ι : X → F}
50 (ProC := ProCGroups.ProC.allFiniteProC) ι)
51 (e : F ≃* F) (φ : X → H) :
52 Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :=
54 (X := X) (Y := X) (F := F) (F' := F) hι e.symm.toMonoidHom
56 (X := X) (F := F) hι e.toMonoidHom φ ι)
57 ι
59/-- A finite-stage projection of the named inverse matrix for a completed Fox-Jacobian of a
60continuous automorphism. -/
62 {ι : X → F}
64 (ProC := ProCGroups.ProC.allFiniteProC) ι)
65 (e : F ≃* F) (φ : X → H)
66 (j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :
67 Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j) :=
68 fun x y =>
69 zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
71 (X := X) (F := F) (H := H) hι e φ x y)
73omit [Fintype X] in
74/-- Evaluation of the finite-stage inverse matrix for a completed Fox-Jacobian of a continuous
75automorphism. -/
76@[simp]
78 {ι : X → F}
80 (ProC := ProCGroups.ProC.allFiniteProC) ι)
81 (e : F ≃* F) (φ : X → H)
82 (j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) (x y : X) :
84 (X := X) (F := F) (H := H) hι e φ j x y =
85 zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
87 (X := X) (F := F) (H := H) hι e φ x y) :=
88 rfl
90/-- The named inverse linear map is row-vector multiplication by the named inverse matrix. -/
92 {ι : X → F}
94 (ProC := ProCGroups.ProC.allFiniteProC) ι)
95 (e : F ≃* F) (φ : X → H)
96 (v : ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H)) :
98 (X := X) (F := F) (H := H) hι e φ v =
99 Matrix.vecMul v
101 (X := X) (F := F) (H := H) hι e φ) := by
103 (X := X) (F := F) hι e.symm.toMonoidHom
105 (X := X) (F := F) hι e.toMonoidHom φ ι)
106 ι v
108omit [Fintype X] in
109/-- Pulling the target generator map first along an automorphism and then along its inverse
112 {ι : X → F}
114 (ProC := ProCGroups.ProC.allFiniteProC) ι)
115 (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
117 (X := X) (F := F) hι e.symm.toMonoidHom
119 (X := X) (F := F) hι e.toMonoidHom φ ι)
120 ι =
121 φ := by
122 let htarget : ProCGroups.ProC.allFiniteProC
123 (G := ZCCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H) :=
124 allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H
125 let hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProCGroups.ProC.allFiniteProC) φ) :=
126 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H φ
127 let φe : X → H :=
129 (X := X) (F := F) hι e.toMonoidHom φ ι
130 let hφe : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProCGroups.ProC.allFiniteProC) φe) :=
131 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H φe
133 (X := X) (Y := X) (F := F) (F' := F) (H := H)
134 hι hι e.toMonoidHom he_continuous φ
135 funext x
137 (ProC := ProCGroups.ProC.allFiniteProC) hι htarget φe hφe
138 (e.symm (ι x)) = φ x
139 have happ := congrFun (congrArg DFunLike.coe hρ) (e.symm (ι x))
140 calc
142 (ProC := ProCGroups.ProC.allFiniteProC) hι htarget φe hφe
143 (e.symm (ι x)) =
145 (ProC := ProCGroups.ProC.allFiniteProC) hι htarget φ hφ).comp
146 e.toMonoidHom) (e.symm (ι x)) := by
147 simpa [φe, htarget, hφ, hφe] using happ
149 (ProC := ProCGroups.ProC.allFiniteProC) hι htarget φ hφ (ι x) := by
150 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
151 MulEquiv.apply_symm_apply, freeProCZCCompletedFoxRightHom_apply, freeProCZCCompletedFoxSemidirectLift_generator,
153 _ = φ x := by
154 simp only [freeProCZCCompletedFoxRightHom_apply, freeProCZCCompletedFoxSemidirectLift_generator,
157/-- The completed Fox-Jacobian linear map of a continuous automorphism composed with its named
158inverse is the identity. -/
160 {ι : X → F}
162 (ProC := ProCGroups.ProC.allFiniteProC) ι)
163 (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
165 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι).comp
167 (X := X) (F := F) (H := H) hι e φ) =
168 LinearMap.id := by
169 apply linearMap_ext_pi_single
170 intro x
171 have hchain := allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp
172 (X := X) (Y := X) (F := F) (F' := F) (H := H)
173 hι hι e.toMonoidHom he_continuous φ (e.symm (ι x))
174 simpa [LinearMap.comp_apply,
177 allFiniteProC_freeProCZCCompletedFoxJacobian] using hchain.symm
179/-- The named inverse for the completed Fox-Jacobian linear map of a continuous automorphism
180composed with the Jacobian is the identity. -/
182 {ι : X → F}
184 (ProC := ProCGroups.ProC.allFiniteProC) ι)
185 (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
186 (φ : X → H) :
188 (X := X) (F := F) (H := H) hι e φ).comp
190 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι) =
191 LinearMap.id := by
192 apply linearMap_ext_pi_single
193 intro x
194 let φe : X → H :=
196 (X := X) (F := F) hι e.toMonoidHom φ ι
197 have hpull :
199 (X := X) (F := F) hι e.symm.toMonoidHom φe ι =
200 φ := by
201 simpa [φe] using
203 (X := X) (F := F) (H := H) hι e he_continuous φ
204 have hchain := allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp
205 (X := X) (Y := X) (F := F) (F' := F) (H := H)
206 hι hι e.symm.toMonoidHom he_symm_continuous φe (e (ι x))
207 rw [hpull] at hchain
208 simpa [LinearMap.comp_apply,
211 allFiniteProC_freeProCZCCompletedFoxJacobian, φe] using hchain.symm
213/-- The named inverse matrix is a left inverse for the completed Fox-Jacobian matrix of a
214continuous automorphism. -/
216 {ι : X → F}
218 (ProC := ProCGroups.ProC.allFiniteProC) ι)
219 (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
221 (X := X) (F := F) (H := H) hι e φ *
223 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι =
224 (1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H)) := by
225 rw [Matrix.ext_iff_vecMul]
226 intro v
227 have hlin :=
229 (X := X) (F := F) (H := H) hι e he_continuous φ
230 have happ := congrFun (congrArg DFunLike.coe hlin) v
231 simpa [LinearMap.comp_apply,
234 Matrix.vecMul_vecMul, Matrix.vecMul_one] using happ
236/-- The named inverse matrix is a right inverse for the completed Fox-Jacobian matrix of a
237continuous automorphism. -/
239 {ι : X → F}
241 (ProC := ProCGroups.ProC.allFiniteProC) ι)
242 (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
243 (φ : X → H) :
245 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι *
247 (X := X) (F := F) (H := H) hι e φ =
248 (1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H)) := by
249 rw [Matrix.ext_iff_vecMul]
250 intro v
251 have hlin :=
253 (X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φ
254 have happ := congrFun (congrArg DFunLike.coe hlin) v
255 simpa [LinearMap.comp_apply,
258 Matrix.vecMul_vecMul, Matrix.vecMul_one] using happ
260/-- The finite-stage inverse matrix is a left inverse for the finite-stage completed Fox-Jacobian
261matrix of a continuous automorphism. -/
263 {ι : X → F}
265 (ProC := ProCGroups.ProC.allFiniteProC) ι)
266 (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H)
267 (j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :
269 (X := X) (F := F) (H := H) hι e φ j *
271 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι j =
272 (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j)) := by
273 apply Matrix.ext
274 intro x y
275 have h := congrArg
276 (fun M : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) =>
277 zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j (M x y))
279 (X := X) (F := F) (H := H) hι e he_continuous φ)
280 have hone :
281 zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
282 ((1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H)) x y) =
283 (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j)) x y := by
284 by_cases hxy : x = y
285 · subst y
286 simp only [zcCompletedGroupAlgebraProjection, Matrix.one_apply_eq, zcCompletedGroupAlgebraProjection_one]
287 · simp only [zcCompletedGroupAlgebraProjection, ne_eq, hxy, not_false_eq_true, Matrix.one_apply_ne,
289 simp only [Matrix.mul_apply] at h
290 rw [zcCompletedGroupAlgebraProjection_sum] at h
291 rw [hone] at h
292 simp only [zcCompletedGroupAlgebraProjection, MulEquiv.toMonoidHom_eq_coe,
293 allFiniteProC_freeProCZCCompletedFoxJacobianMatrix_apply, zcCompletedGroupAlgebraProjection_mul] at h
294 simpa [Matrix.mul_apply,
298/-- The finite-stage inverse matrix is a right inverse for the finite-stage completed Fox-Jacobian
299matrix of a continuous automorphism. -/
301 {ι : X → F}
303 (ProC := ProCGroups.ProC.allFiniteProC) ι)
304 (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
305 (φ : X → H) (j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :
307 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι j *
309 (X := X) (F := F) (H := H) hι e φ j =
310 (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j)) := by
311 apply Matrix.ext
312 intro x y
313 have h := congrArg
314 (fun M : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) =>
315 zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j (M x y))
317 (X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φ)
318 have hone :
319 zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
320 ((1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H)) x y) =
321 (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j)) x y := by
322 by_cases hxy : x = y
323 · subst y
324 simp only [zcCompletedGroupAlgebraProjection, Matrix.one_apply_eq, zcCompletedGroupAlgebraProjection_one]
325 · simp only [zcCompletedGroupAlgebraProjection, ne_eq, hxy, not_false_eq_true, Matrix.one_apply_ne,
327 simp only [Matrix.mul_apply] at h
328 rw [zcCompletedGroupAlgebraProjection_sum] at h
329 rw [hone] at h
330 simp only [zcCompletedGroupAlgebraProjection, MulEquiv.toMonoidHom_eq_coe,
331 allFiniteProC_freeProCZCCompletedFoxJacobianMatrix_apply, zcCompletedGroupAlgebraProjection_mul] at h
332 simpa [Matrix.mul_apply,
336/-- The completed Fox-Jacobian of a continuous automorphism as a linear equivalence. -/
338 {ι : X → F}
340 (ProC := ProCGroups.ProC.allFiniteProC) ι)
341 (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
342 (φ : X → H) :
343 ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) ≃ₗ[ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H]
344 ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) := by
345 refine LinearEquiv.ofLinear
347 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι)
349 (X := X) (F := F) (H := H) hι e φ)
350 ?_ ?_
352 (X := X) (F := F) (H := H) hι e he_continuous φ
354 (X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φ
356end AllFiniteAutomorphismJacobian
358end
360end FoxDifferential