Yamaguchi Lean 4 Library
ProCGroups.CrowellExactSequence.Profinite.SequenceMaps
ProCGroups/CrowellExactSequence/Profinite/SequenceMaps

ProCGroups.CrowellExactSequence.Profinite.SequenceMaps

2 sections | 2 files | 19 declarations

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

imports
Imported by

Basic

1 file | 6 declarations | 3 Theorems | 3 Definitions
This file defines the completed differential boundary and the maps from completed and separated differential modules to the completed \(\mathbb Z_C\)-group algebra. It proves th...

Exactness

1 file | 13 declarations | 13 Theorems
This file identifies the completed map with the boundary expressed in closed-generator coordinates and transfers exactness between finite-family, completed, and separated sequen...