Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Continuous.Automorphism
ProCGroups/FoxDifferential/Completed/Continuous/Automorphism/Source

Source: ProCGroups.FoxDifferential.Completed.Continuous.Automorphism

1import ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Iterated
3/-!
4# Fox differential: completed — continuous — automorphism
6The principal declarations in this module are:
8- `allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse`
9 The named inverse linear map for the completed Fox-Jacobian of a continuous automorphism.
10- `allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse`
11 The named inverse matrix for the completed Fox-Jacobian of a continuous automorphism.
12- `allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage_apply`
13 Evaluation of the finite-stage inverse matrix for a completed Fox-Jacobian of a continuous
14 automorphism.
15- `allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul`
16 The named inverse linear map is row-vector multiplication by the named inverse matrix.
17-/
19namespace FoxDifferential
21noncomputable section
23open scoped BigOperators
25universe u v
27section AllFiniteAutomorphismJacobian
29variable {X F H : Type u}
30variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
31variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
32variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
33variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
36/-- The named inverse linear map for the completed Fox-Jacobian of a continuous automorphism. -/
37def allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
38 {ι : X → F}
41 (e : F ≃* F) (φ : X → H) :
42 ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)
43 →ₗ[ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H]
44 ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H) :=
45 allFinite_freeProCZCCompletedFoxJacobianLinearMap
46 (X := X) (Y := X) (F := F) (F' := F) hι e.symm.toMonoidHom
47 (allFinite_freeProCZCCompletedFoxPullbackGenerator
48 (X := X) (F := F) hι e.toMonoidHom φ ι)
49 ι
51/-- The named inverse matrix for the completed Fox-Jacobian of a continuous automorphism. -/
52def allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
53 {ι : X → F}
56 (e : F ≃* F) (φ : X → H) :
57 Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H) :=
58 allFinite_freeProCZCCompletedFoxJacobianMatrix
59 (X := X) (Y := X) (F := F) (F' := F) hι e.symm.toMonoidHom
60 (allFinite_freeProCZCCompletedFoxPullbackGenerator
61 (X := X) (F := F) hι e.toMonoidHom φ ι)
62 ι
64/--
65A finite-stage projection of the named inverse matrix for a completed Fox-Jacobian of a
66continuous automorphism.
67-/
68def allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
69 {ι : X → F}
72 (e : F ≃* F) (φ : X → H)
73 (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) :
74 Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H j) :=
75 fun x y =>
76 zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
77 (allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
78 (X := X) (F := F) (H := H) hι e φ x y)
80omit [Fintype X] in
81/--
82Evaluation of the finite-stage inverse matrix for a completed Fox-Jacobian of a continuous
83automorphism.
84-/
85@[simp]
86theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage_apply
87 {ι : X → F}
90 (e : F ≃* F) (φ : X → H)
91 (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) (x y : X) :
92 allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
93 (X := X) (F := F) (H := H) hι e φ j x y =
94 zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
95 (allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
96 (X := X) (F := F) (H := H) hι e φ x y) :=
97 rfl
99/-- The named inverse linear map is row-vector multiplication by the named inverse matrix. -/
100theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul
101 {ι : X → F}
104 (e : F ≃* F) (φ : X → H)
105 (v : ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)) :
106 allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
107 (X := X) (F := F) (H := H) hι e φ v =
108 Matrix.vecMul v
109 (allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
110 (X := X) (F := F) (H := H) hι e φ) := by
111 exact allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul
112 (X := X) (F := F) hι e.symm.toMonoidHom
113 (allFinite_freeProCZCCompletedFoxPullbackGenerator
114 (X := X) (F := F) hι e.toMonoidHom φ ι)
115 ι v
117omit [Fintype X] in
118/--
119Pulling the target generator map first along an automorphism and then along its inverse recovers
120the original generator map.
121-/
122theorem allFinite_freeProCZCCompletedFoxAutomorphism_pullback_symm
123 {ι : X → F}
126 (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
127 allFinite_freeProCZCCompletedFoxPullbackGenerator
128 (X := X) (F := F) hι e.symm.toMonoidHom
129 (allFinite_freeProCZCCompletedFoxPullbackGenerator
130 (X := X) (F := F) hι e.toMonoidHom φ ι)
131 ι =
132 φ := by
133 let htarget :
135 (ZCCompletedFoxSemidirect ProCGroups.FiniteGroupClass.allFinite X H) :=
136 ProCGrp.allFinite_property (ProfiniteGrp.of _)
137 let hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C :=
139 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
141 let φe : X → H :=
142 allFinite_freeProCZCCompletedFoxPullbackGenerator
143 (X := X) (F := F) hι e.toMonoidHom φ ι
144 let hφe : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C :=
146 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
148 have hρ := allFinite_freeProCZCCompletedFoxRightHom_comp
149 (X := X) (Y := X) (F := F) (F' := F) (H := H)
150 hι hι e.toMonoidHom he_continuous φ
151 funext x
152 change freeProCZCCompletedFoxRightHom
153 (C := ProCGroups.FiniteGroupClass.allFinite) hι htarget φe hφe
154 (e.symm (ι x)) = φ x
155 have happ := congrFun (congrArg DFunLike.coe hρ) (e.symm (ι x))
156 calc
157 freeProCZCCompletedFoxRightHom
158 (C := ProCGroups.FiniteGroupClass.allFinite) hι htarget φe hφe
159 (e.symm (ι x)) =
160 ((freeProCZCCompletedFoxRightHom
161 (C := ProCGroups.FiniteGroupClass.allFinite) hι htarget φ hφ).comp
162 e.toMonoidHom) (e.symm (ι x)) := by
163 simpa [φe, htarget, hφ, hφe] using happ
164 _ = freeProCZCCompletedFoxRightHom
165 (C := ProCGroups.FiniteGroupClass.allFinite) hι htarget φ hφ (ι x) := by
166 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe,
167 Function.comp_apply,
168 MulEquiv.apply_symm_apply, freeProCZCCompletedFoxRightHom_apply,
169 freeProCZCCompletedFoxSemidirectLift_generator,
170 freeProCZCCompletedFoxSemidirectGenerator_right]
171 _ = φ x := by
172 simp only [freeProCZCCompletedFoxRightHom_apply,
173 freeProCZCCompletedFoxSemidirectLift_generator,
174 freeProCZCCompletedFoxSemidirectGenerator_right]
176/--
177Composing the completed Fox-Jacobian linear map of a continuous automorphism with its named
178inverse gives the identity.
179-/
180theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse
181 {ι : X → F}
184 (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
185 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
186 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι).comp
187 (allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
188 (X := X) (F := F) (H := H) hι e φ) =
189 LinearMap.id := by
190 apply linearMap_ext_pi_single
191 intro x
192 have hchain := allFinite_freeProCZCCompletedFoxDerivativeVector_comp
193 (X := X) (Y := X) (F := F) (F' := F) (H := H)
194 hι hι e.toMonoidHom he_continuous φ (e.symm (ι x))
195 convert hchain.symm using 1
196 all_goals
197 simp [LinearMap.comp_apply,
198 allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse,
199 allFinite_freeProCZCCompletedFoxJacobianLinearMap,
200 allFinite_freeProCZCCompletedFoxJacobian]
201 all_goals rfl
203/--
204Composing the named inverse for the completed Fox-Jacobian linear map of a continuous
205automorphism with the Jacobian gives the identity.
206-/
207theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp
208 {ι : X → F}
211 (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
212 (φ : X → H) :
213 (allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
214 (X := X) (F := F) (H := H) hι e φ).comp
215 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
216 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι) =
217 LinearMap.id := by
218 apply linearMap_ext_pi_single
219 intro x
220 let φe : X → H :=
221 allFinite_freeProCZCCompletedFoxPullbackGenerator
222 (X := X) (F := F) hι e.toMonoidHom φ ι
223 have hpull :
224 allFinite_freeProCZCCompletedFoxPullbackGenerator
225 (X := X) (F := F) hι e.symm.toMonoidHom φe ι =
226 φ := by
227 simpa [φe] using
228 allFinite_freeProCZCCompletedFoxAutomorphism_pullback_symm
229 (X := X) (F := F) (H := H) hι e he_continuous φ
230 have hchain := allFinite_freeProCZCCompletedFoxDerivativeVector_comp
231 (X := X) (Y := X) (F := F) (F' := F) (H := H)
232 hι hι e.symm.toMonoidHom he_symm_continuous φe (e (ι x))
233 rw [hpull] at hchain
234 convert hchain.symm using 1
235 · simp only [
236 allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse,
237 allFinite_freeProCZCCompletedFoxJacobianLinearMap,
238 MulEquiv.toMonoidHom_eq_coe, LinearMap.comp_apply,
239 foxJacobianLinearMap_single, allFinite_freeProCZCCompletedFoxJacobian,
240 MonoidHom.coe_coe, φe]
241 · simpa only [LinearMap.id_coe, id_eq, MulEquiv.toMonoidHom_eq_coe,
242 MonoidHom.coe_coe, MulEquiv.symm_apply_apply] using
243 (freeProCZCCompletedFoxDerivativeVector_generator
245 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φe
246 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
249/--
250The named inverse matrix is a left inverse for the completed Fox-Jacobian matrix of a continuous
251automorphism.
252-/
253theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse_mul
254 {ι : X → F}
257 (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
258 allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
259 (X := X) (F := F) (H := H) hι e φ *
260 allFinite_freeProCZCCompletedFoxJacobianMatrix
261 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι =
262 (1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H)) := by
263 rw [Matrix.ext_iff_vecMul]
264 intro v
265 have hlin :=
266 allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse
267 (X := X) (F := F) (H := H) hι e he_continuous φ
268 have happ := congrFun (congrArg DFunLike.coe hlin) v
269 simpa [LinearMap.comp_apply,
270 allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul,
271 allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul,
272 Matrix.vecMul_vecMul, Matrix.vecMul_one] using happ
274/--
275The named inverse matrix is a right inverse for the completed Fox-Jacobian matrix of a
276continuous automorphism.
277-/
278theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrix_mul_inverse
279 {ι : X → F}
282 (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
283 (φ : X → H) :
284 allFinite_freeProCZCCompletedFoxJacobianMatrix
285 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι *
286 allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
287 (X := X) (F := F) (H := H) hι e φ =
288 (1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H)) := by
289 rw [Matrix.ext_iff_vecMul]
290 intro v
291 have hlin :=
292 allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp
293 (X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φ
294 have happ := congrFun (congrArg DFunLike.coe hlin) v
295 simpa [LinearMap.comp_apply,
296 allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul,
297 allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul,
298 Matrix.vecMul_vecMul, Matrix.vecMul_one] using happ
300/--
301The finite-stage inverse matrix is a left inverse for the finite-stage completed Fox-Jacobian
302matrix of a continuous automorphism.
303-/
304theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStageInverse_mul
305 {ι : X → F}
308 (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H)
309 (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) :
310 allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
311 (X := X) (F := F) (H := H) hι e φ j *
312 allFinite_freeProCZCCompletedFoxJacobianMatrixStage
313 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι j =
314 (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H j))
315 := by
316 apply Matrix.ext
317 intro x y
318 have h := congrArg
319 (fun M : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H) =>
320 zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j (M x y))
321 (allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse_mul
322 (X := X) (F := F) (H := H) hι e he_continuous φ)
323 have hone :
324 zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
325 ((1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H)) x y) =
326 (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H
327 j)) x y := by
328 by_cases hxy : x = y
329 · subst y
330 simp only [zcCompletedGroupAlgebraProjection, Matrix.one_apply_eq,
331 zcCompletedGroupAlgebraProjection_one]
332 · simp only [zcCompletedGroupAlgebraProjection, ne_eq, hxy, not_false_eq_true,
333 Matrix.one_apply_ne,
334 zcCompletedGroupAlgebraProjection_zero]
335 simp only [Matrix.mul_apply] at h
336 rw [zcCompletedGroupAlgebraProjection_sum] at h
337 rw [hone] at h
338 simp only [zcCompletedGroupAlgebraProjection, MulEquiv.toMonoidHom_eq_coe,
339 allFinite_freeProCZCCompletedFoxJacobianMatrix_apply, zcCompletedGroupAlgebraProjection_mul] at h
340 simpa [Matrix.mul_apply,
341 allFinite_freeProCZCCompletedFoxJacobianMatrixStage,
342 allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage] using h
344/--
345The finite-stage inverse matrix is a right inverse for the finite-stage completed Fox-Jacobian
346matrix of a continuous automorphism.
347-/
348theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStage_mul_inverse
349 {ι : X → F}
352 (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
353 (φ : X → H) (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) :
354 allFinite_freeProCZCCompletedFoxJacobianMatrixStage
355 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι j *
356 allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
357 (X := X) (F := F) (H := H) hι e φ j =
358 (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H j))
359 := by
360 apply Matrix.ext
361 intro x y
362 have h := congrArg
363 (fun M : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H) =>
364 zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j (M x y))
365 (allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrix_mul_inverse
366 (X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φ)
367 have hone :
368 zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
369 ((1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H)) x y) =
370 (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H
371 j)) x y := by
372 by_cases hxy : x = y
373 · subst y
374 simp only [zcCompletedGroupAlgebraProjection, Matrix.one_apply_eq,
375 zcCompletedGroupAlgebraProjection_one]
376 · simp only [zcCompletedGroupAlgebraProjection, ne_eq, hxy, not_false_eq_true,
377 Matrix.one_apply_ne,
378 zcCompletedGroupAlgebraProjection_zero]
379 simp only [Matrix.mul_apply] at h
380 rw [zcCompletedGroupAlgebraProjection_sum] at h
381 rw [hone] at h
382 simp only [zcCompletedGroupAlgebraProjection, MulEquiv.toMonoidHom_eq_coe,
383 allFinite_freeProCZCCompletedFoxJacobianMatrix_apply, zcCompletedGroupAlgebraProjection_mul] at h
384 simpa [Matrix.mul_apply,
385 allFinite_freeProCZCCompletedFoxJacobianMatrixStage,
386 allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage] using h
388/-- The completed Fox-Jacobian of a continuous automorphism is bundled into a linear equivalence. -/
389def allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearEquiv
390 {ι : X → F}
393 (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
394 (φ : X → H) :
395 ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)
396 ≃ₗ[ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H]
397 ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H) := by
398 refine LinearEquiv.ofLinear
399 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
400 (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι)
401 (allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
402 (X := X) (F := F) (H := H) hι e φ)
403 ?_ ?_
404 · exact allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse
405 (X := X) (F := F) (H := H) hι e he_continuous φ
406 · exact allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp
407 (X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φ
409end AllFiniteAutomorphismJacobian
411end
413end FoxDifferential