FoxDifferential.Completed.ProCIntegerCoefficients

5 sections | 12 files | 268 declarations

This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Augmentation

1 files | 17 declarations | 12 Theorem | 3 Definition | 2 Abbreviation

The canonical trivial group quotient used to read the completed augmentation.

AugmentationIdeal

5 files | 65 declarations | 46 Theorem | 18 Definition | 1 Abbreviation

Wrapper for the `FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal` folder.

Core

The pro-\(C\) integer coefficient ring.

FreeGroup

4 files | 52 declarations | 40 Theorem | 11 Definition | 1 Abbreviation

This module gives the free-group formulas for pro-\(C\) integer coefficients, used to compare completed Fox derivatives with ordinary finite-stage derivatives.

Naturality

1 files | 42 declarations | 34 Theorem | 8 Definition

The finite-stage component of the target map on \(\mathbb{Z}_C\llbracket H\rrbracket\).