Source: ProCGroups.FoxDifferential.Common.FoxBoundary
1import ProCGroups.FoxDifferential.Common.FreeCrossedDifferential
3/-!
4# Fox differential: common — fox boundary
6The principal declarations in this module are:
8- `coefficientFoxBoundary`
9 The Fox boundary crossed differential attached to a coefficient homomorphism: \(g \mapsto
10 \operatorname{coeff}(g)-1\).
11- `coefficientFoxBoundaryCrossedHom`
12 The coefficient Fox boundary is a crossed differential.
13- `coefficientFoxBoundary_one`
14 The coefficient Fox boundary sends the identity to zero.
15- `coefficientFoxBoundary_mul`
16 Product rule for the coefficient Fox boundary \(g \mapsto \operatorname{coeff}(g)-1\).
17-/
19namespace FoxDifferential
21noncomputable section
23open scoped BigOperators
25universe u v
27section CoefficientBoundary
29variable {R : Type u} [Ring R]
30variable {G : Type v} [Group G]
32/--
33The Fox boundary crossed differential attached to a coefficient homomorphism: \(g \mapsto
34\operatorname{coeff}(g)-1\).
35-/
36def coefficientFoxBoundary (coeff : G →* R) (g : G) : R :=
37 coeff g - 1
39/-- The coefficient Fox boundary sends the identity to zero. -/
40@[simp]
41theorem coefficientFoxBoundary_one (coeff : G →* R) :
42 coefficientFoxBoundary coeff 1 = 0 := by
43 simp only [coefficientFoxBoundary, map_one, sub_self]
45/-- Product rule for the coefficient Fox boundary \(g \mapsto \operatorname{coeff}(g)-1\). -/
46theorem coefficientFoxBoundary_mul (coeff : G →* R) (g h : G) :
47 coefficientFoxBoundary coeff (g * h) =
48 coefficientFoxBoundary coeff g + coeff g • coefficientFoxBoundary coeff h := by
49 rw [coefficientFoxBoundary, coefficientFoxBoundary, coefficientFoxBoundary, map_mul]
50 change coeff g * coeff h - 1 = coeff g - 1 + coeff g * (coeff h - 1)
51 rw [sub_eq_add_neg, sub_eq_add_neg, sub_eq_add_neg, mul_add, mul_neg, mul_one]
52 rw [show coeff g + -1 + (coeff g * coeff h + -coeff g) =
53 coeff g + -coeff g + (coeff g * coeff h + -1) by ac_rfl]
54 simp only [add_neg_cancel, zero_add]
56/-- The coefficient Fox boundary is a crossed differential. -/
57def coefficientFoxBoundaryCrossedHom (coeff : G →* R) : ScalarCrossedHom coeff R where
58 toFun := coefficientFoxBoundary coeff
59 map_mul' := coefficientFoxBoundary_mul coeff
61/-- The coefficient boundary crossed homomorphism sends a group element to its coefficient
62minus one. -/
63@[simp]
64theorem coefficientFoxBoundaryCrossedHom_apply (coeff : G →* R) (g : G) :
65 coefficientFoxBoundaryCrossedHom coeff g = coeff g - 1 :=
66 rfl
68end CoefficientBoundary
70section BoundaryMap
72variable {R : Type u} [Ring R]
73variable {X : Type v} [Fintype X]
75/--
76The finite Fox boundary map with prescribed generator boundary values sends a coordinate vector
77\(v : X \to R\) to \(\sum_x v(x)\,\mathrm{generatorBoundary}(x)\).
78-/
79def foxBoundaryMap (generatorBoundary : X → R) : (X → R) →ₗ[R] R where
80 toFun v := ∑ x : X, v x * generatorBoundary x
81 map_add' v w := by
82 simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
83 map_smul' r v := by
84 simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, RingHom.id_apply, Finset.mul_sum]
86/--
87The boundary map is evaluated on the canonical generators and then extended linearly to the
88coordinate module.
89-/
90theorem foxBoundaryMap_apply (generatorBoundary : X → R) (v : X → R) :
91 foxBoundaryMap generatorBoundary v =
92 ∑ x : X, v x * generatorBoundary x :=
93 rfl
95variable [DecidableEq X]
97/--
98The finite Fox boundary map sends a coordinate basis vector to the corresponding generator
99boundary.
100-/
101@[simp]
102theorem foxBoundaryMap_single (generatorBoundary : X → R) (x : X) :
103 foxBoundaryMap generatorBoundary (Pi.single x (1 : R)) = generatorBoundary x := by
104 rw [foxBoundaryMap_apply]
105 rw [Finset.sum_eq_single x]
106 · simp only [Pi.single_eq_same, one_mul]
107 · intro y _ hy
108 simp only [Pi.single_eq_of_ne hy, zero_mul]
109 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_mul, IsEmpty.forall_iff]
111end BoundaryMap
113section FreeGroup
115variable {R : Type u} [Ring R]
116variable {X : Type v} [Fintype X] [DecidableEq X]
117variable (coeff : FreeGroup X →* R)
118variable (generatorBoundary : X → R)
120/--
121Boundary-map form of the generic free-group Fox formula: applying the Fox boundary map to the
122free crossed differential recovers the crossed differential with the prescribed generator
123values.
124-/
125theorem foxBoundaryMap_freeCrossedHomWithCoeff
126 (boundary : ScalarCrossedHom coeff R)
127 (hgenerator : ∀ x : X, boundary (FreeGroup.of x) = generatorBoundary x)
128 (w : FreeGroup X) :
129 foxBoundaryMap generatorBoundary
130 (freeCrossedHomWithCoeff
131 (A := X → R) coeff (fun x : X => Pi.single x (1 : R)) w) =
132 boundary w := by
133 let delta : ScalarCrossedHom coeff R :=
134 ScalarCrossedHom.mapLinear
135 (freeCrossedHomWithCoeff
136 (A := X → R) coeff (fun x : X => Pi.single x (1 : R)))
137 (foxBoundaryMap generatorBoundary)
138 have hdelta_generator :
139 ∀ x : X, delta (FreeGroup.of x) = generatorBoundary x := by
140 intro x
141 simp only [delta, ScalarCrossedHom.mapLinear_apply, freeCrossedHomWithCoeff_of,
142 foxBoundaryMap_single]
143 have hdelta_eq :
144 delta = freeCrossedHomWithCoeff (A := R) coeff generatorBoundary :=
145 freeCrossedHomWithCoeff_unique
146 (A := R) coeff generatorBoundary delta hdelta_generator
147 have hboundary_eq :
148 boundary = freeCrossedHomWithCoeff (A := R) coeff generatorBoundary :=
149 freeCrossedHomWithCoeff_unique
150 (A := R) coeff generatorBoundary boundary hgenerator
151 change delta w = boundary w
152 rw [hdelta_eq, hboundary_eq]
154/--
155Conditional boundary-map form of the generic free-group Fox formula. Any crossed differential
156with standard coordinate values satisfies the same boundary formula as the canonical free
157crossed differential.
158-/
159theorem foxBoundaryMap_of_crossedHom
160 (delta : ScalarCrossedHom coeff (X → R))
161 (hdelta_generator :
162 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : R))
163 (boundary : ScalarCrossedHom coeff R)
164 (hboundary_generator :
165 ∀ x : X, boundary (FreeGroup.of x) = generatorBoundary x)
166 (w : FreeGroup X) :
167 foxBoundaryMap generatorBoundary (delta w) = boundary w := by
168 have hdelta_eq :
169 delta =
170 freeCrossedHomWithCoeff
171 (A := X → R) coeff (fun x : X => Pi.single x (1 : R)) :=
172 freeCrossedHomWithCoeff_unique
173 (A := X → R) coeff (fun x : X => Pi.single x (1 : R))
174 delta hdelta_generator
175 rw [hdelta_eq]
176 exact foxBoundaryMap_freeCrossedHomWithCoeff
177 coeff generatorBoundary boundary hboundary_generator w
179/--
180Explicit finite-sum form of the generic Fox--Euler formula for any crossed differential with
181standard coordinate values: \(\mathrm{coeff}(w)-1=\sum_x \delta_x(w)(\mathrm{coeff}(x)-1)\).
182-/
183theorem foxEulerFormula_of_crossedHom
184 (delta : ScalarCrossedHom coeff (X → R))
185 (hdelta_generator :
186 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : R))
187 (w : FreeGroup X) :
188 coeff w - 1 =
189 ∑ x : X, delta w x * (coeff (FreeGroup.of x) - 1) := by
190 have hboundary :=
191 foxBoundaryMap_of_crossedHom
192 coeff
193 (fun x : X => coefficientFoxBoundary coeff (FreeGroup.of x))
194 delta hdelta_generator
195 (coefficientFoxBoundaryCrossedHom coeff)
196 (by intro x; rfl)
197 w
198 simpa [coefficientFoxBoundary, foxBoundaryMap_apply] using hboundary.symm
200end FreeGroup
202end
204end FoxDifferential