FoxDifferential.Completed.FiniteStage.PrimePower.Derivative

6 sections | 14 files | 54 declarations

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

CompletedSource

1 files | 4 declarations | 3 Theorem | 1 Definition
The completed source Fox derivative with values in the prime-power finite-stage target limit.

CompletedTarget

1 files | 6 declarations | 5 Theorem | 1 Definition
The completed source Fox derivative, mapped from the finite-stage target limit into the completed group algebra of the target quotient.

Limit

1 files | 8 declarations | 6 Theorem | 2 Definition
Naturality of the finite-stage group-algebra Fox derivative along a prime-power transition.

OnGroup

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

Source

5 files | 19 declarations | 19 Theorem
Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

Vector

1 files | 2 declarations | 1 Theorem | 1 Definition
The vector of all completed-target Fox derivatives, indexed by free generators.