ProCGroups.FoxDifferential.Completed.Continuous

12 sections | 31 files | 679 declarations

This aggregate imports the topology and continuity of completed Fox coordinates, their naturality and chain rules, free-source and universal constructions, topological-generation formulas, semidirect-kernel bases, automorphism formulas, and the resulting tail exactness theorems. The common algebraic CrossedHom interface is supplied by FoxDifferential.Common; finite-stage and completion-specific implementations are collected here.

imports

Imported by

ProCGroups.FoxDifferential.Completed

Automorphism

1 file | 13 declarations | 9 Theorems | 4 Definitions

The principal declarations in this module are: - `allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse` The named inverse linear map for the completed Fox-Jacobi...

ChainRule

3 files | 29 declarations | 22 Theorems | 5 Definitions | 2 Abbreviations

This aggregate re-exports the following parts of the Fox differential API: - `Completed.Continuous.ChainRule.Basic` - `Completed.Continuous.ChainRule.Iterated`

ClosedGeneratedCoordinates

5 files | 47 declarations | 41 Theorems | 6 Definitions

This aggregate collects the construction, equivalences, topology, and comparison formulas for closed-generated coordinates in completed Fox differential modules.

Free

6 files | 36 declarations | 34 Theorems | 2 Definitions

This aggregate re-exports the following parts of the Fox differential API: - `Completed.Continuous.Free.DiscreteGenerators` - `Completed.Continuous.Free.Rules`

Magnus

4 files | 10 declarations | 8 Theorems | 2 Definitions

This module collects the closed-generation, finite-stage kernel, and closed-commutator results for the completed Magnus map.

Naturality

1 file | 20 declarations | 18 Theorems | 2 Definitions

The principal declarations in this module are: - `zcCompletedFoxSemidirectMapTarget` Target functoriality for completed Fox semidirect products. - `zcCompletedFoxSemidirectMapTa...

PresentedCoordinates

1 file | 11 declarations | 7 Theorems | 4 Definitions

The principal declarations in this module are: - `presentedCompletedDifferentialFamilyMapProCInteger` The \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear family map sending the st...

SemidirectKernelBasis

1 file | 6 declarations | 6 Theorems

The principal declarations in this module are: - `finiteCoordinateZeroRectangularNeighbourhoods_pi` Finite-coordinate product neighborhoods in a function space contain coordinat...

TailExactness

1 file | 2 declarations | 2 Theorems

The principal declarations in this module are: - `exact_foxBoundaryMap_zcGroupLike_sub_one_of_topologicallyGenerates` If a finite family topologically generates \(H\), the corre...

TopologicalGeneration

1 file | 20 declarations | 16 Theorems | 3 Definitions | 1 Instance

Continuous crossed homomorphisms into Hausdorff targets are determined by their values on a topologically generating set. This module applies that principle to bundled completed...

Topology

1 file | 55 declarations | 23 Theorems | 6 Definitions | 26 Instances

The principal declarations in this module are: - `freeProCZCCompletedFoxBoundary` Source-shaped completed Fox boundary map for a finite generating set. It evaluates a vector of ...

Universal

This aggregate re-exports the following parts of the Fox differential API: - `Completed.Continuous.Universal.AugmentationQuotient` - `Completed.Continuous.Universal.Basic` - `Co...