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

Source: ProCGroups.FoxDifferential.Completed.Continuous.Naturality

1import ProCGroups.FoxDifferential.Completed.Continuous.Free.Rules
3/-!
4# Fox differential: completed — continuous — naturality
6The principal declarations in this module are:
8- `zcCompletedFoxSemidirectMapTarget`
9 Target functoriality for completed Fox semidirect products.
10- `zcCompletedFoxSemidirectMapTargetHom`
11 Target functoriality for completed Fox semidirect products as a continuous homomorphism.
12- `continuous_zcCompletedGroupAlgebraMap`
13 The completed group-algebra map induced by a continuous target homomorphism is continuous.
14- `zcCompletedGroupAlgebraMap_surjective_of_surjective`
15 A surjective target homomorphism induces a surjective completed group-algebra map.
16-/
18namespace FoxDifferential
20noncomputable section
22open ProCGroups.Completion
23open ProCGroups.InverseSystems
24open ProCGroups.ProC
25open scoped BigOperators
27universe u v
29section ContinuousTargetMaps
31variable (C : ProCGroups.FiniteGroupClass.{u})
33variable {H K : Type u}
34variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
35variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
37/-- The completed group-algebra map induced by a continuous target homomorphism is continuous. -/
38theorem continuous_zcCompletedGroupAlgebraMap (η : H →ₜ* K) :
39 Continuous (zcCompletedGroupAlgebraMap C hC η) := by
40 refine Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C K)
41 (continuous_pi fun i => ?_) (fun x => (zcCompletedGroupAlgebraMap C hC η x).2)
42 let sourceIndex : ZCCompletedGroupAlgebraIndex C H :=
43 (i.1, completedGroupAlgebraComapIndexInClass
44 (G := H) (H := K) C hC η i.2)
45 letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H sourceIndex) := ⊥
46 letI : DiscreteTopology (ZCCompletedGroupAlgebraStage C H sourceIndex) := ⟨rfl⟩
47 have hstage : Continuous (zcCompletedGroupAlgebraMapStage C hC η i) :=
48 continuous_of_discreteTopology
49 exact hstage.comp ((continuous_apply sourceIndex).comp continuous_subtype_val)
51/-- A surjective target homomorphism induces a surjective completed group-algebra map. -/
52theorem zcCompletedGroupAlgebraMap_surjective_of_surjective
55 (η : H →ₜ* K) (hη : Function.Surjective η) :
56 Function.Surjective (zcCompletedGroupAlgebraMap C hC η) := by
57 let S := zcCompletedGroupAlgebraSystem C K
58 let ψ : ∀ i : ZCCompletedGroupAlgebraIndex C K,
59 ZCCompletedGroupAlgebra C H → S.X i :=
60 fun i x => zcCompletedGroupAlgebraProjection C K i
61 (zcCompletedGroupAlgebraMap C hC η x)
62 have hψcont : ∀ i, Continuous (ψ i) := by
63 intro i
64 exact (continuous_apply i).comp
65 (continuous_subtype_val.comp (continuous_zcCompletedGroupAlgebraMap C hC η))
66 have hψcompat : S.CompatibleMaps ψ := by
67 intro i j hij
68 funext x
69 change zcCompletedGroupAlgebraTransition C K hij
70 (zcCompletedGroupAlgebraProjection C K j
71 (zcCompletedGroupAlgebraMap C hC η x)) =
72 zcCompletedGroupAlgebraProjection C K i
73 (zcCompletedGroupAlgebraMap C hC η x)
74 exact (zcCompletedGroupAlgebraMap C hC η x).2 i j hij
75 have hψsurj : ∀ i, Function.Surjective (ψ i) := by
76 intro i y
77 rcases zcCompletedGroupAlgebraMapStage_surjective_of_surjective
78 C hC η hη i y with ⟨y₀, hy₀⟩
79 rcases zcCompletedGroupAlgebraProjection_surjective C H
80 (i.1, completedGroupAlgebraComapIndexInClass
81 (G := H) (H := K) C hC η i.2) y₀ with ⟨x, hx⟩
82 refine ⟨x, ?_⟩
83 dsimp [ψ]
84 rw [hx, hy₀]
85 letI : Nonempty (ZCCompletedGroupAlgebraIndex C K) :=
86 ⟨(ProCIntegerIndex.terminal (C := C) inferInstance, zcCompletedGroupAlgebraTopIndex C K)⟩
87 have hdir : Directed (· ≤ ·)
88 (id : ZCCompletedGroupAlgebraIndex C K → ZCCompletedGroupAlgebraIndex C K) := by
89 intro i j
90 rcases ProCIntegerIndex.directed_of_formation hForm i.1 j.1 with
91 ⟨n, hin, hjn⟩
92 rcases directed_openNormalSubgroupInClass
93 (C := C) (G := K) hForm i.2 j.2 with
94 ⟨U, hiU, hjU⟩
95 exact ⟨(n, U), ⟨hin, hiU⟩, ⟨hjn, hjU⟩⟩
96 letI : ∀ i : ZCCompletedGroupAlgebraIndex C K, T2Space (S.X i) := fun i => by
97 dsimp [S, zcCompletedGroupAlgebraSystem]
98 change @T2Space (ZCCompletedGroupAlgebraStage C K i) ⊥
99 exact @DiscreteTopology.toT2Space _ ⊥ ⟨rfl⟩
100 have hlift : Function.Surjective (S.inverseLimitLift ψ hψcompat) :=
101 S.surjective_inverseLimitLift ψ hψcont hψcompat hψsurj hdir
102 intro y
103 rcases hlift y with ⟨x, hx⟩
104 refine ⟨x, ?_⟩
105 apply Subtype.ext
106 funext i
107 have hi := congrArg (fun z : S.inverseLimit => S.projection i z) hx
108 convert hi using 1 <;> rfl
110/-- A surjective completed group-algebra map is a quotient map. -/
111theorem isQuotientMap_zcCompletedGroupAlgebraMap_of_surjective
114 (η : H →ₜ* K) (hη : Function.Surjective η) :
115 Topology.IsQuotientMap (zcCompletedGroupAlgebraMap C hC η) :=
116 Topology.IsQuotientMap.of_surjective_continuous
117 (zcCompletedGroupAlgebraMap_surjective_of_surjective C hC hForm η hη)
118 (continuous_zcCompletedGroupAlgebraMap C hC η)
120/--
121A surjective completed group-algebra map is an open quotient map as an additive-group
122homomorphism.
123-/
124theorem isOpenQuotientMap_zcCompletedGroupAlgebraMap_of_surjective
127 (η : H →ₜ* K) (hη : Function.Surjective η) :
128 IsOpenQuotientMap (zcCompletedGroupAlgebraMap C hC η) :=
129 AddMonoidHom.isOpenQuotientMap_of_isQuotientMap
130 (isQuotientMap_zcCompletedGroupAlgebraMap_of_surjective C hC hForm η hη)
132variable {X : Type v}
134/-- The coordinatewise target map on completed Fox-coordinate vectors is continuous. -/
135theorem continuous_zcFreeFoxCoordinatesMap (η : H →ₜ* K) :
136 Continuous (zcFreeFoxCoordinatesMap (X := X) C hC η) := by
137 refine continuous_pi fun x => ?_
138 exact (continuous_zcCompletedGroupAlgebraMap C hC η).comp (continuous_apply x)
140end ContinuousTargetMaps
142section SourceBoundaryNaturality
144variable (C : ProCGroups.FiniteGroupClass.{u})
146variable {X H K : Type u} [Fintype X]
147variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
148variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
150/-- Source-shaped completed Fox boundary maps are natural in the target group. -/
151theorem freeProCZCCompletedFoxBoundary_mapTarget
152 (η : H →ₜ* K) (φ : X → H)
153 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
154 zcCompletedGroupAlgebraMap C hC η (freeProCZCCompletedFoxBoundary C φ v) =
155 freeProCZCCompletedFoxBoundary C (fun x : X => η (φ x))
156 (zcFreeFoxCoordinatesMap (X := X) C hC η v) := by
157 simp only [freeProCZCCompletedFoxBoundary_apply, map_sum, map_mul, map_sub,
158 zcCompletedGroupAlgebraMap_groupLike, map_one, zcFreeFoxCoordinatesMap]
160end SourceBoundaryNaturality
162section SemidirectTargetMap
164variable (C : ProCGroups.FiniteGroupClass.{u})
166variable {X H K : Type u} [DecidableEq X]
167variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
168variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
170/-- Target functoriality for completed Fox semidirect products. -/
171def zcCompletedFoxSemidirectMapTarget (η : H →ₜ* K) :
172 ZCCompletedFoxSemidirect C X H →* ZCCompletedFoxSemidirect C X K where
173 toFun a :=
174 { left := zcFreeFoxCoordinatesMap (X := X) C hC η a.left
175 right := η a.right }
176 map_one' := by
177 ext x
178 · simp only [ZCCompletedFoxSemidirect.one_left, zcFreeFoxCoordinatesMap_apply,
179 Pi.zero_apply, map_zero, zcCompletedGroupAlgebraProjection_zero]
180 · simp only [ZCCompletedFoxSemidirect.one_right, map_one]
181 map_mul' a b := by
182 ext x
183 · simp only [ZCCompletedFoxSemidirect.mul_left, zcFreeFoxCoordinatesMap_apply,
184 Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_add, map_mul,
185 zcCompletedGroupAlgebraMap_groupLike, zcCompletedGroupAlgebraProjection_add,
186 zcCompletedGroupAlgebraProjection_map, zcCompletedGroupAlgebraProjection_mul,
187 zcCompletedGroupAlgebraProjection_groupLike, MonoidAlgebra.of_apply,
188 MonoidAlgebra.coeff_add]
189 · simp only [ZCCompletedFoxSemidirect.mul_right, map_mul]
191omit [DecidableEq X] in
192/--
193This declaration identifies the left component of the target map on completed Fox semidirect
194products.
195-/
196@[simp]
197theorem zcCompletedFoxSemidirectMapTarget_left
198 (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
199 (zcCompletedFoxSemidirectMapTarget (X := X) C hC η a).left =
200 zcFreeFoxCoordinatesMap (X := X) C hC η a.left :=
201 rfl
203omit [DecidableEq X] in
204/--
205This declaration identifies the right component of the target map on completed Fox semidirect
206products.
207-/
208@[simp]
209theorem zcCompletedFoxSemidirectMapTarget_right
210 (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
211 (zcCompletedFoxSemidirectMapTarget (X := X) C hC η a).right = η a.right :=
212 rfl
214omit [DecidableEq X] in
215/-- The target map on completed Fox semidirect products is continuous. -/
216theorem continuous_zcCompletedFoxSemidirectMapTarget
217 (η : H →ₜ* K) :
218 Continuous (zcCompletedFoxSemidirectMapTarget (X := X) C hC η) := by
219 rw [continuous_induced_rng]
220 refine (continuous_zcFreeFoxCoordinatesMap (X := X) C hC η).comp
221 (continuous_zcCompletedFoxSemidirect_left C X H) |>.prodMk ?_
222 exact η.continuous_toFun.comp (continuous_zcCompletedFoxSemidirect_right C X H)
224/-- Target functoriality for completed Fox semidirect products as a continuous homomorphism. -/
225def zcCompletedFoxSemidirectMapTargetHom (η : H →ₜ* K) :
226 ZCCompletedFoxSemidirect C X H →ₜ* ZCCompletedFoxSemidirect C X K where
227 toMonoidHom := zcCompletedFoxSemidirectMapTarget (X := X) C hC η
228 continuous_toFun := continuous_zcCompletedFoxSemidirectMapTarget (X := X) C hC η
230omit [DecidableEq X] in
231/-- The continuous target map has the expected underlying homomorphism. -/
232@[simp]
233theorem zcCompletedFoxSemidirectMapTargetHom_toMonoidHom
234 (η : H →ₜ* K) :
235 (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η).toMonoidHom =
236 zcCompletedFoxSemidirectMapTarget (X := X) C hC η :=
237 rfl
239omit [DecidableEq X] in
240/--
241This declaration identifies the left component of the continuous target map on completed Fox
242semidirect products.
243-/
244@[simp]
245theorem zcCompletedFoxSemidirectMapTargetHom_left
246 (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
247 (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η a).left =
248 zcFreeFoxCoordinatesMap (X := X) C hC η a.left :=
249 rfl
251omit [DecidableEq X] in
252/--
253This declaration identifies the right component of the continuous target map on completed Fox
254semidirect products.
255-/
256@[simp]
257theorem zcCompletedFoxSemidirectMapTargetHom_right
258 (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
259 (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η a).right = η a.right :=
260 rfl
262end SemidirectTargetMap
264section SourceNaturality
266variable {C : ProCGroups.FiniteGroupClass.{u}}
268include hC
269variable {X F H K : Type u}
270variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
271variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
272variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
273variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
274variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
275variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
276variable [T2Space (ZCCompletedFoxSemidirect C X H)]
277variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
278variable [CompactSpace (ZCCompletedFoxSemidirect C X K)]
279variable [T2Space (ZCCompletedFoxSemidirect C X K)]
280variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X K)]
282omit [Fintype X] in
283/-- Target naturality of the canonical completed Fox semidirect lift. -/
284theorem freeProCZCCompletedFoxSemidirectLift_mapTarget
285 {ι : X → F}
287 (htargetH :
288 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
289 (htargetK :
290 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
291 (η : H →ₜ* K) (φ : X → H) (g : F) :
292 zcCompletedFoxSemidirectMapTarget (X := X) C hC η
293 (freeProCZCCompletedFoxSemidirectLift
294 (C := C) hι htargetH φ
295 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g) =
296 freeProCZCCompletedFoxSemidirectLift
297 (C := C) hι htargetK (fun x : X => η (φ x))
298 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
299 X => η (φ x))) g := by
300 let hφH : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) :=
301 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ
302 let φK : X → K := fun x => η (φ x)
303 let hφK : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φK) :=
304 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K φK
305 let f : F →* ZCCompletedFoxSemidirect C X K :=
306 (zcCompletedFoxSemidirectMapTarget (X := X) C hC η).comp
307 (freeProCZCCompletedFoxSemidirectLift
308 (C := C) hι htargetH φ hφH)
309 let h : F →* ZCCompletedFoxSemidirect C X K :=
310 freeProCZCCompletedFoxSemidirectLift
311 (C := C) hι htargetK φK hφK
312 have hf_continuous : Continuous f :=
313 (continuous_zcCompletedFoxSemidirectMapTarget
314 (X := X) C hC η).comp
315 (continuous_freeProCZCCompletedFoxSemidirectLift
316 (C := C) hι htargetH φ hφH)
317 have hh_continuous : Continuous h :=
318 continuous_freeProCZCCompletedFoxSemidirectLift
319 (C := C) hι htargetK φK hφK
320 have hfg : ∀ x : X, f (ι x) = h (ι x) := by
321 intro x
322 change
323 zcCompletedFoxSemidirectMapTarget (X := X) C hC η
324 (freeProCZCCompletedFoxSemidirectLift
325 (C := C) hι htargetH φ hφH (ι x)) =
326 freeProCZCCompletedFoxSemidirectLift
327 (C := C) hι htargetK φK hφK (ι x)
328 rw [freeProCZCCompletedFoxSemidirectLift_generator,
329 freeProCZCCompletedFoxSemidirectLift_generator]
330 apply ZCCompletedFoxSemidirect.ext
331 · funext y
332 by_cases hxy : x = y
333 · subst y
334 simp only [zcCompletedFoxSemidirectMapTarget_left, zcFreeFoxCoordinatesMap,
335 freeProCZCCompletedFoxSemidirectGenerator_left, Pi.single_eq_same, map_one]
336 · simp only [zcCompletedFoxSemidirectMapTarget_left, zcFreeFoxCoordinatesMap,
337 freeProCZCCompletedFoxSemidirectGenerator_left, ne_eq, hxy, not_false_eq_true,
338 Pi.single_eq_of_ne', map_zero]
339 · simp only [zcCompletedFoxSemidirectMapTarget_right,
340 freeProCZCCompletedFoxSemidirectGenerator_right, φK]
341 have hfh : f = h := hι.hom_ext htargetK hf_continuous hh_continuous hfg
342 exact congrFun (congrArg DFunLike.coe hfh) g
344omit [Fintype X] in
345/-- Continuous-hom form of target naturality for the canonical completed Fox semidirect lift. -/
346theorem freeProCZCCompletedFoxSemidirectLiftHom_mapTarget
347 {ι : X → F}
349 (htargetH :
350 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
351 (htargetK :
352 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
353 (η : H →ₜ* K) (φ : X → H) :
354 (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η).comp
355 (freeProCZCCompletedFoxSemidirectLiftHom
356 (C := C) hι htargetH φ
357 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)) =
358 freeProCZCCompletedFoxSemidirectLiftHom
359 (C := C) hι htargetK (fun x : X => η (φ x))
360 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
361 X => η (φ x))) := by
362 apply ContinuousMonoidHom.ext
363 intro g
364 exact freeProCZCCompletedFoxSemidirectLift_mapTarget
365 (C := C) (X := X) (F := F) (H := H) (K := K)
366 hC hι htargetH htargetK η φ g
368omit [Fintype X] in
369/-- Target naturality of the right homomorphism of the canonical completed Fox lift. -/
370theorem freeProCZCCompletedFoxRightHom_mapTarget
371 {ι : X → F}
373 (htargetH :
374 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
375 (htargetK :
376 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
377 (η : H →ₜ* K) (φ : X → H) :
378 freeProCZCCompletedFoxRightHom
379 (C := C) hι htargetK (fun x : X => η (φ x))
380 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
381 X => η (φ x))) =
382 η.toMonoidHom.comp
383 (freeProCZCCompletedFoxRightHom
384 (C := C) hι htargetH φ
385 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)) := by
386 ext g
387 have h := congrArg ZCCompletedFoxSemidirect.right
388 (freeProCZCCompletedFoxSemidirectLift_mapTarget
389 (C := C) (X := X) (F := F) (H := H) (K := K)
390 hC hι htargetH htargetK η φ g)
391 simpa [freeProCZCCompletedFoxRightHom_apply, MonoidHom.comp_apply] using h.symm
393omit [Fintype X] in
394/-- Target naturality of the derivative vector of the canonical completed Fox lift. -/
395theorem freeProCZCCompletedFoxDerivativeVector_mapTarget
396 {ι : X → F}
398 (htargetH :
399 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
400 (htargetK :
401 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
402 (η : H →ₜ* K) (φ : X → H) (g : F) :
403 freeProCZCCompletedFoxDerivativeVector
404 (C := C) hι htargetK (fun x : X => η (φ x))
405 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
406 X => η (φ x))) g =
407 zcFreeFoxCoordinatesMap (X := X) C hC η
408 (freeProCZCCompletedFoxDerivativeVector
409 (C := C) hι htargetH φ
410 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g) := by
411 have h := congrArg ZCCompletedFoxSemidirect.left
412 (freeProCZCCompletedFoxSemidirectLift_mapTarget
413 (C := C) (X := X) (F := F) (H := H) (K := K)
414 hC hι htargetH htargetK η φ g)
415 convert h.symm using 1 <;> rfl
417omit [Fintype X] in
418/-- Target naturality for the canonical completed Fox derivative holds componentwise. -/
419theorem freeProCZCCompletedFoxDerivativeVector_mapTarget_apply
420 {ι : X → F}
422 (htargetH :
423 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
424 (htargetK :
425 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
426 (η : H →ₜ* K) (φ : X → H) (g : F) (x : X) :
427 freeProCZCCompletedFoxDerivativeVector
428 (C := C) hι htargetK (fun x : X => η (φ x))
429 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
430 X => η (φ x))) g x =
431 zcCompletedGroupAlgebraMap C hC η
432 (freeProCZCCompletedFoxDerivativeVector
433 (C := C) hι htargetH φ
434 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g x)
435 := by
436 have h := congrFun
437 (freeProCZCCompletedFoxDerivativeVector_mapTarget
438 (C := C) (X := X) (F := F) (H := H) (K := K)
439 hC hι htargetH htargetK η φ g) x
440 simpa [zcFreeFoxCoordinatesMap] using h
442/--
443Target naturality for the source-shaped boundary applied to the canonical completed Fox
444derivative vector.
445-/
446theorem freeProCZCCompletedFoxBoundary_mapTarget_of_derivativeVector
447 {ι : X → F}
449 (htargetH :
450 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
451 (htargetK :
452 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
453 (η : H →ₜ* K) (φ : X → H) (g : F) :
454 zcCompletedGroupAlgebraMap C hC η
455 (freeProCZCCompletedFoxBoundary C φ
456 (freeProCZCCompletedFoxDerivativeVector
457 (C := C) hι htargetH φ
458 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g)) =
459 freeProCZCCompletedFoxBoundary C (fun x : X => η (φ x))
460 (freeProCZCCompletedFoxDerivativeVector
461 (C := C) hι htargetK (fun x : X => η (φ x))
462 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x
463 : X => η (φ x))) g) := by
464 rw [freeProCZCCompletedFoxBoundary_mapTarget]
465 rw [← freeProCZCCompletedFoxDerivativeVector_mapTarget
466 (C := C) (X := X) (F := F) (H := H) (K := K)
467 hC hι htargetH htargetK η φ g]
469end SourceNaturality
471end
473end FoxDifferential