Yamaguchi Lean 4 Library
FoxDifferential.Completed.FiniteStage.Stage
FoxDifferential/Completed/FiniteStage/Stage

FoxDifferential.Completed.FiniteStage.Stage

6 sections | 16 files | 126 declarations

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

Derivative

9 files | 66 declarations | 53 Theorem | 13 Definition
Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

Fundamental

3 files | 9 declarations | 8 Theorem | 1 Definition
Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

KernelIdeal

1 files | 2 declarations | 2 Theorem
The finite-stage source generator \([x_i]-1\) belongs to the source augmentation ideal.

Naturality

1 files | 18 declarations | 13 Theorem | 5 Definition
Commutator-power relators are monotone in the normal subgroup.

Semidirect

1 files | 21 declarations | 9 Theorem | 3 Definition | 4 Abbreviation | 1 Structure | 4 Instance
The finite-stage target quotient \(F/N\).

Source

1 files | 10 declarations | 7 Theorem | 3 Definition
A chosen free-group representative of a finite Fox source quotient element. It supplies source-valued coefficients for the finite algebra argument; no canonicality is needed.