theorem relativeDifferentialToFreeFoxCoordinates_comp_relativeFreeFoxCoordinatesLinearMap :
(relativeDifferentialToFreeFoxCoordinates (H := H) X ψ).comp
(relativeFreeFoxCoordinatesLinearMap (H := H) X ψ) =
LinearMap.idThe coordinate map is a left inverse to the coordinate-to-differential map.
Show proof
by
apply LinearMap.ext
intro a
rw [LinearMap.comp_apply]
change relativeDifferentialToFreeFoxCoordinates (H := H) X ψ
(∑ y : X, a y • universalDifferential ψ (FreeGroup.of y)) = a
rw [map_sum]
simp only [map_smul, relativeDifferentialToFreeFoxCoordinates_d]
funext x
change ((∑ y : X,
a y • relativeFreeGroupFoxDerivative (H := H) X ψ (FreeGroup.of y)) :
RelativeFreeFoxCoordinates (H := H) X) x = a x
rw [Finset.sum_apply]
rw [Finset.sum_eq_single x]
· simp only [relativeFreeGroupFoxDerivative_of, Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one]
· intro y _ hy
have hxy : x ≠ y := fun h => hy h.symm
simp only [relativeFreeGroupFoxDerivative_of, Pi.smul_apply, Pi.single_eq_of_ne hxy, smul_eq_mul, mul_zero]
· simp only [Finset.mem_univ, not_true_eq_false, relativeFreeGroupFoxDerivative_of, Pi.smul_apply,
Pi.single_eq_same, smul_eq_mul, mul_one, 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 relativeFreeFoxCoordinatesLinearMap_comp_relativeDifferentialToFreeFoxCoordinates :
(relativeFreeFoxCoordinatesLinearMap (H := H) X ψ).comp
(relativeDifferentialToFreeFoxCoordinates (H := H) X ψ) =
LinearMap.idThe coordinate-to-differential map is a left inverse to the differential-to-coordinate map.
Show proof
by
apply hom_ext ψ
intro w
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, LinearMap.coe_comp, Function.comp_apply,
relativeDifferentialToFreeFoxCoordinates_d, relativeFreeFoxCoordinatesLinearMap_derivative, LinearMap.id_coe, id_eq]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.
□def relativeFreeFoxCoordinatesLinearEquivDifferential :
RelativeFreeFoxCoordinates (H := H) X ≃ₗ[GroupRing H] DifferentialModule ψ := by
refine LinearEquiv.ofLinear
(relativeFreeFoxCoordinatesLinearMap (H := H) X ψ)
(relativeDifferentialToFreeFoxCoordinates (H := H) X ψ)
?_ ?_
· exact relativeFreeFoxCoordinatesLinearMap_comp_relativeDifferentialToFreeFoxCoordinates
(H := H) X ψ
· exact relativeDifferentialToFreeFoxCoordinates_comp_relativeFreeFoxCoordinatesLinearMap
(H := H) X ψThe linear equivalence between pushed-forward Fox coordinates and the universal differential module of a finite-rank free group.