Source: ProCGroups.FoxDifferential.Discrete.FoxCalculus.Coordinates
1import ProCGroups.FoxDifferential.Discrete.FoxCalculus.Boundary
3/-!
4# Fox differential: discrete — fox calculus — coordinates
6The principal declarations in this module are:
8- `relativeFreeFoxCoordinatesLinearEquivDifferential`
9 The linear equivalence between pushed-forward Fox coordinates and the universal differential
10 module of a finite-rank free group.
11- `relativeDifferentialToFreeFoxCoordinates_comp_relativeFreeFoxCoordinatesLinearMap`
12 The coordinate map is a left inverse to the coordinate-to-differential map.
13- `relativeFreeFoxCoordinatesLinearMap_comp_relativeDifferentialToFreeFoxCoordinates`
14 The coordinate-to-differential map is a left inverse to the differential-to-coordinate map.
15-/
17namespace FoxDifferential
19noncomputable section
21namespace FoxCalculus
23open scoped BigOperators
25universe u v
28variable {H : Type v} [Group H]
29variable (X : Type u)
31variable [DecidableEq X]
32variable (ψ : FreeGroup X →* H)
34variable [Fintype X]
36/-- The coordinate map is a left inverse to the coordinate-to-differential map. -/
37theorem relativeDifferentialToFreeFoxCoordinates_comp_relativeFreeFoxCoordinatesLinearMap :
38 (relativeDifferentialToFreeFoxCoordinates (H := H) X ψ).comp
39 (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ) =
40 LinearMap.id := by
41 apply LinearMap.ext
42 intro a
43 rw [LinearMap.comp_apply]
44 change relativeDifferentialToFreeFoxCoordinates (H := H) X ψ
45 (∑ y : X, a y • universalDifferential ψ (FreeGroup.of y)) = a
46 rw [map_sum]
47 simp only [map_smul, relativeDifferentialToFreeFoxCoordinates_d]
48 funext x
49 change ((∑ y : X,
50 a y • relativeFreeGroupFoxDerivative (H := H) X ψ (FreeGroup.of y)) :
51 RelativeFreeFoxCoordinates (H := H) X) x = a x
52 rw [Finset.sum_apply]
53 rw [Finset.sum_eq_single x]
54 · simp only [relativeFreeGroupFoxDerivative_of, Pi.smul_apply, Pi.single_eq_same, smul_eq_mul,
55 mul_one]
56 · intro y _ hy
57 have hxy : x ≠ y := fun h => hy h.symm
58 simp only [relativeFreeGroupFoxDerivative_of, Pi.smul_apply, Pi.single_eq_of_ne hxy,
59 smul_eq_mul, mul_zero]
60 · simp only [Finset.mem_univ, not_true_eq_false, relativeFreeGroupFoxDerivative_of, Pi.smul_apply,
61 Pi.single_eq_same, smul_eq_mul, mul_one, IsEmpty.forall_iff]
63/-- The coordinate-to-differential map is a left inverse to the differential-to-coordinate map. -/
64theorem relativeFreeFoxCoordinatesLinearMap_comp_relativeDifferentialToFreeFoxCoordinates :
65 (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ).comp
66 (relativeDifferentialToFreeFoxCoordinates (H := H) X ψ) =
67 LinearMap.id := by
68 apply hom_ext ψ
69 intro w
70 change relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
71 (relativeDifferentialToFreeFoxCoordinates (H := H) X ψ
72 (universalDifferential ψ w)) = universalDifferential ψ w
73 rw [relativeDifferentialToFreeFoxCoordinates_d,
74 relativeFreeFoxCoordinatesLinearMap_derivative]
76/--
77The linear equivalence between pushed-forward Fox coordinates and the universal differential
78module of a finite-rank free group.
79-/
80def relativeFreeFoxCoordinatesLinearEquivDifferential :
81 RelativeFreeFoxCoordinates (H := H) X ≃ₗ[GroupRing H] DifferentialModule ψ := by
82 refine LinearEquiv.ofLinear
83 (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ)
84 (relativeDifferentialToFreeFoxCoordinates (H := H) X ψ)
85 ?_ ?_
86 · exact relativeFreeFoxCoordinatesLinearMap_comp_relativeDifferentialToFreeFoxCoordinates
87 (H := H) X ψ
88 · exact relativeDifferentialToFreeFoxCoordinates_comp_relativeFreeFoxCoordinatesLinearMap
89 (H := H) X ψ
91end FoxCalculus
93end
95end FoxDifferential