ProCGroups.FoxDifferential.Discrete.FoxCalculus

5 sections | 5 files | 34 declarations

This aggregate re-exports the following parts of the Fox differential API:

Discrete.FoxCalculus.Boundary - Discrete.FoxCalculus.Coordinates - Discrete.FoxCalculus.Derivative - Discrete.FoxCalculus.Semidirect - Discrete.FoxCalculus.Universal

imports

Imported by

ProCGroups.FoxDifferential.Discrete

Boundary

1 file | 10 declarations | 9 Theorems | 1 Definition

The principal declarations in this module are: - `relativeFreeGroupFoxBoundary` The pushed-forward Fox boundary \(a \mapsto \sum_x a_x (\psi(x) - 1)\). - `relativeFreeGroupFoxBo...

Coordinates

1 file | 3 declarations | 2 Theorems | 1 Definition

The principal declarations in this module are: - `relativeFreeFoxCoordinatesLinearEquivDifferential` The linear equivalence between pushed-forward Fox coordinates and the univer...

Derivative

1 file | 13 declarations | 10 Theorems | 3 Definitions

The principal declarations in this module are: - `relativeFreeGroupFoxLift` The semidirect-product lift whose left component is the Fox derivative pushed forward by \(\psi\), an...

Semidirect

1 file | 2 declarations | 2 Abbreviations

The principal declarations in this module are: - `RelativeFreeFoxCoordinates` Fox-coordinate vectors for a homomorphism from a free group to a target group \(H\). The coefficien...

Universal

1 file | 6 declarations | 4 Theorems | 2 Definitions

The principal declarations in this module are: - `relativeDifferentialToFreeFoxCoordinates` The universal map \(A_{\psi}\) \(\to\) \(\mathbb{Z}[H]^X\) induced by the relative Fo...