FoxDifferential.Discrete.FoxCalculus.Derivative
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.
import
def relativeFreeGroupFoxLift : FreeGroup X →* RelativeFoxSemidirect (H := H) X :=
FreeGroup.lift fun x =>
{ left := Pi.single x (1 : GroupRing H)
right := ψ (FreeGroup.of x) }The semidirect-product lift whose left component is the Fox derivative pushed forward by \(\psi\), and whose right component is \(\psi\) itself.
def relativeFreeGroupFoxDerivative (w : FreeGroup X) :
RelativeFreeFoxCoordinates (H := H) X :=
(relativeFreeGroupFoxLift (H := H) X ψ w).leftThe Fox derivative of a free-group word, with coefficients pushed forward to \(\mathbb{Z}[H]\) by \(\psi\).
theorem relativeFreeGroupFoxLift_right (w : FreeGroup X) :
(relativeFreeGroupFoxLift (H := H) X ψ w).right = ψ wThe right component of the relative Fox lift is the target homomorphism \(\psi\).
Show proof
by
induction w using FreeGroup.induction_on with
| C1 =>
simp only [relativeFreeGroupFoxLift, map_one, RelativeFoxSemidirect.one_right]
| of x =>
simp only [relativeFreeGroupFoxLift, FreeGroup.lift_apply_of]
| inv_of x hx =>
simpa using congrArg Inv.inv hx
| mul x y hx hy =>
simp only [map_mul, RelativeFoxSemidirect.mul_right, hx, hy]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 relativeFreeGroupFoxDerivative_one :
relativeFreeGroupFoxDerivative (H := H) X ψ (1 : FreeGroup X) = 0The relative Fox derivative of the identity word is zero.
Show proof
by
simp only [relativeFreeGroupFoxDerivative, relativeFreeGroupFoxLift, map_one, RelativeFoxSemidirect.one_left]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 relativeFreeGroupFoxDerivative_of (x : X) :
relativeFreeGroupFoxDerivative (H := H) X ψ (FreeGroup.of x) =
Pi.single x (1 : GroupRing H)The relative Fox derivative of a free generator is the corresponding coordinate vector.
Show proof
by
simp only [relativeFreeGroupFoxDerivative, relativeFreeGroupFoxLift, FreeGroup.lift_apply_of]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 relativeFreeGroupFoxDerivative_mul (w₁ w₂ : FreeGroup X) :
relativeFreeGroupFoxDerivative (H := H) X ψ (w₁ * w₂) =
relativeFreeGroupFoxDerivative (H := H) X ψ w₁ +
(MonoidAlgebra.of ℤ H (ψ w₁) : GroupRing H) •
relativeFreeGroupFoxDerivative (H := H) X ψ w₂Relative Fox product rule.
Show proof
by
simp only [relativeFreeGroupFoxDerivative, map_mul, RelativeFoxSemidirect.mul_left,
relativeFreeGroupFoxLift_right, MonoidAlgebra.of_apply]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 relativeFreeGroupFoxDerivative_inv (w : FreeGroup X) :
relativeFreeGroupFoxDerivative (H := H) X ψ w⁻¹ =
-((MonoidAlgebra.of ℤ H (ψ w⁻¹) : GroupRing H) •
relativeFreeGroupFoxDerivative (H := H) X ψ w)The relative Fox derivative satisfies the inverse rule.
Show proof
by
simp only [relativeFreeGroupFoxDerivative, map_inv, RelativeFoxSemidirect.inv_left,
relativeFreeGroupFoxLift_right, MonoidAlgebra.of_apply]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 relativeFreeGroupFoxDerivative_isDifferentialMap :
IsDifferentialMap
(A := RelativeFreeFoxCoordinates (H := H) X)
ψ
(relativeFreeGroupFoxDerivative (H := H) X ψ)The relative free-group Fox derivative is a differential map for \(\psi\).
Show proof
by
intro w₁ w₂
simpa using relativeFreeGroupFoxDerivative_mul (H := H) X ψ w₁ w₂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 relativeFreeGroupFoxDerivative_unique
(delta : FreeGroup X → RelativeFreeFoxCoordinates (H := H) X)
(hdelta : IsDifferentialMap (A := RelativeFreeFoxCoordinates (H := H) X) ψ delta)
(hbasis :
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : GroupRing H)) :
delta = relativeFreeGroupFoxDerivative (H := H) X ψUniqueness of the relative free-group Fox derivative among differential maps with standard coordinate values on free generators.
Show proof
by
have hdelta_free :
delta =
freeCrossedDifferentialWithCoeff
(A := RelativeFreeFoxCoordinates (H := H) X) (groupRingScalar ψ)
(fun x : X => Pi.single x (1 : GroupRing H)) :=
freeCrossedDifferentialWithCoeff_unique
(A := RelativeFreeFoxCoordinates (H := H) X) (groupRingScalar ψ)
(fun x : X => Pi.single x (1 : GroupRing H))
delta hdelta hbasis
have hrelative_free :
relativeFreeGroupFoxDerivative (H := H) X ψ =
freeCrossedDifferentialWithCoeff
(A := RelativeFreeFoxCoordinates (H := H) X) (groupRingScalar ψ)
(fun x : X => Pi.single x (1 : GroupRing H)) :=
freeCrossedDifferentialWithCoeff_unique
(A := RelativeFreeFoxCoordinates (H := H) X) (groupRingScalar ψ)
(fun x : X => Pi.single x (1 : GroupRing H))
(relativeFreeGroupFoxDerivative (H := H) X ψ)
(relativeFreeGroupFoxDerivative_isDifferentialMap (H := H) X ψ)
(relativeFreeGroupFoxDerivative_of (H := H) X ψ)
exact hdelta_free.trans hrelative_free.symmProof. 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 relativeFreeGroupFoxDerivative_pow (w : FreeGroup X) (n : ℕ) :
relativeFreeGroupFoxDerivative (H := H) X ψ (w ^ n) =
(Finset.range n).sum (fun k =>
(MonoidAlgebra.of ℤ H (ψ (w ^ k)) : GroupRing H) •
relativeFreeGroupFoxDerivative (H := H) X ψ w)Relative Fox derivative of a positive power.
Show proof
by
simpa [groupRingScalar] using
IsCrossedDifferential.pow
(relativeFreeGroupFoxDerivative_isDifferentialMap (H := H) X ψ) w nProof. 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 relativeFreeGroupFoxDerivative_conj (g h : FreeGroup X) :
relativeFreeGroupFoxDerivative (H := H) X ψ (g * h * g⁻¹) =
relativeFreeGroupFoxDerivative (H := H) X ψ g +
(MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) •
relativeFreeGroupFoxDerivative (H := H) X ψ h -
(MonoidAlgebra.of ℤ H (ψ (g * h * g⁻¹)) : GroupRing H) •
relativeFreeGroupFoxDerivative (H := H) X ψ gRelative Fox derivative of a conjugate.
Show proof
by
simpa [groupRingScalar] using
IsCrossedDifferential.conj
(relativeFreeGroupFoxDerivative_isDifferentialMap (H := H) X ψ) g hProof. 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 relativeFreeGroupFoxDerivative_commutator (g h : FreeGroup X) :
relativeFreeGroupFoxDerivative (H := H) X ψ ⁅g, h⁆ =
relativeFreeGroupFoxDerivative (H := H) X ψ g +
(MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) •
relativeFreeGroupFoxDerivative (H := H) X ψ h -
(MonoidAlgebra.of ℤ H (ψ (g * h * g⁻¹)) : GroupRing H) •
relativeFreeGroupFoxDerivative (H := H) X ψ g -
(MonoidAlgebra.of ℤ H (ψ ⁅g, h⁆) : GroupRing H) •
relativeFreeGroupFoxDerivative (H := H) X ψ hRelative Fox derivative of a commutator.
Show proof
by
simpa [groupRingScalar] using
IsCrossedDifferential.commutator
(relativeFreeGroupFoxDerivative_isDifferentialMap (H := H) X ψ) g hProof. 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.
□