Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental
1import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Coordinates
3/-!
4# Fox differential: completed — \(\mathbb{Z}_C\) coefficients — free group — fundamental
6The principal declarations in this module are:
8- `zcFreeGroupFoxBoundary_derivativeVector`
9 The boundary-map form of the completed Fox fundamental formula.
10- `zcFreeGroupFoxBoundary_of_crossedHom`
11 Conditional completed Fox boundary formula. Any completed crossed differential on a free group
12 with the standard basis values satisfies the completed Fox boundary formula.
13- `zcFreeGroupFoxDerivative_fundamental_formula_of_crossedHom`
14 Conditional completed Fox fundamental formula. The finite Fox-Euler sum computed from any
15 completed crossed differential with standard basis values is \([\psi(w)]-1\).
16- `zcFreeGroupFoxDerivative_euler_formula_of_crossedHom`
17 The explicit \([\psi(w)]-1\) form of the conditional completed Fox-Euler formula.
18-/
20namespace FoxDifferential
22noncomputable section
24open scoped BigOperators
26universe u v
29variable (C : ProCGroups.FiniteGroupClass.{v})
30variable {X : Type u} [DecidableEq X]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33section FiniteBasis
35variable [Fintype X]
37/-- The boundary-map form of the completed Fox fundamental formula. -/
38theorem zcFreeGroupFoxBoundary_derivativeVector
39 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
40 zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w) =
41 zcCompletedGroupAlgebraBoundary C ψ w := by
42 let beta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
43 (ZCCompletedGroupAlgebra C H) :=
44 (zcFreeGroupFoxDerivativeVector C ψ).mapLinear
45 (zcFreeGroupFoxBoundary C ψ)
46 have hbasis :
47 ∀ x : X, beta (FreeGroup.of x) =
48 zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x) := by
49 intro x
50 change zcFreeGroupFoxBoundary C ψ
51 (zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of x)) =
52 zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x)
53 rw [zcFreeGroupFoxDerivativeVector_of, zcFreeGroupFoxBoundary_single]
54 have hbeta_eq :
55 beta =
56 freeCrossedHomWithCoeff
57 (A := ZCCompletedGroupAlgebra C H)
58 (zcCompletedGroupAlgebraScalar C ψ)
59 (fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x)) := by
60 exact freeCrossedHomWithCoeff_unique
61 (A := ZCCompletedGroupAlgebra C H)
62 (zcCompletedGroupAlgebraScalar C ψ)
63 (fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x))
64 beta hbasis
65 have hboundary_eq :
66 zcCompletedGroupAlgebraBoundary C ψ =
67 freeCrossedHomWithCoeff
68 (A := ZCCompletedGroupAlgebra C H)
69 (zcCompletedGroupAlgebraScalar C ψ)
70 (fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x)) := by
71 exact freeCrossedHomWithCoeff_unique
72 (A := ZCCompletedGroupAlgebra C H)
73 (zcCompletedGroupAlgebraScalar C ψ)
74 (fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x))
75 (zcCompletedGroupAlgebraBoundary C ψ) (by intro x; rfl)
76 exact congrArg
77 (fun d : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
78 (ZCCompletedGroupAlgebra C H) => d w)
79 (hbeta_eq.trans hboundary_eq.symm)
81/--
82Conditional completed Fox boundary formula. Any completed crossed differential on a free group
83with the standard basis values satisfies the completed Fox boundary formula.
84-/
85theorem zcFreeGroupFoxBoundary_of_crossedHom
86 (ψ : FreeGroup X →* H)
87 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
88 (ZCFreeFoxCoordinates C (X := X) (H := H)))
89 (hbasis :
90 ∀ x : X, delta (FreeGroup.of x) =
91 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
92 (w : FreeGroup X) :
93 zcFreeGroupFoxBoundary C ψ (delta w) =
94 zcCompletedGroupAlgebraBoundary C ψ w := by
95 have hdelta_eq :
96 delta = zcFreeGroupFoxDerivativeVector C ψ :=
97 zcFreeGroupFoxDerivativeVector_unique C ψ delta hbasis
98 rw [hdelta_eq]
99 exact zcFreeGroupFoxBoundary_derivativeVector C ψ w
101/--
102Conditional completed Fox fundamental formula. The finite Fox-Euler sum computed from any
103completed crossed differential with standard basis values is \([\psi(w)]-1\).
104-/
105theorem zcFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
106 (ψ : FreeGroup X →* H)
107 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
108 (ZCFreeFoxCoordinates C (X := X) (H := H)))
109 (hbasis :
110 ∀ x : X, delta (FreeGroup.of x) =
111 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
112 (w : FreeGroup X) :
113 zcCompletedGroupAlgebraBoundary C ψ w =
114 ∑ i : X,
115 delta w i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
116 simpa [zcFreeGroupFoxBoundary_apply] using
117 (zcFreeGroupFoxBoundary_of_crossedHom C ψ delta hbasis w).symm
119/-- The explicit \([\psi(w)]-1\) form of the conditional completed Fox-Euler formula. -/
120theorem zcFreeGroupFoxDerivative_euler_formula_of_crossedHom
121 (ψ : FreeGroup X →* H)
122 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
123 (ZCFreeFoxCoordinates C (X := X) (H := H)))
124 (hbasis :
125 ∀ x : X, delta (FreeGroup.of x) =
126 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
127 (w : FreeGroup X) :
128 zcGroupLike C H (ψ w) - 1 =
129 ∑ i : X,
130 delta w i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
131 have h := zcFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
132 C ψ delta hbasis w
133 change zcGroupLike C H (ψ w) - 1 = _ at h
134 exact h
136/--
137The completed Fox fundamental formula, also known as the completed Fox-Euler formula:
138\([\psi(w)]-1 = \sum_i (\partial w/\partial x_i)([\psi(x_i)]-1)\).
139-/
140theorem zcFreeGroupFoxDerivative_fundamental_formula
141 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
142 zcCompletedGroupAlgebraBoundary C ψ w =
143 ∑ i : X,
144 zcFreeGroupFoxDerivative C ψ i w *
145 (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
146 simpa [zcFreeGroupFoxBoundary_apply, zcFreeGroupFoxDerivative] using
147 (zcFreeGroupFoxBoundary_derivativeVector C ψ w).symm
149/-- The explicit \([\psi(w)]-1\) form of the completed Fox-Euler formula. -/
150theorem zcFreeGroupFoxDerivative_euler_formula
151 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
152 zcGroupLike C H (ψ w) - 1 =
153 ∑ i : X,
154 zcFreeGroupFoxDerivative C ψ i w *
155 (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) := by
156 have h := zcFreeGroupFoxDerivative_fundamental_formula C ψ w
157 change zcGroupLike C H (ψ w) - 1 = _ at h
158 exact h
161end FiniteBasis
164end
166end FoxDifferential