ProCGroups.FoxDifferential.Completed.FiniteStage

24 sections | 79 files | 553 declarations

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

Completed.FiniteStage.Basic - Completed.FiniteStage.Bifiltered - Completed.FiniteStage.BoundaryCycleHom - Completed.FiniteStage.BoundaryCycles - Completed.FiniteStage.BoundaryQuotient - Completed.FiniteStage.BoundarySubgroups - Completed.FiniteStage.CoeffMap - Completed.FiniteStage.MagnusQuotient - Completed.FiniteStage.PrimePower - Completed.FiniteStage.RelationAction - Completed.FiniteStage.RelationIdeal - Completed.FiniteStage.RelationIdealDerivative - Completed.FiniteStage.RelationIdealPrimitive - Completed.FiniteStage.RelationModule - Completed.FiniteStage.RelationRealization - Completed.FiniteStage.RelationSubmodule - Completed.FiniteStage.SemidirectCycles - Completed.FiniteStage.SourceBoundary - Completed.FiniteStage.SourceCycleReduction - Completed.FiniteStage.SourceDerivativeVector - Completed.FiniteStage.Stage - Completed.FiniteStage.TargetMap - Completed.FiniteStage.RelationReflection - Completed.FiniteStage.ClosedGeneratedCycles

imports

Imported by

ProCGroups.FoxDifferential.Completed

Basic

1 file | 17 declarations | 10 Theorems | 6 Definitions | 1 Instance

The principal declarations in this module are: - `foxCommutatorPowerRelatorSet` Relators defining the finite Fox source quotient: commutators in \(N\) and \(n\)-th powers in \(N...

Bifiltered

This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.Bifiltered.Transition` - `Completed.FiniteStage.Bifiltered.System` - `Complet...

BoundaryCycleHom

1 file | 8 declarations | 5 Theorems | 2 Definitions | 1 Abbreviation

The principal declarations in this module are: - `foxAlgebraicStageSourceKernel` The kernel of the finite source-to-target quotient \(F/[N,N]N^n \to F/N\). - `foxAlgebraicStageS...

BoundaryCycles

1 file | 13 declarations | 8 Theorems | 5 Definitions

The principal declarations in this module are: - `foxAlgebraicStageBoundaryCycleSubmodule` The finite-stage Fox boundary-cycle submodule \(\ker \partial\). - `foxAlgebraicStageS...

BoundaryQuotient

1 file | 6 declarations | 4 Theorems | 1 Definition | 1 Abbreviation

The principal declarations in this module are: - `foxAlgebraicStageCoordinateModuloRelations` Finite coordinate vectors modulo the submodule generated by finite relation boundar...

BoundarySubgroups

1 file | 7 declarations | 5 Theorems | 2 Definitions

The principal declarations in this module are: - `foxAlgebraicStageSemidirectBoundaryCycleSubgroup` Finite semidirect boundary cycles form a subgroup. - `foxAlgebraicStageSemidi...

ClosedGeneratedCycles

1 file | 2 declarations | 2 Theorems

The principal declarations in this module are: - `freeProCZCBifilteredAllFiniteQuotientStageCoeffMap_additive_basis` The bifiltered coefficient maps form an additive identity-qu...

CoeffMap

7 files | 32 declarations | 27 Theorems | 5 Definitions

This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.CoeffMap.Augmentation` - `Completed.FiniteStage.CoeffMap.Boundary` - `Complet...

MagnusQuotient

1 file | 15 declarations | 14 Theorems | 1 Definition

The principal declarations in this module are: - `foxAlgebraicStageSemidirectReindexHom` Reindex the finite-stage Fox semidirect target along an equivalence of free bases. - `fo...

PrimePower

This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.PrimePower.Completion` - `Completed.FiniteStage.PrimePower.Derivative` - `Com...

RelationAction

1 file | 8 declarations | 6 Theorems | 2 Definitions

The principal declarations in this module are: - `foxAlgebraicStageRelationConjBySource` Conjugating a finite-stage relation by an arbitrary source-quotient element gives anothe...

RelationIdeal

1 file | 13 declarations | 10 Theorems | 3 Definitions

The principal declarations in this module are: - `foxAlgebraicStageRelationAugmentationGenerator` The augmentation generator \(q-1\) attached to a finite-stage relation \(q \in ...

RelationIdealDerivative

1 file | 16 declarations | 15 Theorems | 1 Definition

The principal declarations in this module are: - `foxAlgebraicStageGroupAlgebraDerivativeVector` The vector of target-valued finite Fox derivatives of a source group-algebra ele...

RelationIdealPrimitive

1 file | 20 declarations | 15 Theorems | 5 Definitions

The principal declarations in this module are: - `foxAlgebraicStageSourceBoundaryPrimitive` An element of the source finite group algebra has a relation-compatible source Fox pr...

RelationModule

1 file | 14 declarations | 10 Theorems | 3 Definitions | 1 Abbreviation

The principal declarations in this module are: - `foxAlgebraicStageRelationGroup` The finite-stage relation group \(\ker(F/[N,N]N^n \to F/N)\). Its elements are exactly finite-s...

RelationRealization

1 file | 5 declarations | 5 Theorems

The principal declarations in this module are: - `foxAlgebraicStageSourceKernelDerivativeSet_zsmul_mem` The additive source-kernel derivative set is closed under integer multipl...

RelationReflection

1 file | 1 declaration | 1 Theorem

This module records the elementary equivalence between membership in a finite-stage relation submodule and vanishing in its quotient.

RelationSubmodule

1 file | 14 declarations | 11 Theorems | 3 Definitions

The principal declarations in this module are: - `foxAlgebraicStageRelationBoundarySubmodule` The \((\mathbb{Z}/n\mathbb{Z})[F/N]\)-submodule generated by finite-stage relation-...

SemidirectCycles

1 file | 16 declarations | 10 Theorems | 6 Definitions

The principal declarations in this module are: - `foxAlgebraicStageSemidirectSourceKernelPoint` The finite semidirect point \((Dq,1)\) attached to a source-quotient element. - `...

SourceBoundary

1 file | 15 declarations | 11 Theorems | 3 Definitions | 1 Abbreviation

The principal declarations in this module are: - `foxAlgebraicStageSourceCoordinateVector` Source-valued coordinate vectors over \((\mathbb{Z}/n\mathbb{Z})[F/([N,N]N^n)]\). - `f...

SourceCycleReduction

1 file | 9 declarations | 6 Theorems | 3 Definitions

The principal declarations in this module are: - `foxAlgebraicStageSourceBoundaryCycleSubmodule` Source boundary cycles in the source coordinate module. - `foxAlgebraicStageSour...

SourceDerivativeVector

1 file | 9 declarations | 7 Theorems | 2 Definitions

The principal declarations in this module are: - `foxAlgebraicStageSourceDerivativeVector` Source-valued derivative vector of a source quotient element. - `foxAlgebraicStageSour...

Stage

This aggregate re-exports the following parts of the Fox differential API: - `Completed.FiniteStage.Stage.Derivative` - `Completed.FiniteStage.Stage.Fundamental` - `Completed.Fi...

TargetMap

1 file | 9 declarations | 9 Theorems

The principal declarations in this module are: - `foxAlgebraicStageSemidirectMap_left` The left coordinate of the finite-stage semidirect point is the specified derivative compo...