ProCGroups.FoxDifferential.Discrete.KernelBoundary

6 sections | 6 files | 152 declarations

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

Discrete.KernelBoundary.IdentityAugmentation - Discrete.KernelBoundary.Basic - Discrete.KernelBoundary.Homology - Discrete.KernelBoundary.Quotient - Discrete.KernelBoundary.MagnusKernel - Discrete.KernelBoundary.MagnusComparison

imports

Imported by

ProCGroups.FoxDifferential.Discrete

Basic

1 file | 29 declarations | 15 Theorems | 12 Definitions | 2 Abbreviations

The principal declarations in this module are: - `KernelAbelianizationAdd` Additive form of the kernel abelianization map. - `kernelBoundary` The kernel of \(\psi\) maps multipl...

Homology

The principal declarations in this module are: - `kernelGroupRingRep` The left-multiplication representation of \(\ker \psi\) on \(\mathbb{Z}[G]\). - `kernelSplitEquiv` A sectio...

IdentityAugmentation

1 file | 43 declarations | 31 Theorems | 10 Definitions | 2 Abbreviations

The principal declarations in this module are: - `coinvariantsLEquivOfSubsingleton` For a representation of a subsingleton monoid, taking coinvariants does not change the underl...

MagnusComparison

1 file | 2 declarations | 2 Theorems

This module compares the relative free Fox derivative with the universal differential and deduces the discrete Magnus-kernel criterion in relative Fox coordinates.

MagnusKernel

1 file | 2 declarations | 2 Theorems

The principal declarations in this module are: - `kernelAbelianizationBoundaryLinearOfSurjective_injective` The surjective-case linear kernel-boundary map is injective in the Ma...

Quotient

1 file | 20 declarations | 12 Theorems | 7 Definitions | 1 Abbreviation

The principal declarations in this module are: - `HeadQuotientOfSurjective` The quotient of \(A_{\psi}\) by the image of the head map. - `toIdentityDifferentialModule` The canon...