ProCGroups.FoxDifferential.Discrete.DifferentialModule

3 sections | 3 files | 50 declarations

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

Discrete.DifferentialModule.Boundary

import

ProCGroups.FoxDifferential.Discrete.DifferentialModule.Boundary

Imported by

ProCGroups.FoxDifferential.Discrete

Basic

1 file | 23 declarations | 13 Theorems | 7 Definitions | 3 Abbreviations

The principal declarations in this module are: - `GroupRing` The integral group ring \(\mathbb{Z}[H]\), realized as a monoid algebra. - `groupRingMap` A group homomorphism induc...

Boundary

1 file | 13 declarations | 9 Theorems | 4 Definitions

The principal declarations in this module are: - `groupRingBoundary` The standard map \(G \to \mathbb{Z}[H]\), \(g \mapsto \psi(g)-1\) is viewed as a differential map. - `groupR...

Universal

1 file | 14 declarations | 9 Theorems | 4 Definitions | 1 Abbreviation

The principal declarations in this module are: - `DifferentialHom` A \(\psi\)-differential map is a map satisfying the Fox Leibniz rule. - `liftLinear` The linear map out of the...