Source: ProCGroups.FoxDifferential.Completed.Semidirect
1import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Core
2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental
4/-!
5# Fox differential: completed — semidirect
7The principal declarations in this module are:
9- `ZCCompletedFoxSemidirect`
10 The completed Fox semidirect target `Z_C[[H]]^X ⋊ H`.
11- `rightMonoidHom`
12 The right projection from the completed Fox semidirect product to the target group.
13- `ext`
14 Extensionality for completed Fox semidirect elements.
15- `one_left`
16 The left component of the identity semidirect element is zero.
17-/
19namespace FoxDifferential
21noncomputable section
23open scoped BigOperators
25universe u v
27variable (C : ProCGroups.FiniteGroupClass.{v})
28variable (X : Type u) [DecidableEq X]
29variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
31omit [DecidableEq X] in
32/-- The completed Fox semidirect target `Z_C[[H]]^X ⋊ H`. -/
33structure ZCCompletedFoxSemidirect where
34 /-- The completed Fox-coordinate component. -/
35 left : ZCFreeFoxCoordinates C (X := X) (H := H)
36 /-- The target group component. -/
37 right : H
39namespace ZCCompletedFoxSemidirect
41omit [DecidableEq X] in
42/-- Extensionality for completed Fox semidirect elements. -/
43@[ext]
44theorem ext {a b : ZCCompletedFoxSemidirect C X H}
45 (hleft : a.left = b.left) (hright : a.right = b.right) : a = b := by
46 cases a
47 cases b
48 simp_all
50/-- Identity element of the completed Fox semidirect product. -/
51instance instOneZCCompletedFoxSemidirect : One (ZCCompletedFoxSemidirect C X H) where
52 one := ⟨0, 1⟩
54/-- Multiplication in the completed Fox semidirect product. -/
55instance instMulZCCompletedFoxSemidirect : Mul (ZCCompletedFoxSemidirect C X H) where
56 mul a b :=
57 ⟨a.left + zcGroupLike C H a.right • b.left, a.right * b.right⟩
59/-- Inversion in the completed Fox semidirect product. -/
60instance instInvZCCompletedFoxSemidirect : Inv (ZCCompletedFoxSemidirect C X H) where
61 inv a :=
62 ⟨-(zcGroupLike C H a.right⁻¹ • a.left), a.right⁻¹⟩
64omit [DecidableEq X] in
65/-- The left component of the identity semidirect element is zero. -/
66@[simp]
67theorem one_left :
68 (1 : ZCCompletedFoxSemidirect C X H).left = 0 :=
69 rfl
71omit [DecidableEq X] in
72/-- The right component of the identity semidirect element is the group identity. -/
73@[simp]
74theorem one_right :
75 (1 : ZCCompletedFoxSemidirect C X H).right = 1 :=
76 rfl
78omit [DecidableEq X] in
79/-- The left component of semidirect multiplication. -/
80@[simp]
81theorem mul_left (a b : ZCCompletedFoxSemidirect C X H) :
82 (a * b).left = a.left + zcGroupLike C H a.right • b.left :=
83 rfl
85omit [DecidableEq X] in
86/-- The right component of semidirect multiplication. -/
87@[simp]
88theorem mul_right (a b : ZCCompletedFoxSemidirect C X H) :
89 (a * b).right = a.right * b.right :=
90 rfl
92omit [DecidableEq X] in
93/-- The left component of semidirect inversion. -/
94@[simp]
95theorem inv_left (a : ZCCompletedFoxSemidirect C X H) :
96 a⁻¹.left = -(zcGroupLike C H a.right⁻¹ • a.left) :=
97 rfl
99omit [DecidableEq X] in
100/-- The right component of semidirect inversion. -/
101@[simp]
102theorem inv_right (a : ZCCompletedFoxSemidirect C X H) :
103 a⁻¹.right = a.right⁻¹ :=
104 rfl
106/-- Group structure on the completed Fox semidirect product. -/
107instance instGroupZCCompletedFoxSemidirect : Group (ZCCompletedFoxSemidirect C X H) where
108 one := 1
109 mul := (· * ·)
110 inv := Inv.inv
111 mul_assoc a b c := by
112 ext
113 · simp only [mul_left, mul_right, map_mul, Pi.add_apply, Pi.smul_apply, smul_eq_mul, add_assoc,
114 zcCompletedGroupAlgebraProjection_add, zcCompletedGroupAlgebraProjection_mul,
115 zcCompletedGroupAlgebraProjection_groupLike, MonoidAlgebra.of_apply,
116 MonoidAlgebra.single_mul_single, mul_one, MonoidAlgebra.coeff_add, smul_add, smul_smul]
117 · simp only [mul_right, mul_assoc]
118 one_mul a := by
119 ext
120 · simp only [mul_left, one_left, one_right, map_one, one_smul, Pi.add_apply, Pi.zero_apply,
121 zero_add]
122 · simp only [mul_right, one_right, one_mul]
123 mul_one a := by
124 ext
125 · simp only [mul_left, one_left, smul_zero, Pi.add_apply, Pi.zero_apply, add_zero]
126 · simp only [mul_right, one_right, mul_one]
127 inv_mul_cancel a := by
128 ext
129 · simp only [mul_left, inv_left, inv_right, Pi.add_apply, Pi.neg_apply, Pi.smul_apply,
130 smul_eq_mul,
131 neg_add_cancel, zcCompletedGroupAlgebraProjection_zero, Pi.zero_apply, one_left]
132 · simp only [mul_right, inv_right, inv_mul_cancel, one_right]
134omit [DecidableEq X] in
135/-- The right projection from the completed Fox semidirect product to the target group. -/
136def rightMonoidHom : ZCCompletedFoxSemidirect C X H →* H where
137 toFun a := a.right
138 map_one' := rfl
139 map_mul' _ _ := rfl
141omit [DecidableEq X] in
142/-- Projection to the right factor of the completed Fox semidirect product returns its stored
143group element. -/
144@[simp]
145theorem rightMonoidHom_apply (a : ZCCompletedFoxSemidirect C X H) :
146 rightMonoidHom C X H a = a.right :=
147 rfl
149end ZCCompletedFoxSemidirect
151section Lift
153variable {X H}
155/-- The completed Fox semidirect lift of a free group homomorphism. -/
156def zcCompletedFoxSemidirectLift (ψ : FreeGroup X →* H) :
157 FreeGroup X →* ZCCompletedFoxSemidirect C X H :=
158 FreeGroup.lift fun x =>
159 { left := Pi.single x (1 : ZCCompletedGroupAlgebra C H)
160 right := ψ (FreeGroup.of x) }
162/-- The right component of the completed Fox semidirect lift is `ψ`. -/
163@[simp]
164theorem zcCompletedFoxSemidirectLift_right
165 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
166 (zcCompletedFoxSemidirectLift C ψ w).right = ψ w := by
167 induction w using FreeGroup.induction_on with
168 | C1 =>
169 simp only [zcCompletedFoxSemidirectLift, map_one, ZCCompletedFoxSemidirect.one_right]
170 | of x =>
171 simp only [zcCompletedFoxSemidirectLift, FreeGroup.lift_apply_of]
172 | inv_of x hx =>
173 simpa using congrArg Inv.inv hx
174 | mul u v hu hv =>
175 simp only [map_mul, ZCCompletedFoxSemidirect.mul_right, hu, hv]
177/-- The left component of the completed Fox semidirect lift. -/
178def zcCompletedFoxSemidirectDerivativeVector
179 (ψ : FreeGroup X →* H) :
180 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
181 (ZCFreeFoxCoordinates C (X := X) (H := H)) where
182 toFun w := (zcCompletedFoxSemidirectLift C ψ w).left
183 map_mul' u v := by
184 simp only [scalarCrossedAction_apply, map_mul, ZCCompletedFoxSemidirect.mul_left,
185 zcCompletedFoxSemidirectLift_right,
186 zcCompletedGroupAlgebraScalar_apply]
188/-- The completed semidirect derivative vector sends a free generator to the coordinate basis
189vector. -/
190@[simp]
191theorem zcCompletedFoxSemidirectDerivativeVector_of
192 (ψ : FreeGroup X →* H) (x : X) :
193 zcCompletedFoxSemidirectDerivativeVector C ψ (FreeGroup.of x) =
194 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
195 change (zcCompletedFoxSemidirectLift C ψ (FreeGroup.of x)).left =
196 Pi.single x (1 : ZCCompletedGroupAlgebra C H)
197 simp only [zcCompletedFoxSemidirectLift, FreeGroup.lift_apply_of]
199/-- The completed semidirect derivative vector is the completed free-group Fox derivative
200vector. -/
201theorem zcCompletedFoxSemidirectDerivativeVector_eq
202 (ψ : FreeGroup X →* H) :
203 zcCompletedFoxSemidirectDerivativeVector C ψ =
204 zcFreeGroupFoxDerivativeVector C ψ := by
205 exact zcFreeGroupFoxDerivativeVector_unique C ψ
206 (zcCompletedFoxSemidirectDerivativeVector C ψ)
207 (zcCompletedFoxSemidirectDerivativeVector_of C ψ)
209/-- The completed semidirect lift stores the completed Fox derivative vector and the target
210homomorphism. -/
211theorem zcCompletedFoxSemidirectLift_eq
212 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
213 zcCompletedFoxSemidirectLift C ψ w =
214 { left := zcFreeGroupFoxDerivativeVector C ψ w
215 right := ψ w } := by
216 apply ZCCompletedFoxSemidirect.ext
217 · rw [← zcCompletedFoxSemidirectDerivativeVector_eq]
218 rfl
219 · exact zcCompletedFoxSemidirectLift_right C ψ w
221omit [DecidableEq X] in
222/-- The left component of a semidirect homomorphism with prescribed right component, bundled
223as a completed crossed homomorphism. -/
224def zcCompletedFoxSemidirectLiftLeftCrossedHom
225 (ψ : FreeGroup X →* H)
226 (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
227 (hright : ∀ w : FreeGroup X, (φ w).right = ψ w) :
228 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
229 (ZCFreeFoxCoordinates C (X := X) (H := H)) where
230 toFun w := (φ w).left
231 map_mul' u v := by
232 have h := congrArg ZCCompletedFoxSemidirect.left (map_mul φ u v)
233 change (φ (u * v)).left =
234 (φ u).left + zcCompletedGroupAlgebraScalar C ψ u • (φ v).left
235 rw [h]
236 simp only [ZCCompletedFoxSemidirect.mul_left, hright u,
237 zcCompletedGroupAlgebraScalar_apply]
239/-- Uniqueness of the completed semidirect lift with prescribed right component and generator
240coordinate values. -/
241theorem zcCompletedFoxSemidirectLift_unique
242 (ψ : FreeGroup X →* H)
243 (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
244 (hright : ∀ w : FreeGroup X, (φ w).right = ψ w)
245 (hbasis :
246 ∀ x : X, (φ (FreeGroup.of x)).left =
247 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
248 φ = zcCompletedFoxSemidirectLift C ψ := by
249 let delta :=
250 zcCompletedFoxSemidirectLiftLeftCrossedHom C ψ φ hright
251 have hdelta_eq : delta = zcFreeGroupFoxDerivativeVector C ψ :=
252 zcFreeGroupFoxDerivativeVector_unique C ψ delta hbasis
253 apply MonoidHom.ext
254 intro w
255 apply ZCCompletedFoxSemidirect.ext
256 · change delta w = zcCompletedFoxSemidirectDerivativeVector C ψ w
257 rw [hdelta_eq, zcCompletedFoxSemidirectDerivativeVector_eq]
258 · rw [hright w, zcCompletedFoxSemidirectLift_right]
260/-- Existence and uniqueness theorem for the completed semidirect lift. -/
261theorem existsUnique_zcCompletedFoxSemidirectLift
262 (ψ : FreeGroup X →* H) :
263 ∃! φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H,
264 (∀ w : FreeGroup X, (φ w).right = ψ w) ∧
265 ∀ x : X, (φ (FreeGroup.of x)).left =
266 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
267 refine ⟨zcCompletedFoxSemidirectLift C ψ, ?_, ?_⟩
268 · exact ⟨zcCompletedFoxSemidirectLift_right C ψ,
269 zcCompletedFoxSemidirectDerivativeVector_of C ψ⟩
270 · intro φ hφ
271 exact zcCompletedFoxSemidirectLift_unique C ψ φ hφ.1 hφ.2
273section FiniteBasis
275variable [Fintype X]
277/-- Boundary-map form of the completed Fox fundamental formula for the semidirect derivative
278vector. -/
279theorem zcCompletedFoxSemidirectDerivativeVector_foxBoundary
280 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
281 zcFreeGroupFoxBoundary C ψ (zcCompletedFoxSemidirectDerivativeVector C ψ w) =
282 zcCompletedGroupAlgebraBoundary C ψ w := by
283 exact zcFreeGroupFoxBoundary_of_crossedHom C ψ
284 (zcCompletedFoxSemidirectDerivativeVector C ψ)
285 (zcCompletedFoxSemidirectDerivativeVector_of C ψ) w
287/-- Completed Fox-Euler formula using the left component of the semidirect lift:
288`[ψ(w)] - 1 = ∑ i, φ(w)_i * ([ψ(x_i)] - 1)`. -/
289theorem zcCompletedFoxSemidirectLift_euler_formula
290 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
291 zcGroupLike C H (ψ w) - 1 =
292 ∑ i : X,
293 (zcCompletedFoxSemidirectLift C ψ w).left i *
294 (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
295 exact zcFreeGroupFoxDerivative_euler_formula_of_crossedHom C ψ
296 (zcCompletedFoxSemidirectDerivativeVector C ψ)
297 (zcCompletedFoxSemidirectDerivativeVector_of C ψ) w
299/-- Conditional semidirect Fox boundary formula. Any semidirect lift with right component `ψ`
300and standard generator coordinates satisfies the completed Fox boundary formula. -/
301theorem zcCompletedFoxSemidirectLift_foxBoundary_of_generatorValues
302 (ψ : FreeGroup X →* H)
303 (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
304 (hright : ∀ w : FreeGroup X, (φ w).right = ψ w)
305 (hbasis :
306 ∀ x : X, (φ (FreeGroup.of x)).left =
307 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
308 (w : FreeGroup X) :
309 zcFreeGroupFoxBoundary C ψ (φ w).left =
310 zcCompletedGroupAlgebraBoundary C ψ w := by
311 exact zcFreeGroupFoxBoundary_of_crossedHom C ψ
312 (zcCompletedFoxSemidirectLiftLeftCrossedHom C ψ φ hright)
313 hbasis w
315/-- Conditional semidirect Fox-Euler formula. The left component of any semidirect lift with
316right component `ψ` and standard generator coordinates gives the completed Fox-Euler sum. -/
317theorem zcCompletedFoxSemidirectLift_euler_formula_of_generatorValues
318 (ψ : FreeGroup X →* H)
319 (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
320 (hright : ∀ w : FreeGroup X, (φ w).right = ψ w)
321 (hbasis :
322 ∀ x : X, (φ (FreeGroup.of x)).left =
323 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
324 (w : FreeGroup X) :
325 zcGroupLike C H (ψ w) - 1 =
326 ∑ i : X,
327 (φ w).left i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
328 exact zcFreeGroupFoxDerivative_euler_formula_of_crossedHom C ψ
329 (zcCompletedFoxSemidirectLiftLeftCrossedHom C ψ φ hright)
330 hbasis w
332end FiniteBasis
334end Lift
336end
338end FoxDifferential