CrowellExactSequence.Profinite.ContinuousMagnus

4 sections | 4 files | 12 declarations

This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.

ClosedGeneratedVector

1 files | 6 declarations | 5 Theorem | 1 Definition

The closed-generated continuous Fox derivative vector attached to a finite chosen free pro-\(C\) basis and a presentation map.

FiniteStageKernel

1 files | 4 declarations | 4 Theorem

Free-group comparison for the concrete closed-generated continuous Fox vector, with the right component already identified with the presentation map.

Injectivity

1 files | 1 declarations | 1 Theorem

Continuous Magnus injectivity for the displayed boundary \(d_N\): \(N^{\mathrm{ab}}(C)\) \(\to\) \(A_{\psi}(C)\). This step is obtained by combining the completed Fox-vector ker...

KernelClosedCommutator

1 files | 1 declarations | 1 Theorem

Concrete continuous Magnus kernel for the closed-generated completed Fox vector. It gives the injectivity step for \(d_N : N^{\mathrm{ab}}(C) \to \mathbb{Z}_C\llbracket H\rrbrac...