FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Derivative
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
import
abbrev ZCFreeFoxCoordinates : Type (max u v) :=
X → ZCCompletedGroupAlgebra C HCompleted Fox-coordinate vectors with coefficients in \(\mathbb{Z}_C\llbracket H\rrbracket\).
def zcFreeGroupFoxDerivativeVector (ψ : FreeGroup X →* H) (w : FreeGroup X) :
ZCFreeFoxCoordinates C (X := X) (H := H) :=
freeCrossedDifferentialWithCoeff
(A := ZCFreeFoxCoordinates C (X := X) (H := H))
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))
wCompleted free-group Fox derivative vector, with coefficients pushed forward along \(\psi:\mathrm{FreeGroup}(X)\to H\).
def zcFreeGroupFoxDerivative (ψ : FreeGroup X →* H) (i : X)
(w : FreeGroup X) : ZCCompletedGroupAlgebra C H :=
zcFreeGroupFoxDerivativeVector C ψ w iA coordinate of the completed free-group Fox derivative.
theorem zcFreeGroupFoxDerivativeVector_one (ψ : FreeGroup X →* H) :
zcFreeGroupFoxDerivativeVector C ψ (1 : FreeGroup X) = 0The completed free-group derivative vector sends the identity word to zero.
Show proof
by
simp only [zcFreeGroupFoxDerivativeVector, freeCrossedDifferentialWithCoeff_one]Proof. 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 zcFreeGroupFoxDerivativeVector_of (ψ : FreeGroup X →* H) (x : X) :
zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H)The completed free-group derivative vector sends a free generator to the corresponding coordinate basis vector.
Show proof
by
simp only [zcFreeGroupFoxDerivativeVector, freeCrossedDifferentialWithCoeff_of]Proof. 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 zcFreeGroupFoxDerivativeVector_mul
(ψ : FreeGroup X →* H) (u v : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C ψ (u * v) =
zcFreeGroupFoxDerivativeVector C ψ u +
zcCompletedGroupAlgebraScalar C ψ u • zcFreeGroupFoxDerivativeVector C ψ vProduct rule for the completed free-group derivative vector.
Show proof
by
exact freeCrossedDifferentialWithCoeff_mul
(A := ZCFreeFoxCoordinates C (X := X) (H := H))
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H)) u vProof. 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 zcFreeGroupFoxDerivativeVector_isCrossedDifferential
(ψ : FreeGroup X →* H) :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C ψ) (zcFreeGroupFoxDerivativeVector C ψ)The completed free-group derivative vector is a crossed differential.
Show proof
by
exact freeCrossedDifferentialWithCoeff_isCrossedDifferential
(A := ZCFreeFoxCoordinates C (X := X) (H := H))
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))Proof. 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 freeCrossedDifferentialWithCoeffCoordinates_eq_zcFreeGroupFoxDerivativeVector
(ψ : FreeGroup X →* H) (w : FreeGroup X) :
freeCrossedDifferentialWithCoeffCoordinates
(X := X) (zcCompletedGroupAlgebraScalar C ψ) w =
zcFreeGroupFoxDerivativeVector C ψ wThe coefficient-generic coordinate crossed differential specializes to the completed free-group Fox derivative vector.
Show proof
rflProof. 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 zcCrossedDifferential_comp_zcFreeGroupFoxDerivative
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(delta : FreeGroup Y → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(w : FreeGroup X) :
delta (φ w) =
∑ x : X,
zcFreeGroupFoxDerivative C (ψ.comp φ) x w •
delta (φ (FreeGroup.of x))Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) abstract Fox chain rule for an arbitrary crossed differential.
Show proof
by
calc
delta (φ w) =
freeCrossedDifferentialWithCoeffExpansion
(X := X) (zcCompletedGroupAlgebraScalar C (ψ.comp φ))
(fun x : X => delta (φ (FreeGroup.of x))) w := by
exact freeCrossedDifferentialWithCoeff_comp_expansion
(X := X) (Y := Y) (B := A)
(zcCompletedGroupAlgebraScalar C ψ) φ delta hdelta w
_ =
∑ x : X,
zcFreeGroupFoxDerivative C (ψ.comp φ) x w •
delta (φ (FreeGroup.of x)) := by
rw [freeCrossedDifferentialWithCoeffExpansion,
freeCrossedDifferentialWithCoeffExpansionLinearMap_apply,
freeCrossedDifferentialWithCoeffCoordinates_eq_zcFreeGroupFoxDerivativeVector
C (ψ.comp φ) w]
rflProof. 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.
□def zcFreeGroupHomFoxJacobian
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
X → Y → ZCCompletedGroupAlgebra C H :=
freeCrossedDifferentialWithCoeffJacobian
(X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φCompleted \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian of a homomorphism of free groups.
theorem zcFreeGroupHomFoxJacobian_apply
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(x : X) (y : Y) :
zcFreeGroupHomFoxJacobian C ψ φ x y =
zcFreeGroupFoxDerivative C ψ y (φ (FreeGroup.of x))The completed Fox-Jacobian of a free-group homomorphism is evaluated by taking the completed Fox derivative vector of the image of a generator.
Show proof
rflProof. 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.
□def zcFreeGroupHomFoxJacobianMatrix
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
Matrix X Y (ZCCompletedGroupAlgebra C H) :=
freeCrossedDifferentialWithCoeffJacobianMatrix
(X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φThe completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian is packaged as a matrix.
theorem zcFreeGroupHomFoxJacobianMatrix_apply
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(x : X) (y : Y) :
zcFreeGroupHomFoxJacobianMatrix C ψ φ x y =
zcFreeGroupHomFoxJacobian C ψ φ x yThe matrix evaluation is componentwise the completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian.
Show proof
rflProof. 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.
□def zcFreeGroupHomFoxJacobianLinearMap
[Fintype X]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
ZCFreeFoxCoordinates C (X := Y) (H := H) :=
freeCrossedDifferentialWithCoeffJacobianLinearMap
(X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φThe completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian is bundled into a finite linear map on coordinate vectors.
theorem zcFreeGroupHomFoxJacobianLinearMap_apply
[Fintype X]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(v : ZCFreeFoxCoordinates C (X := X) (H := H)) (y : Y) :
zcFreeGroupHomFoxJacobianLinearMap C ψ φ v y =
∑ x : X, v x * zcFreeGroupHomFoxJacobian C ψ φ x yEvaluation formula for the completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian linear map.
Show proof
rflProof. 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 zcFreeGroupHomFoxJacobianLinearMap_eq_vecMul
[Fintype X]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
zcFreeGroupHomFoxJacobianLinearMap C ψ φ v =
Matrix.vecMul v (zcFreeGroupHomFoxJacobianMatrix C ψ φ)The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian linear map is row-vector multiplication by its matrix.
Show proof
by
exact freeCrossedDifferentialWithCoeffJacobianLinearMap_eq_vecMul
(X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ vProof. 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 zcFreeGroupHomFoxJacobian_id (ψ : FreeGroup X →* H) :
zcFreeGroupHomFoxJacobian C ψ (MonoidHom.id (FreeGroup X)) =
foxJacobianId (R := ZCCompletedGroupAlgebra C H) (X := X)The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian of the identity homomorphism is the identity family.
Show proof
by
simp only [zcFreeGroupHomFoxJacobian,
freeCrossedDifferentialWithCoeffJacobian_id (X := X) (S := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraScalar C ψ)]Proof. 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 zcFreeGroupHomFoxJacobianMatrix_id (ψ : FreeGroup X →* H) :
zcFreeGroupHomFoxJacobianMatrix C ψ (MonoidHom.id (FreeGroup X)) =
(1 : Matrix X X (ZCCompletedGroupAlgebra C H))The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian matrix of the identity homomorphism is the identity matrix.
Show proof
by
simp only [zcFreeGroupHomFoxJacobianMatrix,
freeCrossedDifferentialWithCoeffJacobianMatrix_id (X := X) (S := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraScalar C ψ)]Proof. 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 zcFreeGroupHomFoxJacobianLinearMap_id
[Fintype X] (ψ : FreeGroup X →* H) :
zcFreeGroupHomFoxJacobianLinearMap C ψ (MonoidHom.id (FreeGroup X)) =
(LinearMap.id :
ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
ZCFreeFoxCoordinates C (X := X) (H := H))The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian linear map of the identity homomorphism is the identity.
Show proof
by
simp only [zcFreeGroupHomFoxJacobianLinearMap,
freeCrossedDifferentialWithCoeffJacobianLinearMap_id (X := X) (S := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraScalar C ψ)]Proof. 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 zcFreeGroupFoxDerivativeVector_comp_linearMap
[Fintype X]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C ψ (φ w) =
zcFreeGroupHomFoxJacobianLinearMap C ψ φ
(zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w)Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule in vector form.
Show proof
by
simpa [zcFreeGroupFoxDerivativeVector, zcFreeGroupHomFoxJacobianLinearMap,
zcFreeGroupHomFoxJacobian] using
freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap
(X := X) (Y := Y) (zcCompletedGroupAlgebraScalar 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 zcFreeGroupFoxDerivativeVector_comp_apply
[Fintype X]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(w : FreeGroup X) (y : Y) :
zcFreeGroupFoxDerivativeVector C ψ (φ w) y =
∑ x : X,
zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w x *
zcFreeGroupHomFoxJacobian C ψ φ x yCompleted \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule in component form.
Show proof
by
exact congrFun (zcFreeGroupFoxDerivativeVector_comp_linearMap C ψ φ w) yProof. 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_comp
[Fintype X]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(w : FreeGroup X) (y : Y) :
zcFreeGroupFoxDerivative C ψ y (φ w) =
∑ x : X,
zcFreeGroupFoxDerivative C (ψ.comp φ) x w *
zcFreeGroupHomFoxJacobian C ψ φ x yCompleted \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule, component form for named derivative coordinates.
Show proof
by
exact zcFreeGroupFoxDerivativeVector_comp_apply C ψ φ w yProof. 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 zcFreeGroupFoxDerivativeVector_comp_matrix
[Fintype X]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C ψ (φ w) =
Matrix.vecMul
(zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w)
(zcFreeGroupHomFoxJacobianMatrix C ψ φ)The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule in matrix form.
Show proof
by
rw [zcFreeGroupFoxDerivativeVector_comp_linearMap]
exact zcFreeGroupHomFoxJacobianLinearMap_eq_vecMul C ψ φ
(zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w)Proof. 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 zcFreeGroupHomFoxJacobian_comp_apply
[Fintype Y]
(ψ : FreeGroup Z →* H)
(φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
(x : X) (z : Z) :
zcFreeGroupHomFoxJacobian C ψ (φ.comp χ) x z =
∑ y : Y,
zcFreeGroupHomFoxJacobian C (ψ.comp φ) χ x y *
zcFreeGroupHomFoxJacobian C ψ φ y zThe completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian chain rule is expressed componentwise.
Show proof
by
simpa [zcFreeGroupHomFoxJacobian] using
freeCrossedDifferentialWithCoeffJacobian_comp_apply
(X := X) (Y := Y) (Z := Z) (zcCompletedGroupAlgebraScalar C ψ) φ χ x zProof. 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 zcFreeGroupHomFoxJacobianLinearMap_comp
[Fintype X] [Fintype Y]
(ψ : FreeGroup Z →* H)
(φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
(zcFreeGroupHomFoxJacobianLinearMap C ψ φ).comp
(zcFreeGroupHomFoxJacobianLinearMap C (ψ.comp φ) χ) =
zcFreeGroupHomFoxJacobianLinearMap C ψ (φ.comp χ)The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian chain rule is expressed in linear-map form.
Show proof
by
simpa [zcFreeGroupHomFoxJacobianLinearMap] using
freeCrossedDifferentialWithCoeffJacobianLinearMap_comp
(X := X) (Y := Y) (Z := Z) (zcCompletedGroupAlgebraScalar C ψ) φ χProof. 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 zcFreeGroupHomFoxJacobianMatrix_comp
[Fintype Y]
(ψ : FreeGroup Z →* H)
(φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
zcFreeGroupHomFoxJacobianMatrix C ψ (φ.comp χ) =
zcFreeGroupHomFoxJacobianMatrix C (ψ.comp φ) χ *
zcFreeGroupHomFoxJacobianMatrix C ψ φThe completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian chain rule is expressed in matrix form.
Show proof
by
apply Matrix.ext
intro x z
exact zcFreeGroupHomFoxJacobian_comp_apply C ψ φ χ x zProof. 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 zcFreeGroupFoxDerivativeVector_unique
(ψ : 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)) :
delta = zcFreeGroupFoxDerivativeVector C ψUniqueness of the completed free-group derivative vector among crossed differentials with standard coordinate values on free generators.
Show proof
by
exact freeCrossedDifferentialWithCoeff_unique
(A := ZCFreeFoxCoordinates C (X := X) (H := H))
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))
delta hdelta hbasisProof. 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 existsUnique_zcFreeGroupFoxDerivativeVector
(ψ : FreeGroup X →* H) :
∃! delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H),
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta ∧
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H)Existence and uniqueness theorem for the completed free-group derivative vector.
Show proof
by
exact existsUnique_freeCrossedDifferentialWithCoeff
(A := ZCFreeFoxCoordinates C (X := X) (H := H))
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))Proof. 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.
□def zcFreeCrossedDifferentialEquivLinearMap
(ψ : FreeGroup X →* H) :
{delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H) //
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta} ≃
(ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
ZCFreeFoxCoordinates C (X := X) (H := H)) :=
zcCompletedCrossedDifferentialEquivLinearMap
(A := ZCFreeFoxCoordinates C (X := X) (H := H)) C ψCompleted crossed differentials on a free group are represented by the corresponding completed universal module.
def zcFreeGroupFoxDerivativeVectorLinearMap
(ψ : FreeGroup X →* H) :
ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
ZCFreeFoxCoordinates C (X := X) (H := H) :=
zcCompletedDifferentialModuleLift
(A := ZCFreeFoxCoordinates C (X := X) (H := H)) C ψ
(zcFreeGroupFoxDerivativeVector C ψ)
(zcFreeGroupFoxDerivativeVector_isCrossedDifferential C ψ)The linear map from the completed universal module representing the completed derivative vector.
theorem zcFreeGroupFoxDerivativeVectorLinearMap_universal
(ψ : FreeGroup X →* H) (w : FreeGroup X) :
zcFreeGroupFoxDerivativeVectorLinearMap C ψ
(zcUniversalDifferential C ψ w) =
zcFreeGroupFoxDerivativeVector C ψ wThe representing linear map evaluates on the universal differential as the completed derivative vector.
Show proof
by
exact zcCompletedDifferentialModuleLift_universal
(A := ZCFreeFoxCoordinates C (X := X) (H := H)) C ψ
(zcFreeGroupFoxDerivativeVector C ψ)
(zcFreeGroupFoxDerivativeVector_isCrossedDifferential 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 zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
(ψ : FreeGroup X →* H) {w : FreeGroup X}
(hw : zcUniversalDifferential C ψ w = 0) :
zcFreeGroupFoxDerivativeVector C ψ w = 0If the universal completed differential of a word vanishes, then its completed free Fox derivative vector vanishes.
Show proof
by
have h :=
congrArg (zcFreeGroupFoxDerivativeVectorLinearMap C ψ) hw
simpa using hProof. 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_eq_zero_of_zcUniversalDifferential_eq_zero
(ψ : FreeGroup X →* H) (i : X) {w : FreeGroup X}
(hw : zcUniversalDifferential C ψ w = 0) :
zcFreeGroupFoxDerivative C ψ i w = 0The vanishing criterion for the completed Fox derivative vector holds componentwise.
Show proof
by
have hvec :=
zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
(C := C) ψ hw
simpa [zcFreeGroupFoxDerivative] using congrFun hvec iProof. 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 existsUnique_zcFreeGroupFoxDerivativeVectorLinearMap
(ψ : FreeGroup X →* H) :
∃! f :
ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
ZCFreeFoxCoordinates C (X := X) (H := H),
∀ w : FreeGroup X,
f (zcUniversalDifferential C ψ w) =
zcFreeGroupFoxDerivativeVector C ψ wExistence and uniqueness of the linear map representing the completed derivative vector.
Show proof
by
exact existsUnique_zcCompletedDifferentialModuleLift
(A := ZCFreeFoxCoordinates C (X := X) (H := H)) C ψ
(zcFreeGroupFoxDerivativeVector C ψ)
(zcFreeGroupFoxDerivativeVector_isCrossedDifferential C ψ)Proof. 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.
□