Foundational corpus mapping FC13 Matsumura

Status: Sweep II complete. C00–C11 complete.

Canonical catalogue: FC13 — Matsumura, Commutative Ring Theory.

Pinned project baseline: Mathlib db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. Current Mathlib was refreshed 2026-09-07 to e281a66114fe17935e6ea7917a01b714d0c1e493 on Lean 4.34.0-rc2; 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, Loogle/LeanSearch/Mathlib documentation, Lean Reservoir, and discoverable external Lean repositories. Strict bundle semantics apply throughout.

Provenance contract for FC13 C00

Chapter 0. Conventions and terminology FC13

Provenance contract for FC13 C01

Chapter 1. Commutative rings and modules FC13

Provenance contract for FC13 C02

Chapter 2. Prime ideals FC13

Provenance contract for FC13 C03

Chapter 3. Properties of extension rings FC13

Provenance contract for FC13 C04

Chapter 4. Valuation rings, DVRs, Dedekind rings and Krull rings FC13

Provenance contract for FC13 C05

Chapter 5. Dimension theory FC13

Provenance contract for FC13 C06

Chapter 6. Regular sequences, Cohen–Macaulay and Gorenstein rings FC13

Provenance contract for FC13 C07

Chapter 7. Regular rings, UFDs and complete intersections FC13

Provenance contract for FC13 C08

Chapter 8. Local flatness and openness loci FC13

Provenance contract for FC13 C09

Chapter 9. Differentials, separability and higher derivations FC13

Provenance contract for FC13 C10

Chapter 10. Adic smoothness, Cohen structure and Jacobian criteria FC13

Provenance contract for FC13 C11

Chapter 11. Catenarity, formal fibres and normalization FC13