Source: ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Fundamental
1import ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Boundary
3/-!
4# Fox differential: completed — residue — free group — fundamental
6The principal declarations in this module are:
8- `residueFreeGroupFoxBoundary_derivativeVector`
9 Boundary-map form of the residue Fox fundamental formula.
10- `residueFreeGroupFoxBoundary_of_crossedHom`
11 Any residue crossed homomorphism with the standard basis values satisfies the residue Fox boundary
12 formula.
13- `residueFreeGroupFoxDerivative_fundamental_formula_of_crossedHom`
14 The residue Fox-Euler sum computed from a crossed homomorphism with standard basis values is
15 \([\psi(w)]-1\).
16- `residueFreeGroupFoxDerivative_euler_formula_of_crossedHom`
17 The explicit \([\psi(w)]-1\) form of the residue Fox-Euler formula for a crossed homomorphism.
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/-- Boundary-map form of the residue Fox fundamental formula. -/
36theorem residueFreeGroupFoxBoundary_derivativeVector
37 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
38 residueFreeGroupFoxBoundary n ψ
39 (residueFreeGroupFoxDerivativeVector n ψ w) =
40 residueGroupRingBoundary n ψ w := by
41 let beta : ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueGroupRing n H) :=
42 (residueFreeGroupFoxDerivativeVector n ψ).mapLinear
43 (residueFreeGroupFoxBoundary n ψ)
44 have hbasis :
45 ∀ x : X, beta (FreeGroup.of x) =
46 residueGroupRingBoundary n ψ (FreeGroup.of x) := by
47 intro x
48 simp only [beta, ScalarCrossedHom.mapLinear_apply,
49 residueFreeGroupFoxDerivativeVector_of, residueFreeGroupFoxBoundary_single]
50 have hbeta_eq :
51 beta =
52 freeCrossedHomWithCoeff
53 (A := ResidueGroupRing n H)
54 (residueGroupRingScalar n ψ)
55 (fun x => residueGroupRingBoundary n ψ (FreeGroup.of x)) := by
56 exact freeCrossedHomWithCoeff_unique
57 (A := ResidueGroupRing n H)
58 (residueGroupRingScalar n ψ)
59 (fun x => residueGroupRingBoundary n ψ (FreeGroup.of x)) beta hbasis
60 have hboundary_eq :
61 residueGroupRingBoundary n ψ =
62 freeCrossedHomWithCoeff
63 (A := ResidueGroupRing n H)
64 (residueGroupRingScalar n ψ)
65 (fun x => residueGroupRingBoundary n ψ (FreeGroup.of x)) := by
66 exact freeCrossedHomWithCoeff_unique
67 (A := ResidueGroupRing n H)
68 (residueGroupRingScalar n ψ)
69 (fun x => residueGroupRingBoundary n ψ (FreeGroup.of x))
70 (residueGroupRingBoundary n ψ) (by intro x; rfl)
71 exact congrArg
72 (fun d : ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueGroupRing n H) => d w)
73 (hbeta_eq.trans hboundary_eq.symm)
75/--
76Any residue crossed homomorphism with the standard basis values satisfies the residue Fox
77boundary formula.
78-/
79theorem residueFreeGroupFoxBoundary_of_crossedHom
80 (n : ℕ) (ψ : FreeGroup X →* H)
81 (delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
82 (ResidueFreeFoxCoordinates n H X))
83 (hbasis :
84 ∀ x : X, delta (FreeGroup.of x) =
85 Pi.single x (1 : ResidueGroupRing n H))
86 (w : FreeGroup X) :
87 residueFreeGroupFoxBoundary n ψ (delta w) =
88 residueGroupRingBoundary n ψ w := by
89 have hdelta_eq :
90 delta = residueFreeGroupFoxDerivativeVector n ψ :=
91 residueFreeGroupFoxDerivativeVector_unique n ψ delta hbasis
92 rw [hdelta_eq]
93 exact residueFreeGroupFoxBoundary_derivativeVector n ψ w
95/--
96The residue Fox-Euler sum computed from a crossed homomorphism with standard basis values is
97\([\psi(w)]-1\).
98-/
99theorem residueFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
100 (n : ℕ) (ψ : FreeGroup X →* H)
101 (delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
102 (ResidueFreeFoxCoordinates n H X))
103 (hbasis :
104 ∀ x : X, delta (FreeGroup.of x) =
105 Pi.single x (1 : ResidueGroupRing n H))
106 (w : FreeGroup X) :
107 residueGroupRingBoundary n ψ w =
108 ∑ i : X,
109 delta w i *
110 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) := by
111 simpa [residueFreeGroupFoxBoundary_apply] using
112 (residueFreeGroupFoxBoundary_of_crossedHom n ψ delta hbasis w).symm
114/--
115The explicit \([\psi(w)]-1\) form of the residue Fox-Euler formula for a crossed homomorphism.
116-/
117theorem residueFreeGroupFoxDerivative_euler_formula_of_crossedHom
118 (n : ℕ) (ψ : FreeGroup X →* H)
119 (delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
120 (ResidueFreeFoxCoordinates n H X))
121 (hbasis :
122 ∀ x : X, delta (FreeGroup.of x) =
123 Pi.single x (1 : ResidueGroupRing n H))
124 (w : FreeGroup X) :
125 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) : ResidueGroupRing n H) - 1 =
126 ∑ i : X,
127 delta w i *
128 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) := by
129 have h := residueFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
130 n ψ delta hbasis w
131 change (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) :
132 ResidueGroupRing n H) - 1 = _ at h
133 exact h
135/--
136The residue Fox fundamental formula, also known as the residue Fox-Euler formula: \([\psi(w)]-1
137= \sum_i (\partial w/\partial x_i)([\psi(x_i)]-1)\).
138-/
139theorem residueFreeGroupFoxDerivative_fundamental_formula
140 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
141 residueGroupRingBoundary n ψ w =
142 ∑ i : X,
143 residueFreeGroupFoxDerivative n ψ i w *
144 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) := by
145 simpa [residueFreeGroupFoxBoundary_apply, residueFreeGroupFoxDerivative] using
146 (residueFreeGroupFoxBoundary_derivativeVector n ψ w).symm
148/-- The explicit \([\psi(w)]-1\) form of the residue Fox-Euler formula. -/
149theorem residueFreeGroupFoxDerivative_euler_formula
150 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
151 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) : ResidueGroupRing n H) - 1 =
152 ∑ i : X,
153 residueFreeGroupFoxDerivative n ψ i w *
154 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) := by
155 have h := residueFreeGroupFoxDerivative_fundamental_formula n ψ w
156 change (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) :
157 ResidueGroupRing n H) - 1 = _ at h
158 exact h
160end FiniteBasis
163end
165end FoxDifferential