Source: ProCGroups.FoxDifferential.RightDerivative.Semidirect
1import ProCGroups.FoxDifferential.Discrete.GroupRing
3/-!
4# Fox differential: right derivative — semidirect
6The principal declarations in this module are:
8- `RightFoxSemidirect`
9 The right Fox semidirect product records a group element together with its right-derivative
10 coordinate.
11- `rightHom`
12 The right Fox semidirect construction defines a homomorphism from a right derivation.
13- `ext`
14 The Fox semidirect construction has the stated component formula.
15- `one_left`
16 The additive component of the identity semidirect element is zero.
17-/
19namespace FoxDifferential
21noncomputable section
23/--
24The right Fox semidirect product records a group element together with its right-derivative
25coordinate.
26-/
27structure RightFoxSemidirect (G : Type*) [Group G] where
28 /-- The group-ring coordinate, representing the right Fox derivative. -/
29 left : FoxDifferential.GroupRing G
30 /-- The underlying group element. -/
31 right : G
33namespace RightFoxSemidirect
35variable {G : Type*} [Group G]
37/-- The Fox semidirect construction has the stated component formula. -/
38@[ext]
39theorem ext {x y : RightFoxSemidirect G}
40 (hleft : x.left = y.left) (hright : x.right = y.right) : x = y := by
41 cases x
42 cases y
43 simp_all
45/-- The unit of the right Fox semidirect product is the pair of identity components. -/
46instance instOneRightFoxSemidirect : One (RightFoxSemidirect G) where
47 one := ⟨0, 1⟩
49/--
50Multiplication in the right Fox semidirect product is given by the right action and group
51multiplication.
52-/
53instance instMulRightFoxSemidirect : Mul (RightFoxSemidirect G) where
54 mul x y :=
55 ⟨x.left * MonoidAlgebra.of ℤ G y.right + y.left, x.right * y.right⟩
57/--
58Inversion in the right Fox semidirect product is computed from the right action and the inverse
59in the base group.
60-/
61instance instInvRightFoxSemidirect : Inv (RightFoxSemidirect G) where
62 inv x :=
63 ⟨-x.left * MonoidAlgebra.of ℤ G x.right⁻¹, x.right⁻¹⟩
65/-- The additive component of the identity semidirect element is zero. -/
66@[simp]
67theorem one_left : (1 : RightFoxSemidirect G).left = 0 :=
68 rfl
70/-- The free-group component of the identity semidirect element is the identity word. -/
71@[simp]
72theorem one_right : (1 : RightFoxSemidirect G).right = 1 :=
73 rfl
75/-- The left component of semidirect multiplication is computed by the Fox product rule. -/
76@[simp]
77theorem mul_left (x y : RightFoxSemidirect G) :
78 (x * y).left = x.left * MonoidAlgebra.of ℤ G y.right + y.left :=
79 rfl
81/-- The right component of semidirect multiplication is the product of right components. -/
82@[simp]
83theorem mul_right (x y : RightFoxSemidirect G) :
84 (x * y).right = x.right * y.right :=
85 rfl
87/-- The left component of the semidirect inverse is computed by the Fox inverse formula. -/
88@[simp]
89theorem inv_left (x : RightFoxSemidirect G) :
90 x⁻¹.left = -x.left * MonoidAlgebra.of ℤ G x.right⁻¹ :=
91 rfl
93/-- The right component of the semidirect inverse is the inverse of the right component. -/
94@[simp]
95theorem inv_right (x : RightFoxSemidirect G) :
96 x⁻¹.right = x.right⁻¹ :=
97 rfl
99/-- The right Fox semidirect product carries the group structure induced by its right action. -/
100instance instGroupRightFoxSemidirect : Group (RightFoxSemidirect G) where
101 one := 1
102 mul := (· * ·)
103 inv := Inv.inv
104 mul_assoc x y z := by
105 apply RightFoxSemidirect.ext
106 · simp only [mul_left, mul_right, map_mul, add_mul, mul_assoc, add_assoc]
107 · simp only [mul_right, mul_assoc]
108 one_mul x := by
109 apply RightFoxSemidirect.ext
110 · simp only [mul_left, one_left, MonoidAlgebra.of_apply, zero_mul, zero_add]
111 · simp only [mul_right, one_right, one_mul]
112 mul_one x := by
113 apply RightFoxSemidirect.ext
114 · simp only [mul_left, one_right, map_one, one_left, add_zero, mul_one]
115 · simp only [mul_right, one_right, mul_one]
116 inv_mul_cancel x := by
117 apply RightFoxSemidirect.ext
118 · simp only [mul_left, inv_left]
119 rw [mul_assoc, ← map_mul, inv_mul_cancel, map_one, mul_one,
120 neg_add_cancel, one_left]
121 · simp only [mul_right, inv_right, inv_mul_cancel, one_right]
123/-- The right Fox semidirect construction defines a homomorphism from a right derivation. -/
124def rightHom : RightFoxSemidirect G →* G where
125 toFun x := x.right
126 map_one' := rfl
127 map_mul' _ _ := rfl
129/-- The right projection homomorphism of a Fox semidirect product returns its right coordinate. -/
130@[simp]
131theorem rightHom_apply (x : RightFoxSemidirect G) :
132 rightHom x = x.right :=
133 rfl
135end RightFoxSemidirect
137end
139end FoxDifferential