FoxDifferential/RightDerivative/Semidirect.lean
1import FoxDifferential.RightDerivative.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/RightDerivative/Semidirect.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Right Fox derivatives
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20structure RightFoxSemidirect (G : Type*) [Group G] where
21 left : FoxDifferential.GroupRing G
22 right : G
24namespace RightFoxSemidirect
26variable {G : Type*} [Group G]
28@[ext]
29theorem ext {x y : RightFoxSemidirect G}
30 (hleft : x.left = y.left) (hright : x.right = y.right) : x = y := by
31 cases x
32 cases y
33 simp_all
35instance instOneRightFoxSemidirect : One (RightFoxSemidirect G) where
38instance instMulRightFoxSemidirect : Mul (RightFoxSemidirect G) where
39 mul x y :=
40 ⟨x.left * MonoidAlgebra.of ℤ G y.right + y.left, x.right * y.right⟩
42instance instInvRightFoxSemidirect : Inv (RightFoxSemidirect G) where
43 inv x :=
44 ⟨-x.left * MonoidAlgebra.of ℤ G x.right⁻¹, x.right⁻¹⟩
46@[simp]
47theorem one_left : (1 : RightFoxSemidirect G).left = 0 :=
48 rfl
50@[simp]
51theorem one_right : (1 : RightFoxSemidirect G).right = 1 :=
52 rfl
54@[simp]
55theorem mul_left (x y : RightFoxSemidirect G) :
56 (x * y).left = x.left * MonoidAlgebra.of ℤ G y.right + y.left :=
57 rfl
59@[simp]
60theorem mul_right (x y : RightFoxSemidirect G) :
61 (x * y).right = x.right * y.right :=
62 rfl
64@[simp]
65theorem inv_left (x : RightFoxSemidirect G) :
66 x⁻¹.left = -x.left * MonoidAlgebra.of ℤ G x.right⁻¹ :=
67 rfl
69@[simp]
70theorem inv_right (x : RightFoxSemidirect G) :
71 x⁻¹.right = x.right⁻¹ :=
72 rfl
74instance instGroupRightFoxSemidirect : Group (RightFoxSemidirect G) where
76 mul := (· * ·)
77 inv := Inv.inv
78 mul_assoc x y z := by
79 ext
80 · simp only [mul_left, MonoidAlgebra.of_apply, MonoidAlgebra.coe_add, Pi.add_apply,
81 MonoidAlgebra.mul_single_apply, mul_one, mul_right, mul_inv_rev, mul_assoc,
82 add_assoc]
83 · simp only [mul_right, mul_assoc]
84 one_mul x := by
85 ext
86 · simp only [mul_left, one_left, MonoidAlgebra.of_apply, zero_mul, zero_add]
87 · simp only [mul_right, one_right, one_mul]
88 mul_one x := by
89 ext
90 · simp only [mul_left, one_right, MonoidAlgebra.of_apply, one_left, add_zero,
91 MonoidAlgebra.mul_single_apply, inv_one, mul_one]
92 · simp only [mul_right, one_right, mul_one]
93 inv_mul_cancel x := by
94 ext
95 · simp only [mul_left, inv_left, MonoidAlgebra.of_apply, neg_mul, MonoidAlgebra.coe_add,
97 inv_mul_cancel_right, mul_one, neg_add_cancel, one_left, Finsupp.coe_zero,
98 Pi.zero_apply]
99 · simp only [mul_right, inv_right, inv_mul_cancel, one_right]
101def rightHom : RightFoxSemidirect G →* G where
102 toFun x := x.right
103 map_one' := rfl
104 map_mul' _ _ := rfl
106@[simp]
107theorem rightHom_apply (x : RightFoxSemidirect G) :
109 rfl
113end
115end FoxDifferential