ProCGroups.FoxDifferential.Discrete

8 sections | 25 files | 317 declarations

This module formalizes the discrete Fox calculus.

imports

Imported by

ProCGroups.FoxDifferential

Absolute

1 file | 11 declarations | 10 Theorems | 1 Definition

The principal declarations in this module are: - `freeGroupFoxDerivative` The absolute Fox derivative of a free-group word, with coefficients in \(\mathbb{Z}[\mathrm{FreeGroup}(...

DifferentialModule

4 files | 50 declarations | 31 Theorems | 15 Definitions | 4 Abbreviations

This aggregate re-exports the following parts of the Fox differential API: - `Discrete.DifferentialModule.Boundary`

FoxCalculus

6 files | 34 declarations | 25 Theorems | 7 Definitions | 2 Abbreviations

This aggregate re-exports the following parts of the Fox differential API: - `Discrete.FoxCalculus.Boundary` - `Discrete.FoxCalculus.Coordinates` - `Discrete.FoxCalculus.Derivat...

FreeExpansion

1 file | 7 declarations | 5 Theorems | 2 Definitions

The principal declarations in this module are: - `freeCrossedDifferentialExpansion` Prescribed values on the free generators determine the Fox-coordinate expansion. - `freeCross...

GroupRing

1 file | 28 declarations | 19 Theorems | 9 Definitions

The principal declarations in this module are: - `augmentationAlgHom` The augmentation algebra homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\). - `augmentation` The augmentation r...

Jacobian

4 files | 31 declarations | 25 Theorems | 6 Definitions

This aggregate re-exports the following parts of the Fox differential API: - `Discrete.Jacobian.Automorphism`

KernelBoundary

This aggregate re-exports the following parts of the Fox differential API: - `Discrete.KernelBoundary.IdentityAugmentation` - `Discrete.KernelBoundary.Basic` - `Discrete.KernelB...

Naturality

1 file | 4 declarations | 3 Theorems | 1 Definition

The principal declarations in this module are: - `relativeFreeFoxCoordinatesMap` A homomorphism of coefficient groups pushes a relative Fox-coordinate vector forward. - `relativ...