FoxDifferential.Completed.ProCIntegerCoefficients.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 zcFreeGroupFoxBoundary_derivativeVector
(ψ : FreeGroup X →* H) (w : FreeGroup X) :
zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w) =
zcCompletedGroupAlgebraBoundary C ψ wThe boundary-map form of the completed Fox fundamental formula.
Show proof
by
let beta : FreeGroup X → ZCCompletedGroupAlgebra C H :=
fun w => zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w)
have hbeta :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) beta :=
IsCrossedDifferential.map_linear
(zcFreeGroupFoxDerivativeVector_isCrossedDifferential C ψ)
(zcFreeGroupFoxBoundary C ψ)
have hbasis :
∀ x : X, beta (FreeGroup.of x) =
zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x) := by
intro x
simp only [zcFreeGroupFoxDerivativeVector_of, zcFreeGroupFoxBoundary_single, beta]
have hbeta_eq :
beta =
freeCrossedDifferentialWithCoeff
(A := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x)) := by
exact freeCrossedDifferentialWithCoeff_unique
(A := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x))
beta hbeta hbasis
have hboundary_eq :
zcCompletedGroupAlgebraBoundary C ψ =
freeCrossedDifferentialWithCoeff
(A := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x)) := by
exact freeCrossedDifferentialWithCoeff_unique
(A := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of x))
(zcCompletedGroupAlgebraBoundary C ψ)
(zcCompletedGroupAlgebraBoundary_isCrossedDifferential C ψ)
(by intro x; rfl)
exact congrFun (hbeta_eq.trans hboundary_eq.symm) wProof. Construct the completed free-group Fox coordinates by projecting to every finite \(\mathbb{Z}_C\)-coefficient and finite target quotient stage. The generator values define the derivative vector, and the crossed-differential rule gives product, inverse, Jacobian, chain-rule, and fundamental-formula identities at each finite stage. Compatibility of the stage formulas under refinement gives the completed derivative or matrix, and uniqueness follows from finite-stage projection extensionality.
□theorem zcFreeGroupFoxBoundary_of_crossedDifferential
(ψ : FreeGroup X →* H)
(delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H))
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hbasis :
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H))
(w : FreeGroup X) :
zcFreeGroupFoxBoundary C ψ (delta w) =
zcCompletedGroupAlgebraBoundary C ψ wConditional completed Fox boundary formula. Any completed crossed differential on a free group with the standard basis values satisfies the completed Fox boundary formula.
Show proof
by
have hdelta_eq :
delta = zcFreeGroupFoxDerivativeVector C ψ :=
zcFreeGroupFoxDerivativeVector_unique C ψ delta hdelta hbasis
rw [hdelta_eq]
exact zcFreeGroupFoxBoundary_derivativeVector C ψ wProof. Construct the completed free-group Fox coordinates by projecting to every finite \(\mathbb{Z}_C\)-coefficient and finite target quotient stage. The generator values define the derivative vector, and the crossed-differential rule gives product, inverse, Jacobian, chain-rule, and fundamental-formula identities at each finite stage. Compatibility of the stage formulas under refinement gives the completed derivative or matrix, and uniqueness follows from finite-stage projection extensionality.
□theorem zcFreeGroupFoxDerivative_fundamental_formula_of_crossedDifferential
(ψ : FreeGroup X →* H)
(delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H))
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hbasis :
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H))
(w : FreeGroup X) :
zcCompletedGroupAlgebraBoundary C ψ w =
∑ i : X,
delta w i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)Conditional completed Fox fundamental formula. The finite Fox-Euler sum computed from any completed crossed differential with standard basis values is \([\psi(w)]-1\).
Show proof
by
simpa [zcFreeGroupFoxBoundary_apply] using
(zcFreeGroupFoxBoundary_of_crossedDifferential C ψ delta hdelta hbasis w).symmProof. Construct the completed free-group Fox coordinates by projecting to every finite \(\mathbb{Z}_C\)-coefficient and finite target quotient stage. The generator values define the derivative vector, and the crossed-differential rule gives product, inverse, Jacobian, chain-rule, and fundamental-formula identities at each finite stage. Compatibility of the stage formulas under refinement gives the completed derivative or matrix, and uniqueness follows from finite-stage projection extensionality.
□theorem zcFreeGroupFoxDerivative_euler_formula_of_crossedDifferential
(ψ : FreeGroup X →* H)
(delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H))
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hbasis :
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H))
(w : FreeGroup X) :
zcGroupLike C H (ψ w) - 1 =
∑ i : X,
delta w i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)The explicit \([\psi(w)]-1\) form of the conditional completed Fox-Euler formula.
Show proof
by
simpa [zcCompletedGroupAlgebraBoundary] using
zcFreeGroupFoxDerivative_fundamental_formula_of_crossedDifferential
C ψ delta hdelta hbasis wProof. Construct the completed free-group Fox coordinates by projecting to every finite \(\mathbb{Z}_C\)-coefficient and finite target quotient stage. The generator values define the derivative vector, and the crossed-differential rule gives product, inverse, Jacobian, chain-rule, and fundamental-formula identities at each finite stage. Compatibility of the stage formulas under refinement gives the completed derivative or matrix, and uniqueness follows from finite-stage projection extensionality.
□theorem zcFreeGroupFoxDerivative_fundamental_formula
(ψ : FreeGroup X →* H) (w : FreeGroup X) :
zcCompletedGroupAlgebraBoundary C ψ w =
∑ i : X,
zcFreeGroupFoxDerivative C ψ i w *
(zcGroupLike C H (ψ (FreeGroup.of i)) - 1)The completed Fox fundamental formula, also known as the completed Fox-Euler formula: \([\psi(w)]-1 = \sum_i (\partial w/\partial x_i)([\psi(x_i)]-1)\).
Show proof
by
simpa [zcFreeGroupFoxBoundary_apply, zcFreeGroupFoxDerivative] using
(zcFreeGroupFoxBoundary_derivativeVector C ψ w).symmProof. Construct the completed free-group Fox coordinates by projecting to every finite \(\mathbb{Z}_C\)-coefficient and finite target quotient stage. The generator values define the derivative vector, and the crossed-differential rule gives product, inverse, Jacobian, chain-rule, and fundamental-formula identities at each finite stage. Compatibility of the stage formulas under refinement gives the completed derivative or matrix, and uniqueness follows from finite-stage projection extensionality.
□theorem zcFreeGroupFoxDerivative_euler_formula
(ψ : FreeGroup X →* H) (w : FreeGroup X) :
zcGroupLike C H (ψ w) - 1 =
∑ i : X,
zcFreeGroupFoxDerivative C ψ i w *
(zcGroupLike C H (ψ (FreeGroup.of i)) - 1)The explicit \([\psi(w)]-1\) form of the completed Fox-Euler formula.
Show proof
by
simpa [zcCompletedGroupAlgebraBoundary] using
zcFreeGroupFoxDerivative_fundamental_formula C ψ wProof. Construct the completed free-group Fox coordinates by projecting to every finite \(\mathbb{Z}_C\)-coefficient and finite target quotient stage. The generator values define the derivative vector, and the crossed-differential rule gives product, inverse, Jacobian, chain-rule, and fundamental-formula identities at each finite stage. Compatibility of the stage formulas under refinement gives the completed derivative or matrix, and uniqueness follows from finite-stage projection extensionality.
□