ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients

5 sections | 12 files | 246 declarations

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

Completed.ProCIntegerCoefficients.Augmentation - Completed.ProCIntegerCoefficients.AugmentationIdeal - Completed.ProCIntegerCoefficients.Core - Completed.ProCIntegerCoefficients.FreeGroup - Completed.ProCIntegerCoefficients.Naturality

imports

Imported by

ProCGroups.FoxDifferential.Completed

Augmentation

1 file | 17 declarations | 12 Theorems | 3 Definitions | 2 Abbreviations

The principal declarations in this module are: - `zcCompletedGroupAlgebraTopIndex` The canonical trivial group quotient used to read the completed augmentation. - `zcCompletedGr...

AugmentationIdeal

5 files | 63 declarations | 44 Theorems | 18 Definitions | 1 Abbreviation

This aggregate re-exports the following parts of the Fox differential API: - `Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic` - `Completed.ProCIntegerCoefficients.Aug...

Core

The principal declarations in this module are: - `ZCCoeff` The pro-\(C\) integer coefficient ring. - `ZCCompletedGroupAlgebraIndex` The two-parameter finite-stage index for \(\m...

FreeGroup

4 files | 48 declarations | 37 Theorems | 10 Definitions | 1 Abbreviation

This aggregate re-exports the following parts of the Fox differential API: - `Completed.ProCIntegerCoefficients.FreeGroup.Fundamental`

Naturality

1 file | 43 declarations | 34 Theorems | 9 Definitions

The principal declarations in this module are: - `zcCompletedGroupAlgebraMapStage` The finite-stage component of the target map on \(\mathbb{Z}_C\llbracket H\rrbracket\). - `zcC...