The relative Fox fundamental formula

A group-ring boundary decomposes into Fox derivatives times the boundaries of the generators.

In a presentation, a relator maps to the identity and has zero boundary, so its Fox vector lies in the kernel of a linear map over the group ring. This makes noncommutative relations accessible to module calculations. Fox introduced the calculus in his 1953 paper, following his study of Alexander’s knot polynomial; Crowell later developed its connection with derived modules.

Mathematical statement

Let $X$ be finite, $F(X)$ the free group on $X$, $H$ any group, and $\psi:F(X)\to H$ a homomorphism. For every $w\in F(X)$, $$[\psi(w)]-1=\sum_{x\in X}\frac{\partial_\psi w}{\partial x}\bigl([\psi(x)]-1\bigr)\quad\text{in }\mathbb Z[H].$$ Here $[h]$ denotes the group-ring basis element indexed by $h$, and the derivative is the relative Fox derivative.

The factors occur in the displayed order. The group ring need not be commutative, so exchanging a derivative with the factor to its right changes the assertion.

Lean code

`FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula`

Published library source ↗Same source in NYLL ↗

theorem relativeFreeGroupFoxDerivative_fundamental_formula (w : FreeGroup X) :
    groupRingBoundary ψ w =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X ψ w x *
          augmentationGenerator H (ψ (FreeGroup.of x))

In-scope Lean context

namespace FoxDifferential

noncomputable section

namespace FoxCalculus

open scoped BigOperators

universe u v

variable {H : Type v} [Group H]

variable (X : Type u)

variable [DecidableEq X]

variable (ψ : FreeGroup X →* H)

variable [Fintype X]

Full declaration and proof

/--
Relative Fox fundamental formula, also known as the Fox--Euler formula: \(\psi(w) - 1 = \sum_x
(\partial w/\partial x) (\psi(x) - 1)\).
-/
theorem relativeFreeGroupFoxDerivative_fundamental_formula (w : FreeGroup X) :
    groupRingBoundary ψ w =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X ψ w x *
          augmentationGenerator H (ψ (FreeGroup.of x)) := by
  have h :=
    LinearMap.congr_fun
      (toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap (H := H) X ψ)
      (relativeFreeGroupFoxDerivative (H := H) X ψ w)
  rw [LinearMap.comp_apply, relativeFreeFoxCoordinatesLinearMap_derivative,
    toGroupRing_d] at h
  simpa [relativeFreeGroupFoxBoundary] using h

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

Mathematical statement

Lean code

FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula

References

`FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula`