FoxDifferential.Completed.FreeProC

Coordinate maps attached to a compatible family of coefficient maps.

Compatibility of two completed-to-finite stage maps with the bifiltered finite transition. Equivalently, if the left completed coordinate maps commute with the combined coeffici...

Assemble compatible completed-to-finite semidirect stage maps into a map to the bifiltered inverse limit.

Reindex an identity-neighborhood quotient-kernel basis along a cofinal refinement of kernels. The hypothesis says that every kernel in the original quotient family contains the ...

Coordinatewise finite-stage projection on completed Fox vectors, induced by a coefficient ring map \(\mathbb{Z}_C\llbracket H\rrbracket \to (\mathbb{Z}/n\mathbb{Z})[F/N]\).

A direct neighborhood approximation criterion for set-theoretic closure. This is the form used when a finite-stage argument has already produced an algebraic point of S inside e...

The free-group map to a finite quotient of H induced by a family X \(\to\) H.

A completed Fox semidirect projection to the \(\ell^a\) finite stage.

The completed-to-finite coefficient map at a bifiltered stage, built from an actual \(\mathbb{Z}_C\llbracket H\rrbracket\) stage projection.

The right quotient map attached to a bifiltered \(\mathbb{Z}_C\llbracket H\rrbracket\) stage. It is not independent data: it is the quotient map \(H \to H/U_j\) followed by the ...

A finite stage of \(\mathbb{Z}_C\llbracket H\rrbracket\) maps to a finite Fox target group algebra once its coefficient modulus dominates \(n\) and its finite quotient maps to \...

Quotient kernels form a neighborhood basis at the identity. For every open neighborhood of 1, some finite-stage kernel is contained in it. In a topological group this is the nat...

Completed Fox density from finite-stage relation-submodule exactness.

Additive-coordinate quotient kernels form a neighborhood basis at zero. This is the additive analogue of HasIdentityQuotientKernelNeighborhoodBasis. It is used for the left coor...

The generator map into the completed Fox semidirect target attached to a basis-value map \(\varphi: X \to H\).

Quotient-kernel density from exact finite-stage images. For each quotient stage \(j\), let \(T_{\mathrm{stage}}(j)\) be the image condition satisfied by points of \(T\), and let...

A semidirect projection from the completed Fox semidirect product to a finite Fox stage, constructed from a left coordinate map and a right target quotient map. The only compati...

Free pro-C sources are treated through completed Fox derivatives, stage projections, density arguments, and semidirect lift formulas.