FoxDifferential.RightDerivative.Semidirect
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
structure RightFoxSemidirect (G : Type*) [Group G] where
left : FoxDifferential.GroupRing G
right : GThe right Fox semidirect product records a group element together with its right-derivative coordinate.
theorem ext {x y : RightFoxSemidirect G}
(hleft : x.left = y.left) (hright : x.right = y.right) : x = yThe Fox semidirect construction has the stated component formula.
Show proof
by
cases x
cases y
simp_allProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□instance instOneRightFoxSemidirect : One (RightFoxSemidirect G) where
one := ⟨0, 1⟩The unit of the right Fox semidirect product is the pair of identity components.
instance instMulRightFoxSemidirect : Mul (RightFoxSemidirect G) where
mul x y :=
⟨x.left * MonoidAlgebra.of ℤ G y.right + y.left, x.right * y.right⟩Multiplication in the right Fox semidirect product is given by the right action and group multiplication.
instance instInvRightFoxSemidirect : Inv (RightFoxSemidirect G) where
inv x :=
⟨-x.left * MonoidAlgebra.of ℤ G x.right⁻¹, x.right⁻¹⟩
@[simp]Inversion in the right Fox semidirect product is computed from the right action and the inverse in the base group.
theorem one_left : (1 : RightFoxSemidirect G).left = 0The additive component of the identity semidirect element is zero.
Show proof
rfl
@[simp]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem one_right : (1 : RightFoxSemidirect G).right = 1The free-group component of the identity semidirect element is the identity word.
Show proof
rfl
@[simp]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem mul_left (x y : RightFoxSemidirect G) :
(x * y).left = x.left * MonoidAlgebra.of ℤ G y.right + y.leftThe left component of semidirect multiplication is computed by the Fox product rule.
Show proof
rfl
@[simp]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem mul_right (x y : RightFoxSemidirect G) :
(x * y).right = x.right * y.rightThe right component of semidirect multiplication is the product of right components.
Show proof
rfl
@[simp]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem inv_left (x : RightFoxSemidirect G) :
x⁻¹.left = -x.left * MonoidAlgebra.of ℤ G x.right⁻¹The left component of the semidirect inverse is computed by the Fox inverse formula.
Show proof
rfl
@[simp]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem inv_right (x : RightFoxSemidirect G) :
x⁻¹.right = x.right⁻¹The right component of the semidirect inverse is the inverse of the right component.
Show proof
rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□instance instGroupRightFoxSemidirect : Group (RightFoxSemidirect G) where
one := 1
mul := (· * ·)
inv := Inv.inv
mul_assoc x y z := by
ext
· simp only [mul_left, MonoidAlgebra.of_apply, MonoidAlgebra.coe_add, Pi.add_apply,
MonoidAlgebra.mul_single_apply, mul_one, mul_right, mul_inv_rev, mul_assoc,
add_assoc]
· simp only [mul_right, mul_assoc]
one_mul x := by
ext
· simp only [mul_left, one_left, MonoidAlgebra.of_apply, zero_mul, zero_add]
· simp only [mul_right, one_right, one_mul]
mul_one x := by
ext
· simp only [mul_left, one_right, MonoidAlgebra.of_apply, one_left, add_zero,
MonoidAlgebra.mul_single_apply, inv_one, mul_one]
· simp only [mul_right, one_right, mul_one]
inv_mul_cancel x := by
ext
· simp only [mul_left, inv_left, MonoidAlgebra.of_apply, neg_mul, MonoidAlgebra.coe_add,
Pi.add_apply, MonoidAlgebra.neg_apply, MonoidAlgebra.mul_single_apply, inv_inv,
inv_mul_cancel_right, mul_one, neg_add_cancel, one_left, Finsupp.coe_zero,
Pi.zero_apply]
· simp only [mul_right, inv_right, inv_mul_cancel, one_right]The right Fox semidirect product carries the group structure induced by its right action.
def rightHom : RightFoxSemidirect G →* G where
toFun x := x.right
map_one' := rfl
map_mul' _ _ := rfl
@[simp]The right Fox semidirect construction defines a homomorphism from a right derivation.
theorem rightHom_apply (x : RightFoxSemidirect G) :
rightHom x = x.rightThe Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□