Source: ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Coordinates
1import ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Universal
3/-!
4# Fox differential: completed — residue — free group — coordinates
6The principal declarations in this module are:
8- `residueDifferentialToFreeFoxCoordinates`
9 The linear map from the residue universal module to residue Fox-coordinate vectors.
10- `residueFreeFoxCoordinatesLinearMap`
11 The linear map from residue Fox-coordinate vectors to the residue universal module, sending the
12 coordinate basis at \(x\) to \(d_{\psi}(x)\).
13- `residueDifferentialToFreeFoxCoordinates_universal`
14 The residue coordinate map sends a universal differential to the residue Fox derivative vector.
15- `residueFreeFoxCoordinatesLinearMap_single`
16 The coordinate-to-differential map sends a coordinate basis vector to the corresponding universal
17 residue differential.
18-/
20namespace FoxDifferential
22noncomputable section
24open scoped BigOperators
26universe u v
29variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
31section FiniteBasis
33variable [Fintype X]
35/-- The linear map from the residue universal module to residue Fox-coordinate vectors. -/
36def residueDifferentialToFreeFoxCoordinates (n : ℕ) (ψ : FreeGroup X →* H) :
37 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
38 ResidueFreeFoxCoordinates n H X :=
39 residueFreeGroupFoxDerivativeVectorLinearMap n ψ
41omit [Fintype X] in
42/--
43The residue coordinate map sends a universal differential to the residue Fox derivative vector.
44-/
45@[simp]
46theorem residueDifferentialToFreeFoxCoordinates_universal
47 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
48 residueDifferentialToFreeFoxCoordinates n ψ
49 (residueUniversalDifferential n ψ w) =
50 residueFreeGroupFoxDerivativeVector n ψ w := by
51 exact residueFreeGroupFoxDerivativeVectorLinearMap_universal n ψ w
53/--
54The linear map from residue Fox-coordinate vectors to the residue universal module, sending the
55coordinate basis at \(x\) to \(d_{\psi}(x)\).
56-/
57def residueFreeFoxCoordinatesLinearMap (n : ℕ) (ψ : FreeGroup X →* H) :
58 ResidueFreeFoxCoordinates n H X →ₗ[ResidueGroupRing n H]
59 ResidueDifferentialModule n ψ where
60 toFun v := ∑ x : X, v x • residueUniversalDifferential n ψ (FreeGroup.of x)
61 map_add' := by
62 intro v w
63 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
64 map_smul' := by
65 intro r v
66 simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]
68/--
69The coordinate-to-differential map sends a coordinate basis vector to the corresponding
70universal residue differential.
71-/
72@[simp]
73theorem residueFreeFoxCoordinatesLinearMap_single
74 (n : ℕ) (ψ : FreeGroup X →* H) (x : X) :
75 residueFreeFoxCoordinatesLinearMap n ψ
76 (Pi.single x (1 : ResidueGroupRing n H)) =
77 residueUniversalDifferential n ψ (FreeGroup.of x) := by
78 change (∑ y : X,
79 ((Pi.single x (1 : ResidueGroupRing n H) : ResidueFreeFoxCoordinates n H X) y) •
80 residueUniversalDifferential n ψ (FreeGroup.of y)) =
81 residueUniversalDifferential n ψ (FreeGroup.of x)
82 rw [Finset.sum_eq_single x]
83 · simp only [Pi.single_eq_same, one_smul]
84 · intro y _ hy
85 simp only [Pi.single_eq_of_ne hy, zero_smul]
86 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
88/--
89The coordinate-to-differential map recovers the universal residue differential from the residue
90derivative vector.
91-/
92theorem residueFreeFoxCoordinatesLinearMap_derivativeVector
93 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
94 residueFreeFoxCoordinatesLinearMap n ψ
95 (residueFreeGroupFoxDerivativeVector n ψ w) =
96 residueUniversalDifferential n ψ w := by
97 let beta : ScalarCrossedHom (residueGroupRingScalar n ψ)
98 (ResidueDifferentialModule n ψ) :=
99 (residueFreeGroupFoxDerivativeVector n ψ).mapLinear
100 (residueFreeFoxCoordinatesLinearMap n ψ)
101 have hbasis :
102 ∀ x : X, beta (FreeGroup.of x) =
103 residueUniversalDifferential n ψ (FreeGroup.of x) := by
104 intro x
105 change residueFreeFoxCoordinatesLinearMap n ψ
106 (residueFreeGroupFoxDerivativeVector n ψ (FreeGroup.of x)) =
107 residueUniversalDifferential n ψ (FreeGroup.of x)
108 rw [residueFreeGroupFoxDerivativeVector_of, residueFreeFoxCoordinatesLinearMap_single]
109 have hbeta_eq :
110 beta =
111 freeCrossedHomWithCoeff
112 (A := ResidueDifferentialModule n ψ)
113 (residueGroupRingScalar n ψ)
114 (fun x => residueUniversalDifferential n ψ (FreeGroup.of x)) := by
115 exact freeCrossedHomWithCoeff_unique
116 (A := ResidueDifferentialModule n ψ)
117 (residueGroupRingScalar n ψ)
118 (fun x => residueUniversalDifferential n ψ (FreeGroup.of x)) beta hbasis
119 have huniv_eq :
120 residueUniversalDifferential n ψ =
121 freeCrossedHomWithCoeff
122 (A := ResidueDifferentialModule n ψ)
123 (residueGroupRingScalar n ψ)
124 (fun x => residueUniversalDifferential n ψ (FreeGroup.of x)) := by
125 exact freeCrossedHomWithCoeff_unique
126 (A := ResidueDifferentialModule n ψ)
127 (residueGroupRingScalar n ψ)
128 (fun x => residueUniversalDifferential n ψ (FreeGroup.of x))
129 (residueUniversalDifferential n ψ) (by intro x; rfl)
130 exact congrArg
131 (fun d : ScalarCrossedHom (residueGroupRingScalar n ψ)
132 (ResidueDifferentialModule n ψ) => d w)
133 (hbeta_eq.trans huniv_eq.symm)
135/-- The coordinate map is a left inverse to the coordinate-to-differential map. -/
136theorem residueDifferentialToFreeFoxCoordinates_comp_residueFreeFoxCoordinatesLinearMap
137 (n : ℕ) (ψ : FreeGroup X →* H) :
138 (residueDifferentialToFreeFoxCoordinates n ψ).comp
139 (residueFreeFoxCoordinatesLinearMap n ψ) =
140 LinearMap.id := by
141 apply LinearMap.ext
142 intro v
143 rw [LinearMap.comp_apply]
144 change residueDifferentialToFreeFoxCoordinates n ψ
145 (∑ y : X, v y • residueUniversalDifferential n ψ (FreeGroup.of y)) = v
146 rw [map_sum]
147 simp only [map_smul, residueDifferentialToFreeFoxCoordinates_universal]
148 funext x
149 change ((∑ y : X,
150 v y • residueFreeGroupFoxDerivativeVector n ψ (FreeGroup.of y)) :
151 ResidueFreeFoxCoordinates n H X) x = v x
152 rw [Finset.sum_apply]
153 rw [Finset.sum_eq_single x]
154 · simp only [residueFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_same,
155 smul_eq_mul, mul_one]
156 · intro y _ hy
157 have hxy : x ≠ y := fun h => hy h.symm
158 simp only [residueFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_of_ne hxy,
159 smul_eq_mul,
160 mul_zero]
161 · simp only [Finset.mem_univ, not_true_eq_false, residueFreeGroupFoxDerivativeVector_of,
162 Pi.smul_apply,
163 Pi.single_eq_same, smul_eq_mul, mul_one, IsEmpty.forall_iff]
165/-- The coordinate-to-differential map is a left inverse to the residue coordinate map. -/
166theorem residueFreeFoxCoordinatesLinearMap_comp_residueDifferentialToFreeFoxCoordinates
167 (n : ℕ) (ψ : FreeGroup X →* H) :
168 (residueFreeFoxCoordinatesLinearMap n ψ).comp
169 (residueDifferentialToFreeFoxCoordinates n ψ) =
170 LinearMap.id := by
171 apply residueDifferentialModuleHom_ext n ψ
172 intro w
173 simp only [LinearMap.comp_apply, residueDifferentialToFreeFoxCoordinates_universal,
174 residueFreeFoxCoordinatesLinearMap_derivativeVector, LinearMap.id_coe, id_eq]
176/--
177The linear equivalence between residue Fox coordinates and the residue universal differential
178module of a finite-rank free group.
179-/
180def residueFreeFoxCoordinatesLinearEquivDifferential
181 (n : ℕ) (ψ : FreeGroup X →* H) :
182 ResidueFreeFoxCoordinates n H X ≃ₗ[ResidueGroupRing n H]
183 ResidueDifferentialModule n ψ := by
184 refine LinearEquiv.ofLinear
185 (residueFreeFoxCoordinatesLinearMap n ψ)
186 (residueDifferentialToFreeFoxCoordinates n ψ)
187 ?_ ?_
188 · exact residueFreeFoxCoordinatesLinearMap_comp_residueDifferentialToFreeFoxCoordinates
189 n ψ
190 · exact residueDifferentialToFreeFoxCoordinates_comp_residueFreeFoxCoordinatesLinearMap
191 n ψ
193end FiniteBasis
196end
198end FoxDifferential