Source: ProCGroups.FoxDifferential.Discrete.FoxCalculus.Boundary
1import ProCGroups.FoxDifferential.Common.FoxBoundary
2import ProCGroups.FoxDifferential.Discrete.DifferentialModule.Boundary
3import ProCGroups.FoxDifferential.Discrete.FoxCalculus.Universal
5/-!
6# Fox differential: discrete — fox calculus — boundary
8The principal declarations in this module are:
10- `relativeFreeGroupFoxBoundary`
11 The pushed-forward Fox boundary \(a \mapsto \sum_x a_x (\psi(x) - 1)\).
12- `relativeFreeGroupFoxBoundary_apply`
13 The relative free-group Fox boundary is evaluated on canonical generators and then extended
14 linearly to the coordinate module.
15- `relativeFreeGroupFoxBoundary_single`
16 The relative Fox boundary sends a coordinate basis vector to the corresponding augmentation
17 generator.
18- `toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap`
19 Composing the universal boundary with the coordinate-to-differential map gives the pushed-forward
20 Fox boundary.
21-/
23namespace FoxDifferential
25noncomputable section
27namespace FoxCalculus
29open scoped BigOperators
31universe u v
34variable {H : Type v} [Group H]
35variable (X : Type u)
37variable [DecidableEq X]
38variable (ψ : FreeGroup X →* H)
40variable [Fintype X]
42/-- The pushed-forward Fox boundary \(a \mapsto \sum_x a_x (\psi(x) - 1)\). -/
43def relativeFreeGroupFoxBoundary :
44 RelativeFreeFoxCoordinates (H := H) X →ₗ[GroupRing H] GroupRing H :=
45 { toFun := fun a =>
46 ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x))
47 map_add' := by
48 intro a b
49 simp only [Pi.add_apply, augmentationGenerator_eq_groupRingBoundary, add_mul,
50 Finset.sum_add_distrib]
51 map_smul' := by
52 intro r a
53 simp only [Pi.smul_apply, smul_eq_mul, augmentationGenerator_eq_groupRingBoundary, mul_assoc,
54 RingHom.id_apply, Finset.mul_sum]}
56omit [DecidableEq X] in
57/--
58The relative free-group Fox boundary is evaluated on canonical generators and then extended
59linearly to the coordinate module.
60-/
61theorem relativeFreeGroupFoxBoundary_apply
62 (a : RelativeFreeFoxCoordinates (H := H) X) :
63 relativeFreeGroupFoxBoundary (H := H) X ψ a =
64 ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x)) :=
65 rfl
67/--
68The relative Fox boundary sends a coordinate basis vector to the corresponding augmentation
69generator.
70-/
71@[simp]
72theorem relativeFreeGroupFoxBoundary_single (x : X) :
73 relativeFreeGroupFoxBoundary (H := H) X ψ
74 (Pi.single x (1 : GroupRing H)) =
75 augmentationGenerator H (ψ (FreeGroup.of x)) := by
76 rw [relativeFreeGroupFoxBoundary_apply]
77 rw [Finset.sum_eq_single x]
78 · simp only [Pi.single_eq_same, augmentationGenerator_eq_groupRingBoundary, one_mul]
79 · intro y _ hy
80 simp only [Pi.single_eq_of_ne hy, augmentationGenerator_eq_groupRingBoundary, zero_mul]
81 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same,
82 augmentationGenerator_eq_groupRingBoundary,
83 one_mul, IsEmpty.forall_iff]
85omit [DecidableEq X] in
86/--
87Composing the universal boundary with the coordinate-to-differential map gives the
88pushed-forward Fox boundary.
89-/
90theorem toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap :
91 (toGroupRing ψ).comp
92 (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ) =
93 relativeFreeGroupFoxBoundary (H := H) X ψ := by
94 apply LinearMap.ext
95 intro a
96 change
97 toGroupRing ψ
98 (∑ x : X, a x • universalDifferential ψ (FreeGroup.of x)) =
99 ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x))
100 rw [map_sum]
101 apply Finset.sum_congr rfl
102 intro x _hx
103 rw [map_smul, toGroupRing_d]
104 rfl
106/--
107Relative Fox fundamental formula, also known as the Fox--Euler formula: \(\psi(w) - 1 = \sum_x
108(\partial w/\partial x) (\psi(x) - 1)\).
109-/
110theorem relativeFreeGroupFoxDerivative_fundamental_formula (w : FreeGroup X) :
111 groupRingBoundary ψ w =
112 ∑ x : X,
113 relativeFreeGroupFoxDerivative (H := H) X ψ w x *
114 augmentationGenerator H (ψ (FreeGroup.of x)) := by
115 have h :=
116 LinearMap.congr_fun
117 (toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap (H := H) X ψ)
118 (relativeFreeGroupFoxDerivative (H := H) X ψ w)
119 rw [LinearMap.comp_apply, relativeFreeFoxCoordinatesLinearMap_derivative,
120 toGroupRing_d] at h
121 simpa [relativeFreeGroupFoxBoundary] using h
123/-- Fox boundary form of the relative Fox fundamental formula. -/
124theorem relativeFreeGroupFoxBoundary_derivative (w : FreeGroup X) :
125 relativeFreeGroupFoxBoundary (H := H) X ψ
126 (relativeFreeGroupFoxDerivative (H := H) X ψ w) =
127 groupRingBoundary ψ w := by
128 simpa [relativeFreeGroupFoxBoundary_apply] using
129 (relativeFreeGroupFoxDerivative_fundamental_formula (H := H) X ψ w).symm
131/--
132Conditional relative Fox boundary formula. Any differential map on a free group with the
133standard coordinate values satisfies the relative Fox boundary formula.
134-/
135theorem relativeFreeGroupFoxBoundary_of_crossedHom
136 (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
137 (hbasis :
138 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H))
139 (w : FreeGroup X) :
140 relativeFreeGroupFoxBoundary (H := H) X ψ (delta w) = groupRingBoundary ψ w := by
141 have hdelta_eq : delta = relativeFreeGroupFoxHom (H := H) X ψ :=
142 relativeFreeGroupFoxHom_unique (H := H) X ψ delta hbasis
143 rw [hdelta_eq]
144 exact relativeFreeGroupFoxBoundary_derivative (H := H) X ψ w
146/--
147Conditional relative Fox fundamental formula. The Fox-Euler sum computed from any differential
148map with standard coordinate values is \([\psi(w)]-1\).
149-/
150theorem relativeFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
151 (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
152 (hbasis :
153 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H))
154 (w : FreeGroup X) :
155 groupRingBoundary ψ w =
156 ∑ x : X, delta w x * augmentationGenerator H (ψ (FreeGroup.of x)) := by
157 simpa [relativeFreeGroupFoxBoundary_apply] using
158 (relativeFreeGroupFoxBoundary_of_crossedHom (H := H) X ψ delta hbasis w).symm
160/-- Explicit \(\psi(w)-1\) version of the conditional relative Fox-Euler formula. -/
161theorem relativeFreeGroupFoxDerivative_euler_formula_of_crossedHom
162 (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
163 (hbasis :
164 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H))
165 (w : FreeGroup X) :
166 (MonoidAlgebra.of ℤ H (ψ w) : GroupRing H) - 1 =
167 ∑ x : X, delta w x * augmentationGenerator H (ψ (FreeGroup.of x)) := by
168 simpa [groupRingBoundary] using
169 relativeFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
170 (H := H) X ψ delta hbasis w
172/-- Explicit \(\psi(w)-1\) version of the relative Fox--Euler formula. -/
173theorem relativeFreeGroupFoxDerivative_euler_formula (w : FreeGroup X) :
174 (MonoidAlgebra.of ℤ H (ψ w) : GroupRing H) - 1 =
175 ∑ x : X,
176 relativeFreeGroupFoxDerivative (H := H) X ψ w x *
177 augmentationGenerator H (ψ (FreeGroup.of x)) := by
178 simpa [groupRingBoundary] using
179 relativeFreeGroupFoxDerivative_fundamental_formula (H := H) X ψ w
181end FoxCalculus
183end
185end FoxDifferential