Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.Continuous.Magnus
ProCGroups/FoxDifferential/Completed/Continuous/Magnus

ProCGroups.FoxDifferential.Completed.Continuous.Magnus

3 sections | 3 files | 10 declarations

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

imports
Imported by

ClosedGeneratedVector

1 file | 6 declarations | 4 Theorems | 2 Definitions
This module bundles the completed Fox derivative vector as a scalar crossed homomorphism, first over pro-\(C\) integers and then over the presented coefficient ring. It also rec...

FiniteStageKernel

1 file | 3 declarations | 3 Theorems
This module compares the completed Magnus map with its finite quotient stages and characterizes the kernel through the corresponding discrete Fox calculation.

KernelClosedCommutator

1 file | 1 declaration | 1 Theorem
This module identifies the kernel of the completed Magnus map with the closed commutator subgroup of the presentation kernel, using the finite-stage kernel comparison and the pr...