FC06 — Hartshorne, Algebraic Geometry
This book contains 175 definitions, 101 theorems, 162 propositions, 48 lemmas, 81 corollaries, 187 examples, 52 constructions, 122 remarks, 15 conventions, 3 notations and 23 other statements.
969 of its 969 statements have been checked against Lean; 140 of those are formalized somewhere.
| Chapter | Definitions | Theorems, propositions | Lemmas, corollaries | Everything else | Formalized | Not formalized |
|---|---|---|---|---|---|---|
| Hartshorne, Algebraic Geometry — Chapter I: Varieties | 42 | 44 | 17 | 44 | 32 | 115 |
| Hartshorne, Algebraic Geometry — Chapter II: Schemes | 79 | 83 | 28 | 135 | 82 | 243 |
| Hartshorne, Algebraic Geometry — Chapter III: Cohomology | 25 | 63 | 39 | 77 | 23 | 181 |
| Hartshorne, Algebraic Geometry — Chapter IV: Curves | 18 | 33 | 19 | 78 | 2 | 146 |
| Hartshorne, Algebraic Geometry — Chapter V: Surfaces | 11 | 40 | 26 | 68 | 1 | 144 |
What the book contains
| Kind of statement | Count |
|---|---|
| Definitions | 175 |
| Theorems | 101 |
| Propositions | 162 |
| Lemmas | 48 |
| Corollaries | 81 |
| Examples | 187 |
| Constructions | 52 |
| Remarks | 122 |
| Conventions | 15 |
| Notations | 3 |
| Other statements | 23 |
| Total | 969 |
Where its statements stand in Lean
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 829 | 86% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 137 | 14% | Mathlib states and proves it. |
| in another Lean project | 2 | 0% | Some other Lean development has it; using it means porting that code. |
| in lean-categories | 1 | 0% | This repository states and proves it. |
| checked in total | 969 |
How this book was read
Corpus source: FC06 in Foundational source corpus v1 (frozen).
This is the canonical Sweep-I source-unit catalogue for FC06. Stable source-local IDs are consumed unchanged by Sweeps II–IV.
Frozen source: /home/dzack/Zotero/storage/AMY5NQZM/[Hartshorne 2008] Algebraic geometry.md
Scope: Chapters I–V only. Section-end exercises are excluded item-by-item. Appendices A–C are outside FC06. Stable IDs are chapter-local and source-ordered; dependencies point only to strictly earlier FC06 units.