Foundational corpus mapping FC07 Hatcher

Status: Sweep II complete. C00–C04 and Appendix CA complete.

Canonical catalogue: FC07 — Hatcher, Algebraic Topology.

Pinned project baseline: Mathlib db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. Current upstream Mathlib was refreshed 2026-09-07 to 80cbd0498ab39e21d24d6730b3f932cec672a702 (Lean 4.34.0-rc2). Declarations outside the project pin are revision-specific reference-port routes unless an importable package route is independently justified.

Every canonical unit receives exactly one Sweep-II route: mathlib, project-existing, package-import, reference-port, or unmatched. Project source is searched first, followed by pinned/current Mathlib, open/current work, indexed search services, Reservoir/packages, broad discoverable Lean repositories, and local reference mirrors. Strict bundle semantics apply throughout.

Provenance contract for FC07 C00

Chapter 0. Some Underlying Geometric Notions FC07

Provenance contract for FC07 C01

Chapter 1. The Fundamental Group FC07

Provenance contract for FC07 C02

Chapter 2. Homology FC07

Provenance contract for FC07 C03

Chapter 3. Cohomology FC07

Provenance contract for FC07 C04

Chapter 4. Homotopy Theory FC07 ````

Provenance contract for FC07 CA

Appendix. Topology of Cell Complexes FC07