ProCGroups.FoxDifferential.Completed.Residue.FreeGroup

5 sections | 5 files | 27 declarations

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

Completed.Residue.FreeGroup.Basic - Completed.Residue.FreeGroup.Boundary - Completed.Residue.FreeGroup.Coordinates - Completed.Residue.FreeGroup.Fundamental - Completed.Residue.FreeGroup.Universal

imports

Imported by

ProCGroups.FoxDifferential.Completed.Residue

Basic

1 file | 6 declarations | 3 Theorems | 2 Definitions | 1 Abbreviation

The principal declarations in this module are: - `ResidueFreeFoxCoordinates` Residue Fox-coordinate vectors with coefficients in \((\mathbb{Z}/n\mathbb{Z})[H]\). - `residueFreeG...

Boundary

1 file | 3 declarations | 2 Theorems | 1 Definition

The principal declarations in this module are: - `residueFreeGroupFoxBoundary` The residue Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\). - `residueFreeGroup...

Coordinates

1 file | 8 declarations | 5 Theorems | 3 Definitions

The principal declarations in this module are: - `residueDifferentialToFreeFoxCoordinates` The linear map from the residue universal module to residue Fox-coordinate vectors. - ...

Fundamental

1 file | 6 declarations | 6 Theorems

The principal declarations in this module are: - `residueFreeGroupFoxBoundary_derivativeVector` Boundary-map form of the residue Fox fundamental formula. - `residueFreeGroupFoxB...

Universal

1 file | 4 declarations | 2 Theorems | 2 Definitions

The principal declarations in this module are: - `residueFreeCrossedHomEquivLinearMap` Residue crossed homomorphisms on a free group are represented by the universal residue mod...