ProCGroups.FoxDifferential.Completed.FiniteStage.CoeffMap

6 sections | 6 files | 32 declarations

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

Completed.FiniteStage.CoeffMap.Augmentation - Completed.FiniteStage.CoeffMap.Boundary - Completed.FiniteStage.CoeffMap.BoundaryCycles - Completed.FiniteStage.CoeffMap.Semidirect - Completed.FiniteStage.CoeffMap.Source - Completed.FiniteStage.CoeffMap.Target

imports

Imported by

ProCGroups.FoxDifferential.Completed.FiniteStage

Augmentation

1 file | 1 declaration | 1 Theorem

The principal declarations in this module are: - `foxCommutatorPowerSourceGAAugmentation_powerSourceGAMap` Source augmentation commutes with finite-stage coefficient/source redu...

Boundary

1 file | 2 declarations | 2 Theorems

The principal declarations in this module are: - `foxAlgebraicStageFoxBoundary_coeffMap` Coefficient reduction commutes with the finite-stage Fox boundary map. - `foxAlgebraicSt...

BoundaryCycles

1 file | 7 declarations | 7 Theorems

The principal declarations in this module are: - `foxAlgebraicStageSemidirectCoeffMap_left` The left component of finite-stage semidirect coefficient reduction is obtained by re...

Semidirect

1 file | 4 declarations | 3 Theorems | 1 Definition

The principal declarations in this module are: - `foxAlgebraicStageSemidirectCoeffMap` Coefficient-reduction map on finite-stage semidirect Fox targets. - `foxAlgebraicStageSemi...

Source

1 file | 10 declarations | 7 Theorems | 3 Definitions

The principal declarations in this module are: - `foxAlgebraicStageSameSourceGroupAlgebraCoeffMap` Coefficient-reduction map on a fixed finite Fox source quotient. - `foxAlgebra...

Target

1 file | 8 declarations | 7 Theorems | 1 Definition

The principal declarations in this module are: - `foxAlgebraicStageTargetGroupAlgebraCoeffMap` Coefficient-reduction map on finite-stage target group algebras for a divisor \(n ...