FoxDifferential.Discrete.Absolute
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
def freeGroupFoxDerivative (w : FreeGroup X) :
RelativeFreeFoxCoordinates (H := FreeGroup X) X :=
relativeFreeGroupFoxDerivative (H := FreeGroup X) X
(MonoidHom.id (FreeGroup X)) wThe absolute Fox derivative of a free-group word, with coefficients in \(\mathbb{Z}[\mathrm{FreeGroup}(X)]\).
theorem freeGroupFoxDerivative_one :
freeGroupFoxDerivative (X := X) (1 : FreeGroup X) = 0The absolute Fox derivative of the identity word is zero.
Show proof
by
simp only [freeGroupFoxDerivative, relativeFreeGroupFoxDerivative_one]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 freeGroupFoxDerivative_of (x : X) :
freeGroupFoxDerivative (X := X) (FreeGroup.of x) =
Pi.single x (1 : GroupRing (FreeGroup X))The absolute Fox derivative of a free generator is the corresponding coordinate vector.
Show proof
by
simp only [freeGroupFoxDerivative, relativeFreeGroupFoxDerivative_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 freeGroupFoxDerivative_mul (u v : FreeGroup X) :
freeGroupFoxDerivative (X := X) (u * v) =
freeGroupFoxDerivative (X := X) u +
(MonoidAlgebra.of ℤ (FreeGroup X) u : GroupRing (FreeGroup X)) •
freeGroupFoxDerivative (X := X) vProduct rule for the absolute Fox derivative.
Show proof
by
simpa [freeGroupFoxDerivative] using
relativeFreeGroupFoxDerivative_mul (H := FreeGroup X) X
(MonoidHom.id (FreeGroup X)) u vProof. 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 freeGroupFoxDerivative_inv (w : FreeGroup X) :
freeGroupFoxDerivative (X := X) w⁻¹ =
-((MonoidAlgebra.of ℤ (FreeGroup X) w⁻¹ : GroupRing (FreeGroup X)) •
freeGroupFoxDerivative (X := X) w)Inverse rule for the absolute Fox derivative.
Show proof
by
simpa [freeGroupFoxDerivative] using
relativeFreeGroupFoxDerivative_inv (H := FreeGroup X) X
(MonoidHom.id (FreeGroup X)) wProof. 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 freeGroupFoxDerivative_pow (w : FreeGroup X) (n : ℕ) :
freeGroupFoxDerivative (X := X) (w ^ n) =
(Finset.range n).sum (fun k =>
(MonoidAlgebra.of ℤ (FreeGroup X) (w ^ k) : GroupRing (FreeGroup X)) •
freeGroupFoxDerivative (X := X) w)Positive-power rule for the absolute Fox derivative.
Show proof
by
simpa [freeGroupFoxDerivative] using
relativeFreeGroupFoxDerivative_pow (H := FreeGroup X) X
(MonoidHom.id (FreeGroup 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 freeGroupFoxDerivative_conj (g h : FreeGroup X) :
freeGroupFoxDerivative (X := X) (g * h * g⁻¹) =
freeGroupFoxDerivative (X := X) g +
(MonoidAlgebra.of ℤ (FreeGroup X) g : GroupRing (FreeGroup X)) •
freeGroupFoxDerivative (X := X) h -
(MonoidAlgebra.of ℤ (FreeGroup X) (g * h * g⁻¹) :
GroupRing (FreeGroup X)) •
freeGroupFoxDerivative (X := X) gConjugation rule for the absolute Fox derivative.
Show proof
by
simpa [freeGroupFoxDerivative] using
relativeFreeGroupFoxDerivative_conj (H := FreeGroup X) X
(MonoidHom.id (FreeGroup 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 freeGroupFoxDerivative_commutator (g h : FreeGroup X) :
freeGroupFoxDerivative (X := X) ⁅g, h⁆ =
freeGroupFoxDerivative (X := X) g +
(MonoidAlgebra.of ℤ (FreeGroup X) g : GroupRing (FreeGroup X)) •
freeGroupFoxDerivative (X := X) h -
(MonoidAlgebra.of ℤ (FreeGroup X) (g * h * g⁻¹) :
GroupRing (FreeGroup X)) •
freeGroupFoxDerivative (X := X) g -
(MonoidAlgebra.of ℤ (FreeGroup X) ⁅g, h⁆ : GroupRing (FreeGroup X)) •
freeGroupFoxDerivative (X := X) hCommutator rule for the absolute Fox derivative.
Show proof
by
simpa [freeGroupFoxDerivative] using
relativeFreeGroupFoxDerivative_commutator (H := FreeGroup X) X
(MonoidHom.id (FreeGroup 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 freeGroupFoxDerivative_euler_formula (w : FreeGroup X) :
(MonoidAlgebra.of ℤ (FreeGroup X) w : GroupRing (FreeGroup X)) - 1 =
∑ x : X,
freeGroupFoxDerivative (X := X) w x *
augmentationGenerator (FreeGroup X) (FreeGroup.of x)The Euler formula for the free-group Fox derivative expresses a word as the augmentation term plus the sum of generator derivatives.
Show proof
by
simpa [freeGroupFoxDerivative] using
relativeFreeGroupFoxDerivative_euler_formula (H := FreeGroup X) X
(MonoidHom.id (FreeGroup X)) wProof. 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_eq_map_freeGroupFoxDerivative
(ψ : FreeGroup X →* H) (w : FreeGroup X) :
relativeFreeGroupFoxDerivative (H := H) X ψ w =
relativeFreeFoxCoordinatesMap (X := X) ψ
(freeGroupFoxDerivative (X := X) w)Relative Fox derivatives are obtained from the absolute derivative by pushing coefficients forward along \(\psi\).
Show proof
by
simpa [freeGroupFoxDerivative] using
relativeFreeGroupFoxDerivative_mapDomain
(H := FreeGroup X) (K := H) (X := X)
(MonoidHom.id (FreeGroup X)) ψ wProof. 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_eq_map_freeGroupFoxDerivative_apply
(ψ : FreeGroup X →* H) (w : FreeGroup X) (x : X) :
relativeFreeGroupFoxDerivative (H := H) X ψ w x =
groupRingMap ψ (freeGroupFoxDerivative (X := X) w x)Component form of the absolute-to-relative comparison: each relative Fox derivative coordinate is the group-ring image of the absolute coordinate.
Show proof
by
have h := congrFun
(relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative
(H := H) (X := X) ψ w) x
simpa [relativeFreeFoxCoordinatesMap] using 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.
□