FoxDifferential.Discrete.KernelBoundary

5 sections | 5 files | 150 declarations

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

Basic

1 files | 29 declarations | 15 Theorem | 12 Definition | 2 Abbreviation

Additive form of the kernel abelianization map.

The kernel-boundary codomain carries the trivial multiplication action.

1 files | 43 declarations | 31 Theorem | 10 Definition | 2 Abbreviation

For a representation of a subsingleton monoid, taking coinvariants does not change the underlying module.

1 files | 2 declarations | 2 Theorem

The surjective-case linear kernel-boundary map is injective in the Magnus-kernel comparison.

1 files | 20 declarations | 13 Theorem | 6 Definition | 1 Abbreviation

The quotient of \(A_{\psi}\) by the image of the head map.