FoxDifferential.Completed.Residue.FreeGroup.Boundary
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
def residueFreeGroupFoxBoundary (n : ℕ) (ψ : FreeGroup X →* H) :
ResidueFreeFoxCoordinates n H X →ₗ[ResidueGroupRing n H] ResidueGroupRing n H where
toFun v :=
∑ i : X,
v i *
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)
map_add' := by
intro v w
simp only [Pi.add_apply, MonoidAlgebra.of_apply, add_mul, Finset.sum_add_distrib]
map_smul' := by
intro r v
simp only [Pi.smul_apply, smul_eq_mul, MonoidAlgebra.of_apply, mul_assoc, RingHom.id_apply, Finset.mul_sum]The residue Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\).
theorem residueFreeGroupFoxBoundary_apply
(n : ℕ) (ψ : FreeGroup X →* H) (v : ResidueFreeFoxCoordinates n H X) :
residueFreeGroupFoxBoundary n ψ v =
∑ i : X,
v i *
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)The residue free-group Fox boundary is evaluated on the canonical generators and then extended linearly to the residue coordinate module.
Show proof
rflProof. 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 residueFreeGroupFoxBoundary_single (n : ℕ) (ψ : FreeGroup X →* H) (i : X) :
residueFreeGroupFoxBoundary n ψ
(Pi.single i (1 : ResidueGroupRing n H)) =
residueGroupRingBoundary n ψ (FreeGroup.of i)The residue Fox boundary sends a coordinate basis vector to the corresponding augmentation generator.
Show proof
by
rw [residueFreeGroupFoxBoundary_apply]
rw [Finset.sum_eq_single i]
· simp only [Pi.single_eq_same, MonoidAlgebra.of_apply, one_mul, residueGroupRingBoundary]
· intro j _ hji
simp only [Pi.single_eq_of_ne hji, MonoidAlgebra.of_apply, zero_mul]
· simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, MonoidAlgebra.of_apply, one_mul,
IsEmpty.forall_iff]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.
□