FoxDifferential.Completed.DifferentialModule.TargetQuotient

5 sections | 5 files | 13 declarations

The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.

Basic

1 files | 3 declarations | 2 Theorem | 1 Definition

The completed Fox-differential map is continuous with respect to the inverse-limit topology on the completed coefficient modules.

Fundamental

1 files | 2 declarations | 2 Theorem

The completed Fox derivative satisfies the fundamental formula after passage to the target quotient.

MulProjection

1 files | 1 declarations | 1 Theorem

The finite-stage projection of the prime-power completed target derivative satisfies the Fox product rule.

StageMap

1 files | 3 declarations | 3 Theorem

At a completed finite stage of \(F/N\), the completed map induced by \(F \to F/N\) agrees with first projecting to the completed free derivative source finite quotient and then ...

Surjective

1 files | 4 declarations | 3 Theorem | 1 Definition

The quotient homomorphism \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective. This specialized form is used to lift coefficients from \(\mathbb{Z}_{\ell}\llbrac...