FoxDifferential.Completed.Comparison

4 sections | 4 files | 66 declarations

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

DiscreteCompletion

1 files | 30 declarations | 29 Theorem | 1 Definition

Coefficient reduction from the integral group ring \(\mathbb{Z}[F/N]\) to the finite-stage target group algebra \((\mathbb{Z}/n\mathbb{Z})[F/N]\).

FiniteStage

1 files | 23 declarations | 21 Theorem | 1 Definition | 1 Abbreviation

The finite-stage completed Fox target is the indicated group-ring quotient module.

QuotientFamily

1 files | 9 declarations | 5 Theorem | 3 Abbreviation | 1 Structure

A bundled finite-stage quotient family for source-stage comparison theorems. The purpose is to carry the topology and topological-group structure on the quotient target once, in...

SourceProjection

1 files | 4 declarations | 4 Theorem

The finite-stage projection of the source-shaped completed Fox boundary map.