FoxDifferential.Completed.Residue.FreeGroup.Basic
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
abbrev ResidueFreeFoxCoordinates (n : ℕ) (H : Type v) (X : Type u) : Type (max u v) :=
X → ResidueGroupRing n HResidue Fox-coordinate vectors with coefficients in \((\mathbb{Z}/n\mathbb{Z})[H]\).
def residueFreeGroupFoxDerivativeVector (n : ℕ) (ψ : FreeGroup X →* H)
(w : FreeGroup X) :
ResidueFreeFoxCoordinates n H X :=
freeCrossedDifferentialWithCoeff
(A := ResidueFreeFoxCoordinates n H X)
(residueGroupRingScalar n ψ)
(fun x => Pi.single x (1 : ResidueGroupRing n H))
wResidue free-group Fox derivative vector, with coefficients pushed forward along \(\psi:\mathrm{FreeGroup}(X)\to H\).
def residueFreeGroupFoxDerivative (n : ℕ) (ψ : FreeGroup X →* H) (i : X)
(w : FreeGroup X) : ResidueGroupRing n H :=
residueFreeGroupFoxDerivativeVector n ψ w iA coordinate of the residue free-group Fox derivative.
theorem residueFreeGroupFoxDerivativeVector_one (n : ℕ) (ψ : FreeGroup X →* H) :
residueFreeGroupFoxDerivativeVector n ψ (1 : FreeGroup X) = 0The residue free-group derivative vector sends the identity word to zero.
Show proof
by
simp only [residueFreeGroupFoxDerivativeVector, freeCrossedDifferentialWithCoeff_one]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.
□theorem residueFreeGroupFoxDerivative_one (n : ℕ) (ψ : FreeGroup X →* H) (i : X) :
residueFreeGroupFoxDerivative n ψ i (1 : FreeGroup X) = 0The residue free-group derivative sends the identity word to zero componentwise.
Show proof
by
simp only [residueFreeGroupFoxDerivative, residueFreeGroupFoxDerivativeVector_one, Pi.zero_apply]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.
□theorem residueFreeGroupFoxDerivativeVector_of (n : ℕ) (ψ : FreeGroup X →* H) (x : X) :
residueFreeGroupFoxDerivativeVector n ψ (FreeGroup.of x) =
Pi.single x (1 : ResidueGroupRing n H)The residue free-group derivative vector sends a free generator to the corresponding coordinate basis vector.
Show proof
by
simp only [residueFreeGroupFoxDerivativeVector, freeCrossedDifferentialWithCoeff_of]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.
□theorem residueFreeGroupFoxDerivative_of (n : ℕ) (ψ : FreeGroup X →* H) (i x : X) :
residueFreeGroupFoxDerivative n ψ i (FreeGroup.of x) =
(Pi.single x (1 : ResidueGroupRing n H) :
ResidueFreeFoxCoordinates n H X) iAt a generator, the residue free-group Fox derivative has the corresponding Kronecker component value.
Show proof
by
rw [residueFreeGroupFoxDerivative, residueFreeGroupFoxDerivativeVector_of]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.
□theorem residueFreeGroupFoxDerivativeVector_isCrossedDifferential
(n : ℕ) (ψ : FreeGroup X →* H) :
IsCrossedDifferential
(residueGroupRingScalar n ψ) (residueFreeGroupFoxDerivativeVector n ψ)The residue free-group derivative vector is a crossed differential.
Show proof
by
exact freeCrossedDifferentialWithCoeff_isCrossedDifferential
(A := ResidueFreeFoxCoordinates n H X)
(residueGroupRingScalar n ψ)
(fun x => Pi.single x (1 : ResidueGroupRing n H))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.
□theorem residueFreeGroupFoxDerivativeVector_unique
(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)) :
delta = residueFreeGroupFoxDerivativeVector n ψUniqueness of the residue free-group derivative vector among crossed differentials with standard coordinate values on free generators.
Show proof
by
exact freeCrossedDifferentialWithCoeff_unique
(A := ResidueFreeFoxCoordinates n H X)
(residueGroupRingScalar n ψ)
(fun x => Pi.single x (1 : ResidueGroupRing n H))
delta hdelta hbasisProof. 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_residueFreeGroupFoxDerivativeVector
(n : ℕ) (ψ : FreeGroup X →* H) :
∃! delta : FreeGroup X → ResidueFreeFoxCoordinates n H X,
IsCrossedDifferential (residueGroupRingScalar n ψ) delta ∧
∀ x : X, delta (FreeGroup.of x) =
Pi.single x (1 : ResidueGroupRing n H)Existence and uniqueness theorem for the residue free-group derivative vector.
Show proof
by
exact existsUnique_freeCrossedDifferentialWithCoeff
(A := ResidueFreeFoxCoordinates n H X)
(residueGroupRingScalar n ψ)
(fun x => Pi.single x (1 : ResidueGroupRing n H))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.
□