FoxDifferential.Completed.FiniteStage.Stage.Derivative

5 sections | 8 files | 66 declarations

Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

Boundary

1 files | 7 declarations | 6 Theorem | 1 Definition

The finite-stage Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([x_i] - 1)\) on coordinate vectors.

Lift

1 files | 6 declarations | 2 Theorem | 4 Definition

Semidirect-product lift defining the finite-stage Fox derivative.

Quotient

4 files | 27 declarations | 21 Theorem | 6 Definition

Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

Relators

1 files | 11 declarations | 11 Theorem

If a word lies in N, the finite-stage lift has trivial right component.

Rules

1 files | 15 declarations | 13 Theorem | 2 Definition

The finite-stage derivative vector sends the identity word to zero.