ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient

5 sections | 5 files | 13 declarations

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

Completed.DifferentialModule.TargetQuotient.Basic - Completed.DifferentialModule.TargetQuotient.Fundamental - Completed.DifferentialModule.TargetQuotient.MulProjection - Completed.DifferentialModule.TargetQuotient.StageMap - Completed.DifferentialModule.TargetQuotient.Surjective

imports

Imported by

ProCGroups.FoxDifferential.Completed.DifferentialModule

Basic

1 file | 3 declarations | 2 Theorems | 1 Definition

The principal declarations in this module are: - `foxAlgebraicStageTargetQuotientContinuousMonoidHom` The completed Fox-differential map is continuous with respect to the invers...

Fundamental

1 file | 2 declarations | 2 Theorems

The principal declarations in this module are: - `ppCompletedGAFoxDerivToTarget_of_fundFormula_map` The completed Fox derivative satisfies the fundamental formula after passage ...

MulProjection

1 file | 1 declaration | 1 Theorem

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_mul_projection` The finite-stage projection of the prime-powe...

StageMap

1 file | 3 declarations | 3 Theorems

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraMapStage_targetQuotient_transition_source` At a completed finite stage of \(F/N\), the completed...

Surjective

1 file | 4 declarations | 3 Theorems | 1 Definition

The principal declarations in this module are: - `primePowerCompletedGroupAlgebraMap_targetQuotient_lift` A noncomputable lift of a completed target group-algebra coefficient to...