Foundational corpus mapping FC10 Serre Local Fields

Status: Sweep II complete. C01–C15 complete.

Canonical catalogue: FC10 — Serre, Local Fields.

Pinned project baseline: Mathlib db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. Current Mathlib was checked at 71a80585ee495fc24472fd0eaffc89d94e4fd8d6. Declarations first appearing after the project pin are revision-specific reference-port routes unless independently importable.

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, and targeted external Lean discovery. Strict bundle semantics apply throughout.

Provenance contract for FC10 C01

Chapter 1. Discrete Valuation Rings and Dedekind Domains FC10

Provenance contract for FC10 C02

Chapter 2. Completion FC10

Provenance contract for FC10 C03

Chapter 3. Discriminant and Different FC10

Provenance contract for FC10 C04

Chapter 4. Ramification Groups FC10

Provenance contract for FC10 C05

Chapter 5. The Norm FC10

Provenance contract for FC10 C06

Chapter 6. Artin Representation FC10

Provenance contract for FC10 C07

Chapter 7. Basic Facts FC10

Provenance contract for FC10 C08

Chapter 8. Cohomology of Finite Groups FC10

Provenance contract for FC10 C09

Chapter 9. Theorems of Tate and Nakayama FC10

Provenance contract for FC10 C10

Chapter 10. Galois Cohomology FC10

Provenance contract for FC10 C11

Chapter 11. Class Formations FC10

Provenance contract for FC10 C12

Chapter 12. Brauer Group of a Local Field FC10

Provenance contract for FC10 C13

Chapter 13. Local Class Field Theory FC10

Provenance contract for FC10 C14

Chapter 14. Local Symbols and Existence Theorem FC10

Provenance contract for FC10 C15

Chapter 15. Ramification FC10