Foundational corpus mapping FC05 Weibel

Status: Sweep II complete. C01–C10 and Appendix A are complete.

Canonical catalogue: FC05 — Weibel, An Introduction to Homological Algebra.

Pinned project baseline: Mathlib db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. Current Mathlib was refreshed 2026-09-06 to 5aedf732b6987e8c26ab3c9ebc855314f82b045f; declarations first appearing after 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, and relevant external Lean repositories. Strict bundle semantics apply throughout.

Provenance contract for FC05 C01

Chapter 1. Chain Complexes FC05

Provenance contract for FC05 C02

Chapter 2. Derived Functors FC05

Provenance contract for FC05 C03

Chapter 3. Tor and Ext FC05

Provenance contract for FC05 C04

Chapter 4. Homological Dimension FC05

Provenance contract for FC05 C05

Chapter 5. Spectral Sequences FC05

Provenance contract for FC05 C06

Chapter 6. Group Homology and Cohomology FC05

Provenance contract for FC05 C07

Chapter 7. Lie Algebra Homology and Cohomology FC05

Provenance contract for FC05 C08

Chapter 8. Simplicial Methods in Homological Algebra FC05

Provenance contract for FC05 C09

Chapter 9. Hochschild and Cyclic Homology FC05

Provenance contract for FC05 C10

Chapter 10. The Derived Category FC05

Provenance contract for FC05 CA

Appendix A. Category Theory Language FC05