FoxDifferential.Completed.Residue.FreeGroup.Fundamental
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
theorem residueFreeGroupFoxBoundary_derivativeVector
(n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
residueFreeGroupFoxBoundary n ψ
(residueFreeGroupFoxDerivativeVector n ψ w) =
residueGroupRingBoundary n ψ wBoundary-map form of the residue Fox fundamental formula.
Show proof
by
let beta : FreeGroup X → ResidueGroupRing n H :=
fun w => residueFreeGroupFoxBoundary n ψ (residueFreeGroupFoxDerivativeVector n ψ w)
have hbeta :
IsCrossedDifferential (residueGroupRingScalar n ψ) beta :=
IsCrossedDifferential.map_linear
(residueFreeGroupFoxDerivativeVector_isCrossedDifferential n ψ)
(residueFreeGroupFoxBoundary n ψ)
have hbasis :
∀ x : X, beta (FreeGroup.of x) =
residueGroupRingBoundary n ψ (FreeGroup.of x) := by
intro x
simp only [residueFreeGroupFoxDerivativeVector_of, residueFreeGroupFoxBoundary_single, beta]
have hbeta_eq :
beta =
freeCrossedDifferentialWithCoeff
(A := ResidueGroupRing n H)
(residueGroupRingScalar n ψ)
(fun x => residueGroupRingBoundary n ψ (FreeGroup.of x)) := by
exact freeCrossedDifferentialWithCoeff_unique
(A := ResidueGroupRing n H)
(residueGroupRingScalar n ψ)
(fun x => residueGroupRingBoundary n ψ (FreeGroup.of x))
beta hbeta hbasis
have hboundary_eq :
residueGroupRingBoundary n ψ =
freeCrossedDifferentialWithCoeff
(A := ResidueGroupRing n H)
(residueGroupRingScalar n ψ)
(fun x => residueGroupRingBoundary n ψ (FreeGroup.of x)) := by
exact freeCrossedDifferentialWithCoeff_unique
(A := ResidueGroupRing n H)
(residueGroupRingScalar n ψ)
(fun x => residueGroupRingBoundary n ψ (FreeGroup.of x))
(residueGroupRingBoundary n ψ)
(residueGroupRingBoundary_isCrossedDifferential n ψ)
(by intro x; rfl)
exact congrFun (hbeta_eq.trans hboundary_eq.symm) wProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□theorem residueFreeGroupFoxBoundary_of_crossedDifferential
(n : ℕ) (ψ : FreeGroup X →* H)
(delta : FreeGroup X → ResidueFreeFoxCoordinates n H X)
(hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta)
(hbasis :
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : ResidueGroupRing n H))
(w : FreeGroup X) :
residueFreeGroupFoxBoundary n ψ (delta w) =
residueGroupRingBoundary n ψ wAny residue crossed differential on a free group with the standard basis values satisfies the conditional residue Fox boundary formula.
Show proof
by
have hdelta_eq :
delta = residueFreeGroupFoxDerivativeVector n ψ :=
residueFreeGroupFoxDerivativeVector_unique n ψ delta hdelta hbasis
rw [hdelta_eq]
exact residueFreeGroupFoxBoundary_derivativeVector n ψ wProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□theorem residueFreeGroupFoxDerivative_fundamental_formula_of_crossedDifferential
(n : ℕ) (ψ : FreeGroup X →* H)
(delta : FreeGroup X → ResidueFreeFoxCoordinates n H X)
(hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta)
(hbasis :
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : ResidueGroupRing n H))
(w : FreeGroup X) :
residueGroupRingBoundary n ψ w =
∑ i : X,
delta w i *
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)Conditional residue Fox fundamental formula. The residue Fox-Euler sum computed from any residue crossed differential with standard basis values is \([\psi(w)]-1\).
Show proof
by
simpa [residueFreeGroupFoxBoundary_apply] using
(residueFreeGroupFoxBoundary_of_crossedDifferential n ψ delta hdelta hbasis w).symmProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□theorem residueFreeGroupFoxDerivative_euler_formula_of_crossedDifferential
(n : ℕ) (ψ : FreeGroup X →* H)
(delta : FreeGroup X → ResidueFreeFoxCoordinates n H X)
(hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta)
(hbasis :
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : ResidueGroupRing n H))
(w : FreeGroup X) :
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) : ResidueGroupRing n H) - 1 =
∑ i : X,
delta w i *
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)The explicit \([\psi(w)]-1\) form of the conditional residue Fox-Euler formula.
Show proof
by
simpa [residueGroupRingBoundary] using
residueFreeGroupFoxDerivative_fundamental_formula_of_crossedDifferential
n ψ delta hdelta hbasis wProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□theorem residueFreeGroupFoxDerivative_fundamental_formula
(n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
residueGroupRingBoundary n ψ w =
∑ i : X,
residueFreeGroupFoxDerivative n ψ i w *
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)The residue Fox fundamental formula, also known as the residue Fox-Euler formula: \([\psi(w)]-1 = \sum_i (\partial w/\partial x_i)([\psi(x_i)]-1)\).
Show proof
by
simpa [residueFreeGroupFoxBoundary_apply, residueFreeGroupFoxDerivative] using
(residueFreeGroupFoxBoundary_derivativeVector n ψ w).symmProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□theorem residueFreeGroupFoxDerivative_euler_formula
(n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) : ResidueGroupRing n H) - 1 =
∑ i : X,
residueFreeGroupFoxDerivative n ψ i w *
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)The explicit \([\psi(w)]-1\) form of the residue Fox-Euler formula.
Show proof
by
simpa [residueGroupRingBoundary] using
residueFreeGroupFoxDerivative_fundamental_formula n ψ wProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□