ProCGroups.CrowellExactSequence.Profinite

This module gives the completed Blanchfield--Lyndon boundary maps and exact sequences in canonical lifted coordinates. Concrete `Fin n` formulations are obtained by reindexing o...

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

This file reduces exactness at the separated completed differential module to integration of coordinate cycles. It derives the middle image/kernel equality from finite-stage lif...

For a free pro-\(C\) source, this file combines continuous Magnus injectivity, the completed boundary calculation, and bifiltered finite-stage exactness. The resulting theorems ...

This file constructs the completed and separated boundary maps on the kernel of a profinite presentation. It proves that these maps kill commutators and gives continuity criteri...

This file factors the completed Crowell boundary through the topological abelianization of the kernel. It proves that the resulting boundary is annihilated by the completed diff...

This module packages the separated completed Crowell and Blanchfield--Lyndon sequences as `FourTermLinearSequence` values and states their exactness theorems under the required ...

This aggregate exposes the completed Crowell sequence maps and their exactness properties.