ProCGroups.FoxDifferential.Common

6 sections | 6 files | 177 declarations

This aggregate collects the algebraic interface shared by the discrete and completed theories: bundled crossed homomorphisms, their universal differential modules, Fox boundary identities, free-source differentials, finite-family linear maps, and Jacobian constructions. It does not choose a completion topology or a finite-stage coefficient system.

imports

Imported by

ProCGroups.FoxDifferential

CrossedDifferential

This module defines crossed homomorphisms for an additive group action and their scalar-character specialization. It supplies the Fox product, inverse, conjugation, commutator, ...

CrossedDifferentialModule

1 file | 33 declarations | 20 Theorems | 11 Definitions | 2 Abbreviations

The principal declarations in this module are: - `CrossedDifferentialPreModule` The free \(R\)-module on the underlying set of a group \(G\). - `crossedDifferentialRelationEleme...

FiniteFamilyLinearMap

1 file | 9 declarations | 7 Theorems | 2 Definitions

The principal declarations in this module are: - `finiteFamilyLinearMap` The linear map represented by a finite family of target vectors. - `piReindexLinearEquiv` Reindex finite...

FoxBoundary

1 file | 11 declarations | 8 Theorems | 3 Definitions

The principal declarations in this module are: - `coefficientFoxBoundary` The Fox boundary crossed differential attached to a coefficient homomorphism: \(g \mapsto \operatorname...

FreeCrossedDifferential

1 file | 50 declarations | 35 Theorems | 15 Definitions

The principal declarations in this module are: - `freeCrossedHomActionLift` The standard semidirect-product lift producing a free crossed homomorphism for an arbitrary additive ...

Jacobian

1 file | 13 declarations | 10 Theorems | 3 Definitions

The principal declarations in this module are: - `foxJacobianMatrix` A Fox-Jacobian family packaged as a finite matrix. - `foxJacobianId` The identity Fox-Jacobian family with K...