ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus

1 section | 1 file | 1 declaration

This aggregate combines the reusable completed Magnus theory with the kernel-abelianization injectivity endpoint used in the Crowell exact sequence.

imports

ProCGroups.FoxDifferential.Completed.Continuous.Magnus
ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus.Injectivity

Imported by

ProCGroups.CrowellExactSequence.Profinite

Injectivity

1 file | 1 declaration | 1 Theorem

This module proves injectivity of the completed Magnus map on the abelianized presentation kernel, using the closed-commutator kernel calculation and the general kernel-injectiv...