ProCGroups.FoxDifferential.Discrete.FoxCalculus.Coordinates
The principal declarations in this module are:
relativeFreeFoxCoordinatesLinearEquivDifferentialThe linear equivalence between pushed-forward Fox coordinates and the universal differential module of a finite-rank free group. -relativeDifferentialToFreeFoxCoordinates_comp_relativeFreeFoxCoordinatesLinearMapThe coordinate map is a left inverse to the coordinate-to-differential map. -relativeFreeFoxCoordinatesLinearMap_comp_relativeDifferentialToFreeFoxCoordinatesThe coordinate-to-differential map is a left inverse to the differential-to-coordinate map.
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 Lean 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]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 Lean proof
by
apply hom_ext ψ
intro w
change relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
(relativeDifferentialToFreeFoxCoordinates (H := H) X ψ
(universalDifferential ψ w)) = universalDifferential ψ w
rw [relativeDifferentialToFreeFoxCoordinates_d,
relativeFreeFoxCoordinatesLinearMap_derivative]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.