FoxDifferential/Completed/Semidirect.lean
1import FoxDifferential.Completed.ProCIntegerCoefficients.Core
2import FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Semidirect.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 Fox semidirect products
15Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
16-/
17namespace FoxDifferential
19noncomputable section
21open scoped BigOperators
23universe u v
25variable (C : ProCGroups.FiniteGroupClass.{v})
26variable (X : Type u) [DecidableEq X]
27variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29omit [DecidableEq X] in
30/-- The completed Fox semidirect target `Z_C[[H]]^X ⋊ H`. -/
31structure ZCCompletedFoxSemidirect where
32 /-- The completed Fox-coordinate component. -/
33 left : ZCFreeFoxCoordinates C (X := X) (H := H)
34 /-- The target group component. -/
35 right : H
37namespace ZCCompletedFoxSemidirect
39omit [DecidableEq X] in
40/-- Extensionality for completed Fox semidirect elements. -/
41@[ext]
42theorem ext {a b : ZCCompletedFoxSemidirect C X H}
43 (hleft : a.left = b.left) (hright : a.right = b.right) : a = b := by
44 cases a
45 cases b
46 simp_all
48/-- Identity element of the completed Fox semidirect product. -/
49instance instOneZCCompletedFoxSemidirect : One (ZCCompletedFoxSemidirect C X H) where
52/-- Multiplication in the completed Fox semidirect product. -/
53instance instMulZCCompletedFoxSemidirect : Mul (ZCCompletedFoxSemidirect C X H) where
54 mul a b :=
55 ⟨a.left + zcGroupLike C H a.right • b.left, a.right * b.right⟩
57/-- Inversion in the completed Fox semidirect product. -/
58instance instInvZCCompletedFoxSemidirect : Inv (ZCCompletedFoxSemidirect C X H) where
59 inv a :=
60 ⟨-(zcGroupLike C H a.right⁻¹ • a.left), a.right⁻¹⟩
62omit [DecidableEq X] in
63/-- The left component of the identity semidirect element is zero. -/
64@[simp]
65theorem one_left :
66 (1 : ZCCompletedFoxSemidirect C X H).left = 0 :=
67 rfl
69omit [DecidableEq X] in
70/-- The right component of the identity semidirect element is the group identity. -/
71@[simp]
72theorem one_right :
73 (1 : ZCCompletedFoxSemidirect C X H).right = 1 :=
74 rfl
76omit [DecidableEq X] in
77/-- The left component of semidirect multiplication. -/
78@[simp]
79theorem mul_left (a b : ZCCompletedFoxSemidirect C X H) :
80 (a * b).left = a.left + zcGroupLike C H a.right • b.left :=
81 rfl
83omit [DecidableEq X] in
84/-- The right component of semidirect multiplication. -/
85@[simp]
86theorem mul_right (a b : ZCCompletedFoxSemidirect C X H) :
87 (a * b).right = a.right * b.right :=
88 rfl
90omit [DecidableEq X] in
91/-- The left component of semidirect inversion. -/
92@[simp]
93theorem inv_left (a : ZCCompletedFoxSemidirect C X H) :
94 a⁻¹.left = -(zcGroupLike C H a.right⁻¹ • a.left) :=
95 rfl
97omit [DecidableEq X] in
98/-- The right component of semidirect inversion. -/
99@[simp]
100theorem inv_right (a : ZCCompletedFoxSemidirect C X H) :
101 a⁻¹.right = a.right⁻¹ :=
102 rfl
104/-- Group structure on the completed Fox semidirect product. -/
105instance instGroupZCCompletedFoxSemidirect : Group (ZCCompletedFoxSemidirect C X H) where
107 mul := (· * ·)
108 inv := Inv.inv
109 mul_assoc a b c := by
110 ext
113 zcCompletedGroupAlgebraProjection_groupLike, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one,
114 MonoidAlgebra.coe_add, MonoidAlgebra.single_mul_apply, one_mul, mul_inv_rev, smul_add, smul_smul]
115 · simp only [mul_right, mul_assoc]
116 one_mul a := by
117 ext
118 · simp only [mul_left, one_left, one_right, map_one, one_smul, Pi.add_apply, Pi.zero_apply, zero_add]
119 · simp only [mul_right, one_right, one_mul]
120 mul_one a := by
121 ext
122 · simp only [mul_left, one_left, smul_zero, Pi.add_apply, Pi.zero_apply, add_zero]
123 · simp only [mul_right, one_right, mul_one]
124 inv_mul_cancel a := by
125 ext
126 · simp only [mul_left, inv_left, inv_right, Pi.add_apply, Pi.neg_apply, Pi.smul_apply, smul_eq_mul,
127 neg_add_cancel, zcCompletedGroupAlgebraProjection_zero, Finsupp.coe_zero, Pi.zero_apply, one_left]
128 · simp only [mul_right, inv_right, inv_mul_cancel, one_right]
130omit [DecidableEq X] in
131/-- The right projection from the completed Fox semidirect product to the target group. -/
132def rightMonoidHom : ZCCompletedFoxSemidirect C X H →* H where
133 toFun a := a.right
134 map_one' := rfl
135 map_mul' _ _ := rfl
137omit [DecidableEq X] in
138@[simp]
139theorem rightMonoidHom_apply (a : ZCCompletedFoxSemidirect C X H) :
140 rightMonoidHom C X H a = a.right :=
141 rfl
145section Lift
147variable {X H}
149/-- The completed Fox semidirect lift of a free group homomorphism. -/
150def zcCompletedFoxSemidirectLift (ψ : FreeGroup X →* H) :
151 FreeGroup X →* ZCCompletedFoxSemidirect C X H :=
152 FreeGroup.lift fun x =>
153 { left := Pi.single x (1 : ZCCompletedGroupAlgebra C H)
154 right := ψ (FreeGroup.of x) }
156/-- The right component of the completed Fox semidirect lift is `ψ`. -/
157@[simp]
159 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
160 (zcCompletedFoxSemidirectLift C ψ w).right = ψ w := by
161 induction w using FreeGroup.induction_on with
162 | C1 =>
163 simp only [zcCompletedFoxSemidirectLift, map_one, ZCCompletedFoxSemidirect.one_right]
164 | of x =>
165 simp only [zcCompletedFoxSemidirectLift, FreeGroup.lift_apply_of]
166 | inv_of x hx =>
167 simpa using congrArg Inv.inv hx
168 | mul u v hu hv =>
171/-- The left component of the completed Fox semidirect lift. -/
173 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
174 ZCFreeFoxCoordinates C (X := X) (H := H) :=
175 (zcCompletedFoxSemidirectLift C ψ w).left
177/-- The completed semidirect derivative vector sends the identity word to zero. -/
178@[simp]
180 (ψ : FreeGroup X →* H) :
181 zcCompletedFoxSemidirectDerivativeVector C ψ (1 : FreeGroup X) = 0 := by
183 ZCCompletedFoxSemidirect.one_left]
185/-- The completed semidirect derivative vector sends a free generator to the coordinate basis
186vector. -/
187@[simp]
189 (ψ : FreeGroup X →* H) (x : X) :
190 zcCompletedFoxSemidirectDerivativeVector C ψ (FreeGroup.of x) =
191 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
192 simp only [zcCompletedFoxSemidirectDerivativeVector, zcCompletedFoxSemidirectLift, FreeGroup.lift_apply_of]
194/-- Product rule for the completed semidirect derivative vector. -/
196 (ψ : FreeGroup X →* H) (u v : FreeGroup X) :
197 zcCompletedFoxSemidirectDerivativeVector C ψ (u * v) =
199 zcCompletedGroupAlgebraScalar C ψ u •
200 zcCompletedFoxSemidirectDerivativeVector C ψ v := by
201 simp only [zcCompletedFoxSemidirectDerivativeVector, map_mul, ZCCompletedFoxSemidirect.mul_left,
204/-- The left component of the completed semidirect lift is a crossed differential. -/
206 (ψ : FreeGroup X →* H) :
209 (zcCompletedFoxSemidirectDerivativeVector C ψ) := by
210 intro u v
211 exact zcCompletedFoxSemidirectDerivativeVector_mul C ψ u v
213/-- The completed semidirect derivative vector is the completed free-group Fox derivative
214vector. -/
216 (ψ : FreeGroup X →* H) :
218 zcFreeGroupFoxDerivativeVector C ψ := by
219 exact zcFreeGroupFoxDerivativeVector_unique C ψ
224/-- The completed semidirect lift stores the completed Fox derivative vector and the target
225homomorphism. -/
227 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
228 zcCompletedFoxSemidirectLift C ψ w =
229 { left := zcFreeGroupFoxDerivativeVector C ψ w
230 right := ψ w } := by
231 apply ZCCompletedFoxSemidirect.ext
233 rfl
234 · exact zcCompletedFoxSemidirectLift_right C ψ w
236/-- Uniqueness of the completed semidirect lift with prescribed right component and generator
237coordinate values. -/
239 (ψ : FreeGroup X →* H)
240 (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
241 (hright : ∀ w : FreeGroup X, (φ w).right = ψ w)
242 (hbasis :
243 ∀ x : X, (φ (FreeGroup.of x)).left =
244 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
245 φ = zcCompletedFoxSemidirectLift C ψ := by
246 let delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H) :=
247 fun w => (φ w).left
248 have hdelta :
249 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta := by
250 intro u v
252 change (φ (u * v)).left =
253 (φ u).left + zcCompletedGroupAlgebraScalar C ψ u • (φ v).left
254 rw [h]
255 simp only [ZCCompletedFoxSemidirect.mul_left, hright u, zcCompletedGroupAlgebraScalar_apply]
256 have hdelta_eq : delta = zcFreeGroupFoxDerivativeVector C ψ :=
257 zcFreeGroupFoxDerivativeVector_unique C ψ delta hdelta hbasis
258 apply MonoidHom.ext
259 intro w
260 apply ZCCompletedFoxSemidirect.ext
261 · change delta w = zcCompletedFoxSemidirectDerivativeVector C ψ w
262 rw [hdelta_eq, zcCompletedFoxSemidirectDerivativeVector_eq]
263 · rw [hright w, zcCompletedFoxSemidirectLift_right]
265omit [DecidableEq X] in
266/-- The left component of any semidirect lift with prescribed right component is a completed
267crossed differential. -/
269 (ψ : FreeGroup X →* H)
270 (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
271 (hright : ∀ w : FreeGroup X, (φ w).right = ψ w) :
273 (zcCompletedGroupAlgebraScalar C ψ) (fun w : FreeGroup X => (φ w).left) := by
274 intro u v
276 change (φ (u * v)).left =
277 (φ u).left + zcCompletedGroupAlgebraScalar C ψ u • (φ v).left
278 rw [h]
279 simp only [ZCCompletedFoxSemidirect.mul_left, hright u, zcCompletedGroupAlgebraScalar_apply]
281/-- Existence and uniqueness theorem for the completed semidirect lift. -/
283 (ψ : FreeGroup X →* H) :
284 ∃! φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H,
285 (∀ w : FreeGroup X, (φ w).right = ψ w) ∧
286 ∀ x : X, (φ (FreeGroup.of x)).left =
287 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
288 refine ⟨zcCompletedFoxSemidirectLift C ψ, ?_, ?_⟩
289 · exact ⟨zcCompletedFoxSemidirectLift_right C ψ,
291 · intro φ hφ
292 exact zcCompletedFoxSemidirectLift_unique C ψ φ hφ.1 hφ.2
294section FiniteBasis
296variable [Fintype X]
298/-- Boundary-map form of the completed Fox fundamental formula for the semidirect derivative
299vector. -/
301 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
303 zcCompletedGroupAlgebraBoundary C ψ w := by
309/-- Completed Fox-Euler formula using the left component of the semidirect lift:
310`[ψ(w)] - 1 = ∑ i, φ(w)_i * ([ψ(x_i)] - 1)`. -/
312 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
313 zcGroupLike C H (ψ w) - 1 =
314 ∑ i : X,
315 (zcCompletedFoxSemidirectLift C ψ w).left i *
316 (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
322/-- Conditional semidirect Fox boundary formula. Any semidirect lift with right component `ψ`
325 (ψ : FreeGroup X →* H)
326 (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
327 (hright : ∀ w : FreeGroup X, (φ w).right = ψ w)
328 (hbasis :
329 ∀ x : X, (φ (FreeGroup.of x)).left =
330 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
331 (w : FreeGroup X) :
332 zcFreeGroupFoxBoundary C ψ (φ w).left =
333 zcCompletedGroupAlgebraBoundary C ψ w := by
335 (fun w : FreeGroup X => (φ w).left)
336 (zcCompletedFoxSemidirectLift_left_isCrossedDifferential C ψ φ hright)
337 hbasis w
339/-- Conditional semidirect Fox-Euler formula. The left component of any semidirect lift with
342 (ψ : FreeGroup X →* H)
343 (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
344 (hright : ∀ w : FreeGroup X, (φ w).right = ψ w)
345 (hbasis :
346 ∀ x : X, (φ (FreeGroup.of x)).left =
347 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
348 (w : FreeGroup X) :
349 zcGroupLike C H (ψ w) - 1 =
350 ∑ i : X,
351 (φ w).left i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
353 (fun w : FreeGroup X => (φ w).left)
354 (zcCompletedFoxSemidirectLift_left_isCrossedDifferential C ψ φ hright)
355 hbasis w
357end FiniteBasis
359end Lift
361end
363end FoxDifferential