FoxDifferential/Common/CrossedDifferentialModule.lean
1import FoxDifferential.Common.CrossedDifferential
2import Mathlib.Algebra.MonoidAlgebra.Basic
3import Mathlib.LinearAlgebra.Finsupp.LinearCombination
4import Mathlib.LinearAlgebra.Quotient.Basic
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/FoxDifferential/Common/CrossedDifferentialModule.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Universal Fox calculus
17Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
18-/
19namespace FoxDifferential
21noncomputable section
23variable {R G : Type*} [Ring R] [Group G]
25/-- The free `R`-module on the underlying set of a group `G`. -/
26abbrev CrossedDifferentialPreModule (R G : Type*) [Ring R] : Type _ :=
27 G →₀ R
29/-- The universal crossed-differential relation
30`d(g₁g₂) = d(g₁) + coeff(g₁) • d(g₂)` in the free pre-module. -/
31def crossedDifferentialRelationElement (coeff : G →* R) (g₁ g₂ : G) :
32 CrossedDifferentialPreModule R G :=
33 Finsupp.single (g₁ * g₂) 1 -
34 (Finsupp.single g₁ 1 + coeff g₁ • Finsupp.single g₂ 1)
36/-- The submodule generated by all universal crossed-differential relations. -/
37def crossedDifferentialRelationSubmodule (coeff : G →* R) :
38 Submodule R (CrossedDifferentialPreModule R G) :=
39 Submodule.span R (Set.range fun p : G × G =>
40 crossedDifferentialRelationElement coeff p.1 p.2)
42/-- The universal module representing crossed differentials with coefficient homomorphism
43`coeff : G ->* R`. -/
44abbrev CrossedDifferentialModule (coeff : G →* R) : Type _ :=
47/-- The universal crossed differential `d_coeff : G -> CrossedDifferentialModule coeff`. -/
48def universalCrossedDifferential (coeff : G →* R) (g : G) :
49 CrossedDifferentialModule coeff :=
50 (crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g 1)
52/-- Every defining crossed-differential relation belongs to the relation submodule. -/
53theorem crossedDifferentialRelationElement_mem (coeff : G →* R) (g₁ g₂ : G) :
54 crossedDifferentialRelationElement coeff g₁ g₂ ∈
55 crossedDifferentialRelationSubmodule coeff := by
56 exact Submodule.subset_span ⟨(g₁, g₂), rfl⟩
58/-- The universal crossed differential satisfies the crossed product rule. -/
59theorem universalCrossedDifferential_mul (coeff : G →* R) (g₁ g₂ : G) :
60 universalCrossedDifferential coeff (g₁ * g₂) =
61 universalCrossedDifferential coeff g₁ +
62 coeff g₁ • universalCrossedDifferential coeff g₂ := by
63 have hzero :
64 (crossedDifferentialRelationSubmodule coeff).mkQ
65 (crossedDifferentialRelationElement coeff g₁ g₂) = 0 := by
66 exact
67 (Submodule.Quotient.mk_eq_zero
68 (p := crossedDifferentialRelationSubmodule coeff)
69 (x := crossedDifferentialRelationElement coeff g₁ g₂)).2
70 (crossedDifferentialRelationElement_mem coeff g₁ g₂)
71 have hzero' :
72 universalCrossedDifferential coeff (g₁ * g₂) -
73 (universalCrossedDifferential coeff g₁ +
74 (crossedDifferentialRelationSubmodule coeff).mkQ
75 (coeff g₁ • Finsupp.single g₂ 1)) = 0 := by
76 simpa [universalCrossedDifferential, crossedDifferentialRelationElement] using hzero
77 have hsmul :
78 (crossedDifferentialRelationSubmodule coeff).mkQ
79 (coeff g₁ • Finsupp.single g₂ 1) =
80 coeff g₁ • universalCrossedDifferential coeff g₂ := by
81 simpa [universalCrossedDifferential, Submodule.mkQ_apply] using
82 (Submodule.Quotient.mk_smul (p := crossedDifferentialRelationSubmodule coeff)
83 (r := coeff g₁) (x := Finsupp.single g₂ 1))
84 have hzero'' :
85 universalCrossedDifferential coeff (g₁ * g₂) -
86 (universalCrossedDifferential coeff g₁ +
87 coeff g₁ • universalCrossedDifferential coeff g₂) = 0 := by
88 rw [hsmul] at hzero'
89 exact hzero'
90 exact sub_eq_zero.mp hzero''
92/-- The universal crossed differential vanishes at the identity. -/
93@[simp]
94theorem universalCrossedDifferential_one (coeff : G →* R) :
95 universalCrossedDifferential coeff (1 : G) = 0 := by
96 have h := universalCrossedDifferential_mul coeff (1 : G) (1 : G)
98 have h' := congrArg
99 (fun z : CrossedDifferentialModule coeff => z - universalCrossedDifferential coeff (1 : G))
100 h
101 have hzero : 0 = universalCrossedDifferential coeff (1 : G) := by
102 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
103 simpa using hzero.symm
105/-- The universal crossed differential is itself a crossed differential. -/
106theorem universalCrossedDifferential_isCrossedDifferential (coeff : G →* R) :
107 IsCrossedDifferential coeff (universalCrossedDifferential coeff) := by
108 intro g₁ g₂
109 exact universalCrossedDifferential_mul coeff g₁ g₂
111section UniversalProperty
113variable {A : Type*} [AddCommGroup A] [Module R A]
115/-- The linear extension of a map out of `G` to the free crossed-differential pre-module. -/
116def crossedDifferentialModuleLiftLinear (delta : G → A) :
117 CrossedDifferentialPreModule R G →ₗ[R] A :=
118 Finsupp.linearCombination R delta
120omit [Group G] in
121/-- The linear extension of a map evaluates on a single basis vector by scalar multiplication. -/
122@[simp]
123theorem crossedDifferentialModuleLiftLinear_single (delta : G → A) (g : G) (r : R) :
124 crossedDifferentialModuleLiftLinear (R := R) delta (Finsupp.single g r) = r • delta g := by
125 simp only [crossedDifferentialModuleLiftLinear, Finsupp.linearCombination_single]
127/-- A crossed differential kills each defining universal relation. -/
129 (coeff : G →* R) (delta : G → A)
130 (hdelta : IsCrossedDifferential coeff delta) (g₁ g₂ : G) :
131 crossedDifferentialModuleLiftLinear (R := R) delta
132 (crossedDifferentialRelationElement coeff g₁ g₂) = 0 := by
133 simp only [crossedDifferentialModuleLiftLinear, crossedDifferentialRelationElement, Finsupp.smul_single,
134 smul_eq_mul, mul_one, map_sub, Finsupp.linearCombination_single, hdelta g₁ g₂, smul_add, one_smul, map_add,
135 sub_self]
137/-- The relation submodule is contained in the kernel of the linear extension of a crossed
138differential. -/
140 (coeff : G →* R) (delta : G → A)
141 (hdelta : IsCrossedDifferential coeff delta) :
143 LinearMap.ker (crossedDifferentialModuleLiftLinear (R := R) delta) := by
144 refine Submodule.span_le.2 ?_
145 rintro _ ⟨⟨g₁, g₂⟩, rfl⟩
146 simpa [LinearMap.mem_ker] using
148 (A := A) coeff delta hdelta g₁ g₂
150/-- The universal linear map induced by a crossed differential. -/
152 (coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta) :
153 CrossedDifferentialModule coeff →ₗ[R] A :=
154 (crossedDifferentialRelationSubmodule coeff).liftQ
155 (crossedDifferentialModuleLiftLinear (R := R) delta)
156 (crossedDifferentialRelationSubmodule_le_ker (A := A) coeff delta hdelta)
158/-- The universal lift evaluated on a quotient representative is the finite linear combination of
159the prescribed crossed differential on that representative. -/
161 (coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta)
162 (x : CrossedDifferentialPreModule R G) :
163 crossedDifferentialModuleLift (A := A) coeff delta hdelta
164 ((crossedDifferentialRelationSubmodule coeff).mkQ x) =
165 crossedDifferentialModuleLiftLinear (R := R) delta x := by
166 rw [crossedDifferentialModuleLift, Submodule.mkQ_apply, Submodule.liftQ_apply]
168/-- The universal lift evaluates on `d_coeff g` as the original crossed differential. -/
170 (coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta) (g : G) :
171 crossedDifferentialModuleLift (A := A) coeff delta hdelta
172 (universalCrossedDifferential coeff g) = delta g := by
173 change
174 (crossedDifferentialRelationSubmodule coeff).liftQ
175 (crossedDifferentialModuleLiftLinear (R := R) delta)
176 (crossedDifferentialRelationSubmodule_le_ker (A := A) coeff delta hdelta)
177 ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g 1)) =
178 delta g
179 rw [Submodule.mkQ_apply, Submodule.liftQ_apply]
180 simp only [crossedDifferentialModuleLiftLinear_single, one_smul]
182/-- Linear maps out of the universal crossed-differential module are equal when they agree on all
183universal differentials. -/
184@[ext]
186 (coeff : G →* R) {f h : CrossedDifferentialModule coeff →ₗ[R] A}
187 (hfh : ∀ g, f (universalCrossedDifferential coeff g) =
188 h (universalCrossedDifferential coeff g)) :
189 f = h := by
190 apply Submodule.linearMap_qext _
191 apply Finsupp.lhom_ext
192 intro g r
193 have hsingle :
194 ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g r) :
195 CrossedDifferentialModule coeff) =
196 r • universalCrossedDifferential coeff g := by
197 rw [← Finsupp.smul_single_one]
198 rfl
199 change f ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g r)) =
200 h ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g r))
203/-- The universal lift is the unique linear map with prescribed values on universal
204differentials. -/
206 (coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta)
207 (f : CrossedDifferentialModule coeff →ₗ[R] A)
208 (hf : ∀ g, f (universalCrossedDifferential coeff g) = delta g) :
209 f = crossedDifferentialModuleLift (A := A) coeff delta hdelta := by
210 apply crossedDifferentialModuleHom_ext coeff
211 intro g
212 rw [hf g, crossedDifferentialModuleLift_universal]
214/-- Existence and uniqueness of the linear map representing a crossed differential. -/
216 (coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta) :
217 ∃! f : CrossedDifferentialModule coeff →ₗ[R] A,
218 ∀ g, f (universalCrossedDifferential coeff g) = delta g := by
219 refine ⟨crossedDifferentialModuleLift (A := A) coeff delta hdelta, ?_, ?_⟩
220 · intro g
221 exact crossedDifferentialModuleLift_universal (A := A) coeff delta hdelta g
222 · intro f hf
223 exact crossedDifferentialModuleLift_unique (A := A) coeff delta hdelta f hf
225/-- The crossed differential induced by a linear map out of the universal module. -/
227 (coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) : G → A :=
228 fun g => f (universalCrossedDifferential coeff g)
230/-- A linear map out of the universal module induces a crossed differential. -/
232 (coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) :
233 IsCrossedDifferential coeff (crossedDifferentialOfModuleLinearMap (A := A) coeff f) := by
234 intro g₁ g₂
235 change
236 f (universalCrossedDifferential coeff (g₁ * g₂)) =
237 f (universalCrossedDifferential coeff g₁) +
238 coeff g₁ • f (universalCrossedDifferential coeff g₂)
242/-- Universal representation theorem for crossed differentials with arbitrary coefficient ring.
244Crossed differentials `G -> A` with coefficient homomorphism `coeff : G ->* R` are equivalent to
245`R`-linear maps out of the universal module `CrossedDifferentialModule coeff`. -/
246def crossedDifferentialModuleEquivLinearMap (coeff : G →* R) :
247 {delta : G → A // IsCrossedDifferential coeff delta} ≃
248 (CrossedDifferentialModule coeff →ₗ[R] A) where
249 toFun delta := crossedDifferentialModuleLift (A := A) coeff delta.1 delta.2
250 invFun f :=
251 ⟨crossedDifferentialOfModuleLinearMap (A := A) coeff f,
252 crossedDifferentialOfModuleLinearMap_isCrossedDifferential (A := A) coeff f⟩
253 left_inv delta := by
254 apply Subtype.ext
255 funext g
256 exact crossedDifferentialModuleLift_universal (A := A) coeff delta.1 delta.2 g
257 right_inv f := by
258 apply crossedDifferentialModuleHom_ext coeff
259 intro g
260 exact crossedDifferentialModuleLift_universal (A := A) coeff
261 (crossedDifferentialOfModuleLinearMap (A := A) coeff f)
262 (crossedDifferentialOfModuleLinearMap_isCrossedDifferential (A := A) coeff f) g
264end UniversalProperty
266section MonoidAlgebraIdentityBoundary
268variable {S : Type*} [CommRing S]
270/-- The `S`-linear map from a group algebra to the identity crossed-differential module sending
271`[g]` to the universal differential `d g`. -/
273 MonoidAlgebra S G →ₗ[S]
274 CrossedDifferentialModule (MonoidAlgebra.of S G) :=
275 Finsupp.linearCombination S
276 (fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g)
279 (a : MonoidAlgebra S G) (g : G) :
281 (a * (MonoidAlgebra.of S G g - 1)) =
282 a • universalCrossedDifferential (MonoidAlgebra.of S G) g := by
285 · intro a b ha hb
287 · intro p c
288 rw [MonoidAlgebra.of_apply]
289 rw [mul_sub, mul_one, MonoidAlgebra.single_mul_single]
290 change
292 (Finsupp.single (p * g) (c * 1) - Finsupp.single p c) =
293 (MonoidAlgebra.single p c : MonoidAlgebra S G) •
294 universalCrossedDifferential (MonoidAlgebra.of S G) g
295 rw [map_sub]
296 change
297 (Finsupp.linearCombination S
298 (fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g))
299 (Finsupp.single (p * g) (c * 1)) -
300 (Finsupp.linearCombination S
301 (fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g))
302 (Finsupp.single p c) =
303 (MonoidAlgebra.single p c : MonoidAlgebra S G) •
304 universalCrossedDifferential (MonoidAlgebra.of S G) g
305 rw [Finsupp.linearCombination_single, Finsupp.linearCombination_single]
306 simp only [mul_one]
308 rw [smul_add, add_sub_cancel_left]
309 rw [MonoidAlgebra.of_apply]
310 rw [show (MonoidAlgebra.single p c : MonoidAlgebra S G) =
311 c • MonoidAlgebra.single p 1 by
312 simp only [MonoidAlgebra.smul_single, smul_eq_mul, mul_one]]
313 exact (smul_assoc c (MonoidAlgebra.single p 1 : MonoidAlgebra S G)
314 (universalCrossedDifferential (MonoidAlgebra.of S G) g)).symm
316/-- The identity crossed-differential boundary `d g ↦ [g] - 1` over a group algebra. -/
318 CrossedDifferentialModule (MonoidAlgebra.of S G) →ₗ[MonoidAlgebra S G]
319 MonoidAlgebra S G :=
321 (A := MonoidAlgebra S G)
322 (MonoidAlgebra.of S G)
323 (fun g : G => MonoidAlgebra.of S G g - 1)
324 (by
325 intro g h
326 simp only [map_mul, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one, sub_eq_add_neg,
327 smul_eq_mul, mul_add, mul_neg, add_comm, add_assoc, neg_add_cancel_left])
329@[simp]
330theorem identityCrossedDifferentialBoundary_universal (g : G) :
332 (universalCrossedDifferential (MonoidAlgebra.of S G) g) =
333 MonoidAlgebra.of S G g - 1 := by
337 (x : CrossedDifferentialPreModule (MonoidAlgebra S G) G) :
340 (R := MonoidAlgebra S G)
341 (fun g : G => MonoidAlgebra.of S G g - 1) x) =
342 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x := by
344 · simp only [crossedDifferentialModuleLiftLinear, MonoidAlgebra.of_apply, map_zero]
345 · intro x y hx hy
347 exact congrArg₂ (· + ·)
348 (by simpa [MonoidAlgebra.of_apply] using hx)
349 (by simpa [MonoidAlgebra.of_apply] using hy)
350 · intro g a
352 change
354 (a * (MonoidAlgebra.of S G g - 1)) =
355 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ
356 (Finsupp.single g a)
358 rw [← Finsupp.smul_single_one]
359 exact
360 (Submodule.Quotient.mk_smul
361 (p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G))
362 (r := a) (x := Finsupp.single g 1)).symm
364/-- The boundary of the additive lift `∑ a_g [g] ↦ ∑ a_g d g` is the augmentation-zero
365part of the group-algebra element. -/
367 (a : MonoidAlgebra S G) :
369 (monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) a) =
370 a -
371 MonoidAlgebra.single (1 : G)
372 ((MonoidAlgebra.lift S S G (1 : G →* S)) a) := by
374 · simp only [monoidAlgebraToIdentityCrossedDifferentialModule, map_zero, Finsupp.single_zero, sub_self]
375 · intro x y hx hy
376 rw [show
377 monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) (x + y) =
381 rw [show
390 rw [hx, hy]
391 have haug :
392 ((MonoidAlgebra.lift S S G (1 : G →* S)) (x + y : MonoidAlgebra S G)) =
393 ((MonoidAlgebra.lift S S G (1 : G →* S)) x) +
394 ((MonoidAlgebra.lift S S G (1 : G →* S)) y) := by
396 rw [haug]
397 simp only [sub_eq_add_neg, add_left_comm, add_assoc, Finsupp.single_add, neg_add_rev, add_comm]
398 · intro g c
400 have hlin :
401 (Finsupp.linearCombination S
402 (fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g))
403 (Finsupp.single g c) =
404 c • universalCrossedDifferential (MonoidAlgebra.of S G) g := by
405 exact Finsupp.linearCombination_single
406 (R := S)
407 (v := fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g)
408 (c := c) (a := g)
409 calc
411 ((Finsupp.linearCombination S
412 (fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g))
413 (Finsupp.single g c)) =
415 (c • universalCrossedDifferential (MonoidAlgebra.of S G) g) := by
416 exact congrArg identityCrossedDifferentialBoundary hlin
417 _ =
418 (MonoidAlgebra.single g c : MonoidAlgebra S G) -
419 MonoidAlgebra.single (1 : G)
420 ((MonoidAlgebra.lift S S G (1 : G →* S))
421 (Finsupp.single g c : MonoidAlgebra S G)) := by
422 rw [LinearMap.map_smul_of_tower,
424 rw [Algebra.smul_def, MonoidAlgebra.of_apply]
425 rw [show (algebraMap S (MonoidAlgebra S G)) c =
426 MonoidAlgebra.single (1 : G) c by rfl]
427 rw [mul_sub, mul_one, MonoidAlgebra.single_mul_single]
428 simp only [MonoidAlgebra.single, one_mul, mul_one, MonoidAlgebra.lift_single, MonoidHom.one_apply,
429 smul_eq_mul]
431/-- On the augmentation ideal, the additive lift `∑ a_g [g] ↦ ∑ a_g d g` is a right inverse
432to the identity crossed-differential boundary. -/
434 {a : MonoidAlgebra S G}
435 (ha : (MonoidAlgebra.lift S S G (1 : G →* S)) a = 0) :
437 (monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) a) = a := by
439 ha]
440 simp only [Finsupp.single_zero, sub_zero]
442/-- For the identity coefficient map into a group algebra, the boundary map `d g ↦ [g] - 1`
443is injective. -/
445 Function.Injective (identityCrossedDifferentialBoundary (S := S) (G := G)) := by
446 intro x y hxy
447 revert y
448 refine Submodule.Quotient.induction_on
449 (p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)) x ?_
450 intro x y hxy'
451 revert hxy'
452 refine Submodule.Quotient.induction_on
453 (p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)) y ?_
454 intro y hxy'
455 apply (Submodule.Quotient.eq
456 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G))).2
457 have hdiff :
459 (R := MonoidAlgebra S G)
460 (fun g : G => MonoidAlgebra.of S G g - 1) (x - y) = 0 := by
461 have hboundary :
463 ((crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ (x - y)) =
464 0 := by
465 rw [show
466 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ (x - y) =
467 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x -
468 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ y by
469 rw [map_sub]]
470 rw [map_sub]
471 have hxy'' :
473 ((crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x) =
475 ((crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ y) := by
476 simpa [Submodule.mkQ_apply] using hxy'
477 rw [hxy'', sub_self]
479 using hboundary
480 have hmk :
481 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ (x - y) =
482 0 := by
483 have happ :=
485 (S := S) (G := G) (x - y)
487 exact happ.symm
488 exact
489 (Submodule.Quotient.mk_eq_zero
490 (p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G))
491 (x := x - y)).1 hmk
493end MonoidAlgebraIdentityBoundary
495end
497end FoxDifferential