ProCGroups.FoxDifferential.Completed.Comparison

5 sections | 5 files | 87 declarations

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

Completed.Comparison.DiscreteCompletion - Completed.Comparison.FiniteStage - Completed.Comparison.QuotientFamily - Completed.Comparison.SourceProjection - Completed.Comparison.MagnusKernel

imports

Imported by

ProCGroups.FoxDifferential.Completed

DiscreteCompletion

1 file | 30 declarations | 29 Theorems | 1 Definition

The principal declarations in this module are: - `foxAlgebraicStageGroupRingReduction` Coefficient reduction from the integral group ring \(\mathbb{Z}[F/N]\) to the finite-stage...

FiniteStage

1 file | 23 declarations | 19 Theorems | 3 Definitions | 1 Abbreviation

The principal declarations in this module are: - `zcFiniteStageTarget` The finite-stage completed Fox target is the indicated group-ring quotient module. - `zcCompletedGroupAlge...

MagnusKernel

1 file | 13 declarations | 13 Theorems

This module transfers discrete Magnus-kernel criteria through finite algebraic stages and completed Fox differential coordinates.

QuotientFamily

The principal declarations in this module are: - `ZCFiniteStageQuotientBundle` A bundled finite-stage quotient family for source-stage comparison theorems. The purpose is to car...

SourceProjection

1 file | 5 declarations | 5 Theorems

The principal declarations in this module are: - `freeProCZCCompletedFoxBoundary_finiteStageProjection` Finite-stage projection of the source-shaped completed Fox boundary map. ...