Yamaguchi Lean 4 Library
FoxDifferential/Discrete/FoxCalculus/Semidirect.lean
FoxDifferential/Discrete/FoxCalculus/Semidirect/Source

FoxDifferential/Discrete/FoxCalculus/Semidirect.lean

1import FoxDifferential.Discrete.DifferentialModule.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/FoxCalculus/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# Discrete group-ring Fox calculus
14Ordinary Fox derivatives over group rings are developed through augmentation, relative differential modules, coordinates, Jacobians, and chain rules.
15-/
16namespace FoxDifferential
18noncomputable section
20namespace FoxCalculus
22open scoped BigOperators
24universe u v
27variable {H : Type v} [Group H]
28variable (X : Type u)
30/-- Fox-coordinate vectors for a homomorphism from a free group to a target group `H`.
32The coefficients are already pushed forward to `ℤ[H]`; this is the coordinate module which will
33identify `A_ψ` with `ℤ[H]^X` for `ψ : FreeGroup X →* H`. -/
34abbrev RelativeFreeFoxCoordinates : Type _ := X → GroupRing H
36/-- The semidirect product encoding Fox crossed homomorphisms with coefficients pushed forward
37along a homomorphism `ψ : FreeGroup X →* H`. -/
38structure RelativeFoxSemidirect where
39 /-- The additive Fox-coordinate component. -/
40 left : RelativeFreeFoxCoordinates (H := H) X
41 /-- The target-group component. -/
42 right : H
46/-- Identity element of the relative Fox semidirect product. -/
47instance instOneRelativeFoxSemidirect : One (RelativeFoxSemidirect (H := H) X) where
48 one := ⟨0, 1⟩
50/-- Multiplication in the relative Fox semidirect product. -/
51instance instMulRelativeFoxSemidirect : Mul (RelativeFoxSemidirect (H := H) X) where
52 mul a b :=
53 ⟨a.left + (MonoidAlgebra.of ℤ H a.right : GroupRing H) • b.left, a.right * b.right⟩
55/-- Inversion in the relative Fox semidirect product. -/
56instance instInvRelativeFoxSemidirect : Inv (RelativeFoxSemidirect (H := H) X) where
57 inv a :=
58 ⟨-((MonoidAlgebra.of ℤ H a.right⁻¹ : GroupRing H) • a.left), a.right⁻¹⟩
60omit [Group H] in
61/-- Extensionality for the relative Fox semidirect product. -/
62@[ext]
63theorem ext {a b : RelativeFoxSemidirect (H := H) X}
64 (hleft : a.left = b.left) (hright : a.right = b.right) : a = b := by
65 cases a
66 cases b
67 simp_all
69/-- The left component of the identity semidirect element is zero. -/
70@[simp]
71theorem one_left : (1 : RelativeFoxSemidirect (H := H) X).left = 0 :=
72 rfl
74/-- The right component of the identity semidirect element is the group identity. -/
75@[simp]
76theorem one_right : (1 : RelativeFoxSemidirect (H := H) X).right = 1 :=
77 rfl
79/-- The left component of semidirect multiplication. -/
80@[simp]
81theorem mul_left (a b : RelativeFoxSemidirect (H := H) X) :
82 (a * b).left = a.left + (MonoidAlgebra.of ℤ H a.right : GroupRing H) • b.left :=
83 rfl
85/-- The right component of semidirect multiplication. -/
86@[simp]
87theorem mul_right (a b : RelativeFoxSemidirect (H := H) X) :
88 (a * b).right = a.right * b.right :=
89 rfl
91/-- The left component of semidirect inversion. -/
92@[simp]
93theorem inv_left (a : RelativeFoxSemidirect (H := H) X) :
94 a⁻¹.left = -((MonoidAlgebra.of ℤ H a.right⁻¹ : GroupRing H) • a.left) :=
95 rfl
97/-- The right component of semidirect inversion. -/
98@[simp]
99theorem inv_right (a : RelativeFoxSemidirect (H := H) X) :
100 a⁻¹.right = a.right⁻¹ :=
101 rfl
103/-- Group structure on the relative Fox semidirect product. -/
104instance instGroupRelativeFoxSemidirect : Group (RelativeFoxSemidirect (H := H) X) where
105 one := 1
106 mul := (· * ·)
107 inv := Inv.inv
108 mul_assoc a b c := by
109 ext
110 · simp only [mul_left, MonoidAlgebra.of_apply, mul_right, Pi.add_apply, Pi.smul_apply, smul_eq_mul, add_assoc,
111 MonoidAlgebra.coe_add, MonoidAlgebra.single_mul_apply, one_mul, mul_inv_rev, mul_assoc, smul_add, smul_smul,
112 MonoidAlgebra.single_mul_single, mul_one]
113 · simp only [mul_right, mul_assoc]
114 one_mul a := by
115 ext
116 · simp only [mul_left, one_left, one_right, map_one, one_smul, zero_add]
117 · simp only [mul_right, one_right, one_mul]
118 mul_one a := by
119 ext
120 · simp only [mul_left, one_left, smul_zero, add_zero]
121 · simp only [mul_right, one_right, mul_one]
122 inv_mul_cancel a := by
123 ext
124 · simp only [mul_left, inv_left, inv_right, neg_add_cancel, one_left]
125 · simp only [mul_right, inv_right, inv_mul_cancel, one_right]
129end FoxCalculus
131end
133end FoxDifferential