Yamaguchi Lean 4 Library
ProCGroups.CrowellExactSequence
ProCGroups/CrowellExactSequence

ProCGroups.CrowellExactSequence

4 sections | 20 files | 105 declarations

The discrete and profinite Crowell--Blanchfield--Lyndon exact sequences, together with the shared four-term linear-sequence interface, the completed continuous Magnus comparison, and applications of the exact sequence.

This is the canonical public entry point for Crowell exact sequences in ProCGroups.

imports
Imported by

Applications

2 files | 2 declarations | 1 Theorem | 1 Definition
Applications of the profinite Crowell exact sequence, including the finite-rank criterion for free pro-\(C\) presentations.

Basic

1 file | 13 declarations | 8 Theorems | 3 Definitions | 1 Abbreviation | 1 Structure
Crowell exact sequences / Basic. This module contains the common four-term linear-sequence interface, exactness transport lemmas, and the finite Blanchfield--Lyndon coordinate m...

Discrete

5 files | 12 declarations | 6 Theorems | 6 Definitions
This aggregate exposes the discrete Magnus comparison and the assembled Crowell--Blanchfield--Lyndon exact sequence.

Profinite

12 files | 78 declarations | 60 Theorems | 17 Definitions | 1 Abbreviation
This exhaustive aggregate exposes the relation-reflection support, continuous Magnus criterion, and assembled profinite Crowell--Blanchfield--Lyndon sequence.