FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Coordinates
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
import
def zcFreeGroupFoxBoundary (ψ : FreeGroup X →* H) :
ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedGroupAlgebra C H where
toFun v := ∑ i : X, v i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)
map_add' := by
intro v w
simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
map_smul' := by
intro r v
simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, RingHom.id_apply, Finset.mul_sum]The completed Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\).
theorem zcFreeGroupFoxBoundary_apply
(ψ : FreeGroup X →* H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
zcFreeGroupFoxBoundary C ψ v =
∑ i : X, v i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)The boundary map is evaluated on the canonical generators and then extended linearly to the completed coordinate module.
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 zcFreeGroupFoxBoundary_eq_foxBoundaryMap
(ψ : FreeGroup X →* H) :
zcFreeGroupFoxBoundary C ψ =
foxBoundaryMap
(fun i : X =>
coefficientFoxBoundary (zcCompletedGroupAlgebraScalar C ψ) (FreeGroup.of i))The completed Fox boundary is the generic finite Fox boundary map specialized to \(x \mapsto [\psi(x)] - 1\).
Show proof
by
ext v
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 zcFreeGroupFoxBoundary_single (ψ : FreeGroup X →* H) (i : X) :
zcFreeGroupFoxBoundary C ψ
(Pi.single i (1 : ZCCompletedGroupAlgebra C H)) =
zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of i)The completed Fox boundary sends a coordinate basis vector to the corresponding completed augmentation generator.
Show proof
by
rw [zcFreeGroupFoxBoundary_apply]
rw [Finset.sum_eq_single i]
· simp only [Pi.single_eq_same, one_mul, zcCompletedGroupAlgebraBoundary]
· intro j _ hji
simp only [Pi.single_eq_of_ne hji, zero_mul]
· simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_mul, IsEmpty.forall_iff]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 zcDifferentialToFreeFoxCoordinates (ψ : FreeGroup X →* H) :
ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
ZCFreeFoxCoordinates C (X := X) (H := H) :=
zcFreeGroupFoxDerivativeVectorLinearMap C ψThe linear map from the completed universal module to completed Fox-coordinate vectors.
theorem zcDifferentialToFreeFoxCoordinates_universal
(ψ : FreeGroup X →* H) (w : FreeGroup X) :
zcDifferentialToFreeFoxCoordinates C ψ
(zcUniversalDifferential C ψ w) =
zcFreeGroupFoxDerivativeVector C ψ wThe completed coordinate map sends a universal differential to the completed Fox derivative vector.
Show proof
by
exact zcFreeGroupFoxDerivativeVectorLinearMap_universal 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.
□def zcFreeFoxCoordinatesLinearMap (ψ : FreeGroup X →* H) :
ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedDifferentialModule C ψ where
toFun v := ∑ x : X, v x • zcUniversalDifferential C ψ (FreeGroup.of x)
map_add' := by
intro v w
simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
map_smul' := by
intro r v
simp only [Pi.smul_apply, RingHom.id_apply, smul_eq_mul, Finset.smul_sum, smul_smul]The linear map from completed Fox-coordinate vectors to the completed universal module, sending the coordinate basis at \(x\) to \(d_{\psi}(x)\).
theorem zcFreeFoxCoordinatesLinearMap_single (ψ : FreeGroup X →* H) (x : X) :
zcFreeFoxCoordinatesLinearMap C ψ
(Pi.single x (1 : ZCCompletedGroupAlgebra C H)) =
zcUniversalDifferential C ψ (FreeGroup.of x)The coordinate-to-differential map sends a coordinate basis vector to the corresponding universal completed differential.
Show proof
by
change (∑ y : X,
((Pi.single x (1 : ZCCompletedGroupAlgebra C H) :
ZCFreeFoxCoordinates C (X := X) (H := H)) y) •
zcUniversalDifferential C ψ (FreeGroup.of y)) =
zcUniversalDifferential C ψ (FreeGroup.of x)
rw [Finset.sum_eq_single x]
· simp only [Pi.single_eq_same, one_smul]
· intro y _ hy
simp only [Pi.single_eq_of_ne hy, zero_smul]
· simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]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 zcFreeFoxCoordinatesLinearMap_derivativeVector
(ψ : FreeGroup X →* H) (w : FreeGroup X) :
zcFreeFoxCoordinatesLinearMap C ψ
(zcFreeGroupFoxDerivativeVector C ψ w) =
zcUniversalDifferential C ψ wThe coordinate-to-differential map recovers the universal completed differential from the completed derivative vector.
Show proof
by
let beta : FreeGroup X → ZCCompletedDifferentialModule C ψ :=
fun w => zcFreeFoxCoordinatesLinearMap C ψ (zcFreeGroupFoxDerivativeVector C ψ w)
have hbeta :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) beta :=
IsCrossedDifferential.map_linear
(zcFreeGroupFoxDerivativeVector_isCrossedDifferential C ψ)
(zcFreeFoxCoordinatesLinearMap C ψ)
have hbasis :
∀ x : X, beta (FreeGroup.of x) =
zcUniversalDifferential C ψ (FreeGroup.of x) := by
intro x
simp only [zcFreeGroupFoxDerivativeVector_of, zcFreeFoxCoordinatesLinearMap_single, beta]
have hbeta_eq :
beta =
freeCrossedDifferentialWithCoeff
(A := ZCCompletedDifferentialModule C ψ)
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => zcUniversalDifferential C ψ (FreeGroup.of x)) := by
exact freeCrossedDifferentialWithCoeff_unique
(A := ZCCompletedDifferentialModule C ψ)
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => zcUniversalDifferential C ψ (FreeGroup.of x))
beta hbeta hbasis
have huniv_eq :
zcUniversalDifferential C ψ =
freeCrossedDifferentialWithCoeff
(A := ZCCompletedDifferentialModule C ψ)
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => zcUniversalDifferential C ψ (FreeGroup.of x)) := by
exact freeCrossedDifferentialWithCoeff_unique
(A := ZCCompletedDifferentialModule C ψ)
(zcCompletedGroupAlgebraScalar C ψ)
(fun x => zcUniversalDifferential C ψ (FreeGroup.of x))
(zcUniversalDifferential C ψ)
(zcUniversalDifferential_isCrossedDifferential C ψ)
(by intro x; rfl)
exact congrFun (hbeta_eq.trans huniv_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 zcDifferentialToFreeFoxCoordinates_comp_zcFreeFoxCoordinatesLinearMap
(ψ : FreeGroup X →* H) :
(zcDifferentialToFreeFoxCoordinates C ψ).comp
(zcFreeFoxCoordinatesLinearMap C ψ) =
LinearMap.idThe coordinate map is a left inverse to the coordinate-to-differential map.
Show proof
by
apply LinearMap.ext
intro v
rw [LinearMap.comp_apply]
change zcDifferentialToFreeFoxCoordinates C ψ
(∑ y : X, v y • zcUniversalDifferential C ψ (FreeGroup.of y)) = v
rw [map_sum]
simp only [map_smul, zcDifferentialToFreeFoxCoordinates_universal]
funext x
change ((∑ y : X,
v y • zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of y)) :
ZCFreeFoxCoordinates C (X := X) (H := H)) x = v x
rw [Finset.sum_apply]
rw [Finset.sum_eq_single x]
· simp only [zcFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one]
· intro y _ hy
have hxy : x ≠ y := fun h => hy h.symm
simp only [zcFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_of_ne hxy, smul_eq_mul, mul_zero]
· simp only [Finset.mem_univ, not_true_eq_false, zcFreeGroupFoxDerivativeVector_of, Pi.smul_apply,
Pi.single_eq_same, smul_eq_mul, mul_one, IsEmpty.forall_iff]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 zcFreeFoxCoordinatesLinearMap_comp_zcDifferentialToFreeFoxCoordinates
(ψ : FreeGroup X →* H) :
(zcFreeFoxCoordinatesLinearMap C ψ).comp
(zcDifferentialToFreeFoxCoordinates C ψ) =
LinearMap.idThe coordinate-to-differential map is a left inverse to the completed coordinate map.
Show proof
by
apply zcCompletedDifferentialModuleHom_ext C ψ
intro w
simp only [LinearMap.comp_apply, zcDifferentialToFreeFoxCoordinates_universal,
zcFreeFoxCoordinatesLinearMap_derivativeVector, LinearMap.id_coe, id_eq]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 zcFreeFoxCoordinatesLinearEquivDifferential
(ψ : FreeGroup X →* H) :
ZCFreeFoxCoordinates C (X := X) (H := H) ≃ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedDifferentialModule C ψ := by
refine LinearEquiv.ofLinear
(zcFreeFoxCoordinatesLinearMap C ψ)
(zcDifferentialToFreeFoxCoordinates C ψ)
?_ ?_
· exact zcFreeFoxCoordinatesLinearMap_comp_zcDifferentialToFreeFoxCoordinates C ψ
· exact zcDifferentialToFreeFoxCoordinates_comp_zcFreeFoxCoordinatesLinearMap C ψThe linear equivalence between completed Fox coordinates and the completed universal differential module of a finite-rank free group.