def relativeDifferentialToFreeFoxCoordinates :
DifferentialModule ψ →ₗ[GroupRing H] RelativeFreeFoxCoordinates (H := H) X :=
lift
(A := RelativeFreeFoxCoordinates (H := H) X)
ψ
(relativeFreeGroupFoxDerivative (H := H) X ψ)
(relativeFreeGroupFoxDerivative_isDifferentialMap (H := H) X ψ)The universal map \(A_{\psi}\) \(\to\) \(\mathbb{Z}[H]^X\) induced by the relative Fox derivative.
theorem relativeDifferentialToFreeFoxCoordinates_d (w : FreeGroup X) :
relativeDifferentialToFreeFoxCoordinates (H := H) X ψ (universalDifferential ψ w) =
relativeFreeGroupFoxDerivative (H := H) X ψ wThe coordinate map out of the universal differential module sends \(\mathrm{universalDifferential}(w)\) to the Fox derivative of \(w\).
Show proof
by
simpa [relativeDifferentialToFreeFoxCoordinates] using
lift_d
(A := RelativeFreeFoxCoordinates (H := H) X)
ψ
(relativeFreeGroupFoxDerivative (H := H) X ψ)
(relativeFreeGroupFoxDerivative_isDifferentialMap (H := H) 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.
□def relativeFreeFoxCoordinatesLinearMap :
RelativeFreeFoxCoordinates (H := H) X →ₗ[GroupRing H] DifferentialModule ψ :=
{ toFun := fun a =>
∑ x : X, a x • universalDifferential ψ (FreeGroup.of x)
map_add' := by
intro a b
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Pi.add_apply, add_smul,
Finset.sum_add_distrib]
map_smul' := by
intro r a
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Pi.smul_apply, smul_eq_mul,
RingHom.id_apply, Finset.smul_sum, smul_smul]}The linear map from pushed-forward Fox-coordinate vectors to \(A_{\psi}\), sending the coordinate basis vector at \(x\) to \(\mathrm{universalDifferential}(\psi)(x)\).
theorem relativeFreeFoxCoordinatesLinearMap_single (x : X) :
relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
(Pi.single x (1 : GroupRing H)) =
universalDifferential ψ (FreeGroup.of x)The coordinate-to-differential map sends a coordinate basis vector to the corresponding universal generator differential.
Show proof
by
change (∑ y : X,
((Pi.single x (1 : GroupRing H) : RelativeFreeFoxCoordinates (H := H) X) y) •
universalDifferential ψ (FreeGroup.of y)) =
universalDifferential ψ (FreeGroup.of x)
rw [Finset.sum_eq_single x]
· simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Pi.single_eq_same, one_smul]
· intro y _ hy
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Pi.single_eq_of_ne hy, zero_smul]
· simp only [Finset.mem_univ, not_true_eq_false, relationSubmodule_eq_crossedDifferentialRelationSubmodule,
Pi.single_eq_same, one_smul, IsEmpty.forall_iff]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 relativeFreeGroupDifferential_inv (w : FreeGroup X) :
universalDifferential ψ w⁻¹ =
-((MonoidAlgebra.of ℤ H (ψ w⁻¹) : GroupRing H) • universalDifferential ψ w)The universal relative differential on a free group satisfies the inverse rule.
Show proof
by
have h := universalDifferential_mul_inv_right ψ w⁻¹
rw [eq_neg_iff_add_eq_zero]
simpa 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.
□theorem relativeFreeFoxCoordinatesLinearMap_derivative (w : FreeGroup X) :
relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
(relativeFreeGroupFoxDerivative (H := H) X ψ w) =
universalDifferential ψ wThe relative Fox-coordinate formula recovers the universal differential in \(A_{\psi}\).
Show proof
by
induction w using FreeGroup.induction_on with
| C1 =>
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, relativeFreeGroupFoxDerivative_one,
map_zero, universalDifferential_one]
| of x =>
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, relativeFreeGroupFoxDerivative_of,
relativeFreeFoxCoordinatesLinearMap_single]
| inv_of x hx =>
rw [relativeFreeGroupFoxDerivative_inv, map_neg, map_smul, hx]
exact (relativeFreeGroupDifferential_inv (H := H) X ψ (FreeGroup.of x)).symm
| mul x y hx hy =>
rw [relativeFreeGroupFoxDerivative_mul, map_add, map_smul, hx, hy]
simpa using (universalDifferential_mul ψ x y).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.
□