FoxDifferential.Completed.Continuous

9 sections | 21 files | 626 declarations

This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Automorphism

1 files | 13 declarations | 9 Theorem | 4 Definition

The named inverse linear map for the completed Fox-Jacobian of a continuous automorphism.

ChainRule

3 files | 29 declarations | 22 Theorem | 5 Definition | 2 Abbreviation

The target generator map pulled back along a continuous homomorphism of free pro-\(C\) sources.

Free

6 files | 39 declarations | 37 Theorem | 2 Definition

Boundary-map form of the source-shaped completed Fox formula for the canonical free pro-\(C\) semidirect lift.

Naturality

1 files | 20 declarations | 18 Theorem | 2 Definition

The completed group-algebra map induced by a continuous target homomorphism is continuous.

SemidirectKernelBasis

1 files | 6 declarations | 6 Theorem

Finite-coordinate product neighborhoods in a function space contain coordinate rectangles. This is the generic topological input needed to pass from coefficient-kernel bases for...

TailExactness

1 files | 2 declarations | 2 Theorem

If a finite family topologically generates \(H\), the corresponding completed finite Fox boundary is exact at \(\mathbb{Z}_C\llbracket H\rrbracket\).

TopologicalGeneration

1 files | 20 declarations | 16 Theorem | 3 Definition | 1 Instance

Continuous crossed differentials with the same coefficients are determined by a topological generating set.

Topology

1 files | 59 declarations | 27 Theorem | 6 Definition | 26 Instance

The finite quotients of the all-finite pro-\(C\) predicate are exactly finite groups.

Universal

Wrapper for the `FoxDifferential.Completed.Continuous.Universal` folder.