Yamaguchi Lean 4 Library
FoxDifferential/Common/CrossedDifferential.lean
FoxDifferential/Common/CrossedDifferential/Source

FoxDifferential/Common/CrossedDifferential.lean

1import Mathlib.Algebra.Group.Commutator
2import Mathlib.Algebra.Group.Subgroup.Lattice
3import Mathlib.Algebra.Module.BigOperators
4import Mathlib.Algebra.Module.LinearMap.Basic
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/FoxDifferential/Common/CrossedDifferential.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
21open scoped BigOperators
23/-- A crossed differential with coefficient homomorphism `coeff : G ->* R`.
25The rule is the Fox Leibniz rule
26`delta (g * h) = delta g + coeff g • delta h`. -/
28 {R G A : Type*} [Semiring R] [Group G] [AddCommMonoid A] [Module R A]
29 (coeff : G →* R) (delta : G → A) : Prop :=
30 ∀ g h, delta (g * h) = delta g + coeff g • delta h
34variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
35variable {coeff : G →* R} {delta : G → A}
37/-- The zero map is a crossed differential. -/
38theorem zero :
39 IsCrossedDifferential coeff (fun _ : G => (0 : A)) := by
40 intro g h
41 simp only [smul_zero, add_zero]
43/-- Crossed differentials with the same coefficient homomorphism are closed under addition. -/
44theorem add {delta epsilon : G → A}
45 (hdelta : IsCrossedDifferential coeff delta)
46 (hepsilon : IsCrossedDifferential coeff epsilon) :
47 IsCrossedDifferential coeff (fun g => delta g + epsilon g) := by
48 intro g h
49 change delta (g * h) + epsilon (g * h) =
50 delta g + epsilon g + coeff g • (delta h + epsilon h)
51 rw [hdelta g h, hepsilon g h]
52 simp only [add_left_comm, add_assoc, smul_add]
54/-- Crossed differentials are closed under negation. -/
55theorem neg (hdelta : IsCrossedDifferential coeff delta) :
56 IsCrossedDifferential coeff (fun g => -delta g) := by
57 intro g h
58 change -delta (g * h) = -delta g + coeff g • -delta h
59 rw [hdelta g h]
60 simp only [neg_add_rev, add_comm, smul_neg]
62/-- Crossed differentials with the same coefficient homomorphism are closed under subtraction. -/
63theorem sub {delta epsilon : G → A}
64 (hdelta : IsCrossedDifferential coeff delta)
65 (hepsilon : IsCrossedDifferential coeff epsilon) :
66 IsCrossedDifferential coeff (fun g => delta g - epsilon g) := by
67 simpa [sub_eq_add_neg] using add hdelta (neg hepsilon)
69/-- A linear map sends crossed differentials to crossed differentials. -/
70theorem map_linear {B : Type*} [AddCommGroup B] [Module R B]
71 (hdelta : IsCrossedDifferential coeff delta) (f : A →ₗ[R] B) :
72 IsCrossedDifferential coeff (fun g => f (delta g)) := by
73 intro g h
74 change f (delta (g * h)) = f (delta g) + coeff g • f (delta h)
75 rw [hdelta g h]
76 simp only [map_add, map_smul]
78/-- Pulling a crossed differential back along a group homomorphism is a crossed differential. -/
79theorem comp_monoidHom {K : Type*} [Group K]
80 (hdelta : IsCrossedDifferential coeff delta) (φ : K →* G) :
81 IsCrossedDifferential (coeff.comp φ) (fun k : K => delta (φ k)) := by
82 intro g h
83 simpa [MonoidHom.comp_apply, map_mul] using hdelta (φ g) (φ h)
85/-- Restricting a crossed differential to any subgroup on which the coefficient homomorphism is
86trivial gives an ordinary additive homomorphism. -/
88 (hdelta : IsCrossedDifferential coeff delta) (N : Subgroup G)
89 (hN : ∀ n : N, coeff n = 1) :
90 Additive N →+ A where
91 toFun x := delta ((Additive.toMul x : N) : G)
92 map_zero' := by
93 change delta (1 : G) = 0
94 have h := hdelta 1 1
95 rw [map_one, one_smul] at h
96 have h' := congrArg (fun z : A => z - delta 1) h
97 have hzero : 0 = delta 1 := by
98 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
99 simpa using hzero.symm
100 map_add' x y := by
101 change delta (((Additive.toMul x : N) * (Additive.toMul y : N) : N) : G) =
102 delta ((Additive.toMul x : N) : G) + delta ((Additive.toMul y : N) : G)
103 have h :=
104 hdelta ((Additive.toMul x : N) : G) ((Additive.toMul y : N) : G)
105 simpa [hN (Additive.toMul x)] using h
107@[simp]
109 (hdelta : IsCrossedDifferential coeff delta) (N : Subgroup G)
110 (hN : ∀ n : N, coeff n = 1) (g : N) :
111 restrictTrivialSubgroupAddMonoidHom hdelta N hN (Additive.ofMul g) = delta g :=
112 rfl
114/-- A crossed differential vanishes at the identity. -/
115theorem one (hdelta : IsCrossedDifferential coeff delta) :
116 delta 1 = 0 := by
117 have h := hdelta 1 1
118 rw [map_one, one_smul] at h
119 have h' := congrArg (fun z : A => z - delta 1) h
120 have hzero : 0 = delta 1 := by
121 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
122 simpa using hzero.symm
124/-- Inverse rule for a crossed differential. -/
125theorem inv (hdelta : IsCrossedDifferential coeff delta) (g : G) :
126 delta g⁻¹ = -(coeff g⁻¹ • delta g) := by
127 have h := hdelta g⁻¹ g
128 rw [inv_mul_cancel, one hdelta] at h
129 rw [eq_neg_iff_add_eq_zero]
130 exact h.symm
132/-- Product rule, restated as a theorem for namespaced rewriting. -/
133theorem mul (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
134 delta (g * h) = delta g + coeff g • delta h :=
135 hdelta g h
137/-- Formula for multiplying by an inverse on the left. -/
138theorem inv_mul (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
139 delta (g⁻¹ * h) =
140 -(coeff g⁻¹ • delta g) + coeff g⁻¹ • delta h := by
141 rw [mul hdelta, inv hdelta]
143/-- Formula for multiplying by an inverse on the right. -/
144theorem mul_inv (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
145 delta (g * h⁻¹) =
146 delta g - coeff (g * h⁻¹) • delta h := by
147 rw [mul hdelta, inv hdelta]
148 simp only [smul_neg, smul_smul, map_mul, sub_eq_add_neg]
150/-- Division rule for a crossed differential. -/
151theorem div (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
152 delta (g / h) =
153 delta g - coeff (g / h) • delta h := by
154 simpa [div_eq_mul_inv] using mul_inv hdelta g h
156/-- Conjugation rule for a crossed differential. -/
157theorem conj (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
158 delta (g * h * g⁻¹) =
159 delta g + coeff g • delta h - coeff (g * h * g⁻¹) • delta g := by
160 rw [mul_inv hdelta (g * h) g, mul hdelta g h]
162/-- Commutator rule for a crossed differential. -/
163theorem commutator (hdelta : IsCrossedDifferential coeff delta) (g h : G) :
164 delta ⁅g, h⁆ =
165 delta g + coeff g • delta h -
166 coeff (g * h * g⁻¹) • delta g -
167 coeff ⁅g, h⁆ • delta h := by
168 rw [commutatorElement_def, mul_inv hdelta (g * h * g⁻¹) h,
169 conj hdelta g h]
171/-- Two crossed differentials with the same coefficients that agree on a set agree on the
172abstract subgroup generated by that set. -/
173theorem eqOn_closure {delta epsilon : G → A}
174 (hdelta : IsCrossedDifferential coeff delta)
175 (hepsilon : IsCrossedDifferential coeff epsilon)
176 {s : Set G} (hs : Set.EqOn delta epsilon s) :
177 Set.EqOn delta epsilon ((Subgroup.closure s : Subgroup G) : Set G) := by
178 intro g hg
179 exact
180 Subgroup.closure_induction
181 (p := fun g _ => delta g = epsilon g)
182 (fun x hx => hs hx)
183 (by
184 change delta 1 = epsilon 1
185 rw [hdelta.one, hepsilon.one])
186 (fun x y _ _ hx hy => by
187 change delta (x * y) = epsilon (x * y)
188 rw [hdelta.mul x y, hepsilon.mul x y, hx, hy])
189 (fun x _ hx => by
190 change delta x⁻¹ = epsilon x⁻¹
191 rw [hdelta.inv x, hepsilon.inv x, hx])
192 hg
194/-- Crossed differentials with the same coefficients are determined by a generating set. -/
195theorem eq_of_closure_eq_top {delta epsilon : G → A}
196 (hdelta : IsCrossedDifferential coeff delta)
197 (hepsilon : IsCrossedDifferential coeff epsilon)
198 {s : Set G} (hsgen : Subgroup.closure s = ⊤)
199 (hs : Set.EqOn delta epsilon s) :
200 delta = epsilon := by
201 funext g
202 exact (eqOn_closure hdelta hepsilon hs) (by simp only [hsgen, Subgroup.coe_top, Set.mem_univ])
204/-- Positive power rule for a crossed differential. -/
205theorem pow (hdelta : IsCrossedDifferential coeff delta) (g : G) (n : ℕ) :
206 delta (g ^ n) =
207 (Finset.range n).sum (fun k => coeff (g ^ k) • delta g) := by
208 induction n with
209 | zero =>
210 simp only [pow_zero, one hdelta, Finset.range_zero, map_pow, Finset.sum_empty]
211 | succ n ih =>
212 rw [pow_succ, hdelta, ih]
213 simp only [map_pow, Finset.sum_range_succ]
215/-- Positive power rule with the coefficient sum factored out. -/
216theorem pow_smul_sum (hdelta : IsCrossedDifferential coeff delta) (g : G) (n : ℕ) :
217 delta (g ^ n) =
218 ((Finset.range n).sum (fun k => coeff (g ^ k))) • delta g := by
219 rw [pow hdelta g n]
220 simp only [map_pow, Finset.sum_smul]
222/-- Positive power rule applied to the inverse element. -/
223theorem inv_pow (hdelta : IsCrossedDifferential coeff delta) (g : G) (n : ℕ) :
224 delta (g⁻¹ ^ n) =
225 (Finset.range n).sum (fun k =>
226 coeff (g⁻¹ ^ k) • (-(coeff g⁻¹ • delta g))) := by
227 rw [pow hdelta g⁻¹ n, inv hdelta]
231end FoxDifferential