FC05 — Weibel, An Introduction to Homological Algebra
This book contains 241 definitions, 94 theorems, 62 propositions, 90 lemmas, 115 corollaries, 137 examples, 106 constructions, 8 remarks, 16 conventions, 3 notations, 1 criterion and 186 other statements.
1,059 of its 1,059 statements have been checked against Lean; 288 of those are formalized somewhere.
| Chapter | Definitions | Theorems, propositions | Lemmas, corollaries | Everything else | Formalized | Not formalized |
|---|---|---|---|---|---|---|
| Chapter 1. Chain Complexes | 19 | 5 | 8 | 36 | 43 | 25 |
| Chapter 2. Derived Functors | 18 | 9 | 14 | 41 | 48 | 34 |
| Chapter 3. Tor and Ext | 10 | 14 | 17 | 25 | 5 | 61 |
| Chapter 4. Homological Dimension | 11 | 17 | 17 | 41 | 14 | 72 |
| Chapter 5. Spectral Sequences | 23 | 12 | 11 | 34 | 7 | 73 |
| Chapter 6. Group Homology and Cohomology | 31 | 25 | 30 | 68 | 53 | 101 |
| Chapter 7. Lie Algebra Homology and Cohomology | 14 | 8 | 23 | 35 | 17 | 63 |
| Chapter 8. Simplicial Methods in Homological Algebra | 26 | 14 | 15 | 51 | 24 | 82 |
| Chapter 9. Hochschild and Cyclic Homology | 36 | 33 | 44 | 51 | 14 | 150 |
| Chapter 10. The Derived Category | 27 | 18 | 26 | 50 | 24 | 97 |
| Appendix A. Category Theory Language | 26 | 1 | — | 25 | 39 | 13 |
What the book contains
| Kind of statement | Count |
|---|---|
| Definitions | 241 |
| Theorems | 94 |
| Propositions | 62 |
| Lemmas | 90 |
| Corollaries | 115 |
| Examples | 137 |
| Constructions | 106 |
| Remarks | 8 |
| Conventions | 16 |
| Notations | 3 |
| Criteria | 1 |
| Other statements | 186 |
| Total | 1,059 |
Where its statements stand in Lean
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 771 | 73% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 266 | 25% | Mathlib states and proves it. |
| in another Lean project | 18 | 2% | Some other Lean development has it; using it means porting that code. |
| in lean-categories | 4 | 0% | This repository states and proves it. |
| checked in total | 1059 |
How this book was read
Corpus source: FC05 in Foundational source corpus v1 (frozen).
This is the canonical Sweep-I source-unit catalogue for FC05. Stable source-local IDs are consumed unchanged by Sweeps II–IV.
Frozen source: Weibel - 1994 - An Introduction to Homological Algebra.md
Scope: complete book, Chapters 1–10 and Appendix A; exercises excluded item-by-item. Stable source-unit IDs are in source order and are the identifiers retained by later foundational-corpus sweeps.
Coverage: 1059 source units. Chapter counts: C01=68, C02=82, C03=66, C04=86, C05=80, C06=154, C07=80, C08=106, C09=164, C10=121, CA=52.