Yamaguchi Lean 4 Library
FoxDifferential/RightDerivative/Basic.lean
FoxDifferential/RightDerivative/Basic/Source

FoxDifferential/RightDerivative/Basic.lean

1import FoxDifferential.RightDerivative.GeometricSeries
2import FoxDifferential.Discrete.FoxCalculus.Derivative
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/RightDerivative/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Right Fox derivatives
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
21structure RightDerivation (G : Type*) [Group G] where
23 map_mul' : ∀ u v : FoxDifferential.GroupRing G,
24 toAddHom (u * v) =
25 toAddHom u * v + FoxDifferential.augmentation G u • toAddHom v
29variable {G : Type*} [Group G]
31instance instCoeFunRightDerivation : CoeFun (RightDerivation G) (fun _ =>
33 ⟨fun D => D.toAddHom⟩
35@[simp]
36theorem map_zero (D : RightDerivation G) : D 0 = 0 :=
37 D.toAddHom.map_zero
39@[simp]
41 D (u + v) = D u + D v :=
42 D.toAddHom.map_add u v
45 D (u * v) = D u * v + FoxDifferential.augmentation G u • D v :=
46 D.map_mul' u v
48@[simp]
49theorem map_one (D : RightDerivation G) : D 1 = 0 := by
50 have h := D.map_mul (1 : FoxDifferential.GroupRing G) 1
51 simp only [mul_one, augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe,
52 _root_.map_one, one_smul, left_eq_add] at h
53 exact h
55theorem map_inv_groupElement (D : RightDerivation G) (g : G) :
56 D (MonoidAlgebra.of ℤ G g⁻¹ : FoxDifferential.GroupRing G) =
57 -D (MonoidAlgebra.of ℤ G g : FoxDifferential.GroupRing G) *
58 (MonoidAlgebra.of ℤ G g⁻¹ : FoxDifferential.GroupRing G) := by
59 have h := D.map_mul
60 (MonoidAlgebra.of ℤ G g : FoxDifferential.GroupRing G)
61 (MonoidAlgebra.of ℤ G g⁻¹ : FoxDifferential.GroupRing G)
62 have h0 :
63 D.toAddHom (MonoidAlgebra.single (1 : G) 1 : FoxDifferential.GroupRing G) = 0 := by
64 change D (1 : FoxDifferential.GroupRing G) = 0
65 exact D.map_one
66 simp only [MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_inv_cancel, mul_one, augmentation,
67 augmentationAlgHom, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply,
68 one_smul] at h
69 rw [h0] at h
70 simpa [neg_mul] using eq_neg_of_add_eq_zero_right h.symm
72theorem map_pow_groupElement (D : RightDerivation G) (g : G) :
73 ∀ n : ℕ,
74 D (MonoidAlgebra.of ℤ G (g ^ n) : FoxDifferential.GroupRing G) =
75 D (MonoidAlgebra.of ℤ G g : FoxDifferential.GroupRing G) * geomSeries g n
76 | 0 => by
77 simp only [pow_zero, MonoidAlgebra.of_apply, geomSeries, Finset.range_zero, Finset.sum_empty, mul_zero]
78 change D (1 : FoxDifferential.GroupRing G) = 0
79 exact D.map_one
80 | n + 1 => by
81 rw [pow_succ]
82 have hmul :
83 (MonoidAlgebra.of ℤ G (g ^ n * g) : FoxDifferential.GroupRing G) =
84 (MonoidAlgebra.of ℤ G (g ^ n) : FoxDifferential.GroupRing G) *
85 MonoidAlgebra.of ℤ G g := by
86 simp only [MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
87 rw [hmul, map_mul]
89 simp only [MonoidAlgebra.of_apply, mul_assoc, augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe,
90 RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, mul_one, one_smul,
95 Finsupp.linearCombination ℤ δ
97@[simp]
99 (n : ℤ) :
100 groupRingLinearExtension δ (MonoidAlgebra.single g n : FoxDifferential.GroupRing G) =
101 n • δ g := by
102 exact Finsupp.linearCombination_single ℤ n g
106 (hδ : ∀ g h : G, δ (g * h) = δ g * MonoidAlgebra.of ℤ G h + δ h)
111 classical
112 induction u using Finsupp.induction_linear with
113 | zero =>
114 simp only [groupRingLinearExtension, zero_mul, _root_.map_zero, zero_smul, add_zero]
115 | add u₁ u₂ hu₁ hu₂ =>
116 simp only [add_mul, _root_.map_add, hu₁, zsmul_eq_mul, add_comm, hu₂, add_left_comm, add_assoc, Int.cast_add]
117 | single g n =>
118 induction v using Finsupp.induction_linear with
119 | zero =>
120 simp only [groupRingLinearExtension, mul_zero, _root_.map_zero, smul_zero, add_zero]
121 | add v₁ v₂ hv₁ hv₂ =>
122 simp only [mul_add, _root_.map_add, hv₁, groupRingLinearExtension_single, zsmul_eq_mul, hv₂, add_left_comm,
123 add_assoc, smul_add]
124 | single h m =>
125 rw [MonoidAlgebra.single_mul_single]
128 rw [hδ]
129 simp only [MonoidAlgebra.of_apply, smul_add, zsmul_eq_mul, Int.cast_mul, augmentation, augmentationAlgHom,
130 AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, mul_one]
131 rw [show (Finsupp.single h m : FoxDifferential.GroupRing G) =
132 algebraMap ℤ (FoxDifferential.GroupRing G) m *
133 (MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G) by
134 simpa using (MonoidAlgebra.single_eq_algebraMap_mul_of (M := G) h m)]
136 (δ g * (MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G)) +
140 (MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G)) +
143 rw [mul_assoc (n : FoxDifferential.GroupRing G) (δ g)
145 (MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G))]
146 rw [← mul_assoc (δ g) (m : FoxDifferential.GroupRing G)
147 (MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G)]
148 rw [(Int.cast_commute m (δ g)).eq.symm]
149 rw [mul_assoc (m : FoxDifferential.GroupRing G) (δ g)
150 (MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G)]
151 rw [← mul_assoc (n : FoxDifferential.GroupRing G) (m : FoxDifferential.GroupRing G)
152 (δ g * (MonoidAlgebra.of ℤ G h : FoxDifferential.GroupRing G))]
153 rw [← mul_assoc (n : FoxDifferential.GroupRing G) (m : FoxDifferential.GroupRing G)
154 (δ h)]
157 (hδ : ∀ g h : G, δ (g * h) = δ g * MonoidAlgebra.of ℤ G h + δ h) :
159 toAddHom := (groupRingLinearExtension δ).toAddMonoidHom
164end
166end FoxDifferential