CrowellExactSequence/Profinite.lean

1import CrowellExactSequence.Profinite.FiniteRank

2import CrowellExactSequence.Profinite.MainTheorem

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/CrowellExactSequence/Profinite.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

12/-!

13# Profinite Crowell exact sequence over pro-C integer coefficients

15This is the profinite public entry point. It exposes the finite-coordinate Blanchfield--Lyndon

16maps, the completed Crowell exactness route, and the paper sequence

18```text

19N^ab(C) -> A_psi(C) -> Z_C[[H]] -> Z_C

20```

22and its finite-basis Blanchfield--Lyndon coordinate expression through

23`CrowellExactSequence.Profinite.MainTheorem`.