def residueFreeCrossedDifferentialEquivLinearMap
(n : ℕ) (ψ : FreeGroup X →* H) :
{delta : FreeGroup X → ResidueFreeFoxCoordinates n H X //
IsCrossedDifferential (residueGroupRingScalar n ψ) delta} ≃
(ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
ResidueFreeFoxCoordinates n H X) :=
residueCrossedDifferentialEquivLinearMap
(A := ResidueFreeFoxCoordinates n H X) n ψResidue crossed differentials on a free group are represented by the corresponding universal residue module.
def residueFreeGroupFoxDerivativeVectorLinearMap
(n : ℕ) (ψ : FreeGroup X →* H) :
ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
ResidueFreeFoxCoordinates n H X :=
residueDifferentialModuleLift
(A := ResidueFreeFoxCoordinates n H X) n ψ
(residueFreeGroupFoxDerivativeVector n ψ)
(residueFreeGroupFoxDerivativeVector_isCrossedDifferential n ψ)The linear map from the residue universal module representing the residue derivative vector.
theorem residueFreeGroupFoxDerivativeVectorLinearMap_universal
(n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
residueFreeGroupFoxDerivativeVectorLinearMap n ψ
(residueUniversalDifferential n ψ w) =
residueFreeGroupFoxDerivativeVector n ψ wThe representing linear map evaluates on the universal differential as the residue derivative vector.
Show proof
by
exact residueDifferentialModuleLift_universal
(A := ResidueFreeFoxCoordinates n H X) n ψ
(residueFreeGroupFoxDerivativeVector n ψ)
(residueFreeGroupFoxDerivativeVector_isCrossedDifferential 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 existsUnique_residueFreeGroupFoxDerivativeVectorLinearMap
(n : ℕ) (ψ : FreeGroup X →* H) :
∃! f :
ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
ResidueFreeFoxCoordinates n H X,
∀ w : FreeGroup X,
f (residueUniversalDifferential n ψ w) =
residueFreeGroupFoxDerivativeVector n ψ wExistence and uniqueness of the linear map representing the residue derivative vector.
Show proof
by
exact existsUnique_residueDifferentialModuleLift
(A := ResidueFreeFoxCoordinates n H X) n ψ
(residueFreeGroupFoxDerivativeVector n ψ)
(residueFreeGroupFoxDerivativeVector_isCrossedDifferential n ψ)Proof. 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.
□