FoxDifferential.Discrete.FoxCalculus.Semidirect
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
abbrev RelativeFreeFoxCoordinates : Type _ := X → GroupRing HFox-coordinate vectors for a homomorphism from a free group to a target group \(H\). The coefficients are already pushed forward to \(\mathbb{Z}[H]\); this is the coordinate module which will identify \(A_{\psi}\) with \(\mathbb{Z}[H]^X\) for \(\psi:\mathrm{FreeGroup}(X)\to H\).
structure RelativeFoxSemidirect where
/-- The additive Fox-coordinate component. -/
left : RelativeFreeFoxCoordinates (H := H) X
/-- The target-group component. -/
right : HThe semidirect product encoding Fox crossed homomorphisms with coefficients pushed forward along a homomorphism \(\psi:\mathrm{FreeGroup}(X)\to H\).
instance instOneRelativeFoxSemidirect : One (RelativeFoxSemidirect (H := H) X) where
one := ⟨0, 1⟩The unit of the relative Fox semidirect product is the pair of identity components.
instance instMulRelativeFoxSemidirect : Mul (RelativeFoxSemidirect (H := H) X) where
mul a b :=
⟨a.left + (MonoidAlgebra.of ℤ H a.right : GroupRing H) • b.left, a.right * b.right⟩Multiplication in the relative Fox semidirect product is given by the pushed-forward coefficient action and group multiplication.
instance instInvRelativeFoxSemidirect : Inv (RelativeFoxSemidirect (H := H) X) where
inv a :=
⟨-((MonoidAlgebra.of ℤ H a.right⁻¹ : GroupRing H) • a.left), a.right⁻¹⟩Inversion in the relative Fox semidirect product is computed from the pushed-forward coefficient action and the inverse in the base group.
theorem ext {a b : RelativeFoxSemidirect (H := H) X}
(hleft : a.left = b.left) (hright : a.right = b.right) : a = bExtensionality for the relative Fox semidirect product.
Show proof
by
cases a
cases b
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.
□theorem one_left : (1 : RelativeFoxSemidirect (H := H) X).left = 0The left component of the identity semidirect element is zero.
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.
□theorem one_right : (1 : RelativeFoxSemidirect (H := H) X).right = 1The right component of the identity semidirect element is the group identity.
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.
□theorem mul_left (a b : RelativeFoxSemidirect (H := H) X) :
(a * b).left = a.left + (MonoidAlgebra.of ℤ H a.right : GroupRing H) • b.leftThe left component of semidirect multiplication.
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.
□theorem mul_right (a b : RelativeFoxSemidirect (H := H) X) :
(a * b).right = a.right * b.rightThe right component of semidirect multiplication.
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.
□theorem inv_left (a : RelativeFoxSemidirect (H := H) X) :
a⁻¹.left = -((MonoidAlgebra.of ℤ H a.right⁻¹ : GroupRing H) • a.left)The left component of semidirect inversion.
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.
□theorem inv_right (a : RelativeFoxSemidirect (H := H) X) :
a⁻¹.right = a.right⁻¹The right component of semidirect inversion.
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 instGroupRelativeFoxSemidirect : Group (RelativeFoxSemidirect (H := H) X) where
one := 1
mul := (· * ·)
inv := Inv.inv
mul_assoc a b c := by
ext
· simp only [mul_left, MonoidAlgebra.of_apply, mul_right, Pi.add_apply, Pi.smul_apply, smul_eq_mul, add_assoc,
MonoidAlgebra.coe_add, MonoidAlgebra.single_mul_apply, one_mul, mul_inv_rev, mul_assoc, smul_add, smul_smul,
MonoidAlgebra.single_mul_single, mul_one]
· simp only [mul_right, mul_assoc]
one_mul a := by
ext
· simp only [mul_left, one_left, one_right, map_one, one_smul, zero_add]
· simp only [mul_right, one_right, one_mul]
mul_one a := by
ext
· simp only [mul_left, one_left, smul_zero, add_zero]
· simp only [mul_right, one_right, mul_one]
inv_mul_cancel a := by
ext
· simp only [mul_left, inv_left, inv_right, neg_add_cancel, one_left]
· simp only [mul_right, inv_right, inv_mul_cancel, one_right]The relative Fox semidirect product carries the group structure induced by the pushed-forward coefficient action.