ProCGroups.FoxDifferential.Completed.FreeProC

22 sections | 27 files | 332 declarations

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

Completed.FreeProC.BifilteredCoefficientStageProjection - Completed.FreeProC.BifilteredStageProjection - Completed.FreeProC.BifilteredSystemStageProjection - Completed.FreeProC.CofinalQuotientKernelBasis - Completed.FreeProC.CoordinateStageProjection - Completed.FreeProC.Density - Completed.FreeProC.FiniteQuotientStages - Completed.FreeProC.PrimePowerStageProjection - Completed.FreeProC.ProCIntegerBifilteredStageProjection - Completed.FreeProC.ProCIntegerBifilteredStageRightProjection - Completed.FreeProC.ProCIntegerStageCoeffProjection - Completed.FreeProC.QuotientKernelBasis - Completed.FreeProC.RelationSubmoduleApproximation - Completed.FreeProC.SemidirectKernelBasis - Completed.FreeProC.SemidirectLift - Completed.FreeProC.StageApproximation - Completed.FreeProC.StageProjection - Completed.FreeProC.Uniqueness - Completed.FreeProC.RelationReflection - Completed.FreeProC.NaturalTopology - Completed.FreeProC.Coordinates - Completed.FreeProC.FundamentalFormula

imports

Imported by

ProCGroups.FoxDifferential.Completed

BifilteredCoefficientStageProjection

1 file | 14 declarations | 11 Theorems | 3 Definitions

The principal declarations in this module are: - `zcFreeFoxCoordinatesBifilteredStageMap` Coordinate maps attached to a compatible family of coefficient maps. - `freeProCZCCompl...

BifilteredStageProjection

1 file | 4 declarations | 4 Theorems

The principal declarations in this module are: - `freeProCZCCompletedFoxSemidirectStageMap_bifilteredTransition` Compatibility of two completed-to-finite stage maps with the bif...

BifilteredSystemStageProjection

1 file | 9 declarations | 7 Theorems | 2 Definitions

The principal declarations in this module are: - `freeProCZCCompletedFoxSemidirectBifilteredLimitMap` Assemble compatible completed-to-finite semidirect stage maps into a map to...

CofinalQuotientKernelBasis

1 file | 6 declarations | 6 Theorems

The principal declarations in this module are: - `HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le` Reindex an identity-neighborhood quotient-kernel basis along a c...

Coordinates

1 file | 6 declarations | 2 Theorems | 4 Definitions

The principal declarations in this module are: - `freeProCChosenULift_closedGeneratedCoordinateMap` The coordinate map determined by the chosen \(U\)-lifts has the specified clo...

CoordinateStageProjection

1 file | 14 declarations | 12 Theorems | 2 Definitions

The principal declarations in this module are: - `zcFreeFoxCoordinatesStageMap` Coordinatewise finite-stage projection on completed Fox vectors, induced by a coefficient ring ma...

Density

1 file | 22 declarations | 18 Theorems | 4 Definitions

The principal declarations in this module are: - `HasLeftOpenSubgroupNeighbourhoodBasis` Left open subgroup neighborhood basis, expressed as a proposition rather than a structur...

FiniteQuotientStages

1 file | 25 declarations | 15 Theorems | 8 Definitions | 2 Instances

The principal declarations in this module are: - `freeProCFiniteQuotientStageHom` The free-group map to a finite quotient of H induced by a family X \(\to\) H. - `freeProCFinite...

FundamentalFormula

1 file | 11 declarations | 11 Theorems

The principal declarations in this module are: - `freeProCChosenULift_closedGenerated_fundamental_formula_stageProj` At each finite stage, the chosen \(U\)-lift closed-generatio...

NaturalTopology

1 file | 8 declarations | 8 Theorems

The principal declarations in this module are: - `freeProCClosedGeneratedTarget_proC_of_surjective` For a surjective map from a free pro-\(C\) group, the closed-generated target...

PrimePowerStageProjection

1 file | 11 declarations | 9 Theorems | 2 Definitions

The principal declarations in this module are: - `freeProCZCCompletedFoxSemidirectPrimePowerStageMap` A completed Fox semidirect projection to the \(\ell^a\) finite stage. - `fr...

ProCIntegerBifilteredStageProjection

1 file | 9 declarations | 8 Theorems | 1 Definition

The principal declarations in this module are: - `zcCompletedGroupAlgebraBifilteredStageCoeffMap` The completed-to-finite coefficient map at a bifiltered stage, built from an ac...

ProCIntegerBifilteredStageRightProjection

1 file | 20 declarations | 16 Theorems | 4 Definitions

The principal declarations in this module are: - `zcCompletedGroupAlgebraBifilteredStageRightMap` The right quotient map attached to a bifiltered \(\mathbb{Z}_C\llbracket H\rrbr...

ProCIntegerStageCoeffProjection

1 file | 12 declarations | 10 Theorems | 2 Definitions

The principal declarations in this module are: - `zcCompletedGroupAlgebraStageToFoxAlgebraicStage` A finite stage of \(\mathbb{Z}_C\llbracket H\rrbracket\) maps to a finite Fox ...

QuotientKernelBasis

1 file | 4 declarations | 3 Theorems | 1 Definition

The principal declarations in this module are: - `HasIdentityQuotientKernelNeighbourhoodBasis` Quotient kernels form a neighborhood basis at the identity. For every open neighbo...

RelationReflection

This module supplies the finite free-basis family used to reflect completed Fox relations through finite quotient stages, and relates stagewise vanishing to equality in the comp...

RelationSubmoduleApproximation

1 file | 6 declarations | 6 Theorems

The principal declarations in this module are: - `boundaryCycles_subset_kernelClosure_of_relSubmoduleExact` Completed Fox density from finite-stage relation-submodule exactness....

SemidirectKernelBasis

1 file | 12 declarations | 8 Theorems | 4 Definitions

The principal declarations in this module are: - `HasAdditiveIdentityQuotientKernelNeighbourhoodBasis` Additive-coordinate quotient kernels form a neighborhood basis at zero. Th...

SemidirectLift

1 file | 79 declarations | 57 Theorems | 22 Definitions

The principal declarations in this module are: - `freeProCZCCompletedFoxSemidirectGenerator` The generator map into the completed Fox semidirect target attached to a basis-value...

StageApproximation

1 file | 6 declarations | 6 Theorems

The principal declarations in this module are: - `subset_closure_of_quotientKernel_stage_exact` Quotient-kernel density from exact finite-stage images. For each quotient stage \...

StageProjection

1 file | 16 declarations | 15 Theorems | 1 Definition

The principal declarations in this module are: - `freeProCZCCompletedFoxSemidirectStageMap` A semidirect projection from the completed Fox semidirect product to a finite Fox sta...

Uniqueness

6 files | 20 declarations | 19 Theorems | 1 Definition

This aggregate re-exports the following parts of the Fox differential API: - `Completed.FreeProC.Uniqueness.Derivative` - `Completed.FreeProC.Uniqueness.Existence` - `Completed....