Class field theory roadmap: class formations, Tate–Nakayama, and Artin reciprocity (revision of #250)

[CBirkbeck]

Dependencies: this roadmap depends on Profinite Cohomology #188, Local Fields and Ramification #189, Number-Field Arithmetic #191, and Global Number Fields #245, and should merge after them.

Relation to #250: this branch is built on the head of #250 (fc9257f) and is offered as a revised version of that roadmap. The last commit is the whole change; a summary is posted on #250.

Summary

This replaces the class-field-theory roadmap by one centred on abstract class formations in the sense of Artin–Tate. The spine is

formation
  -> class-formation axioms
  -> fundamental classes
  -> Tate–Nakayama
  -> finite-level Artin maps
  -> local and global reciprocity
  -> existence theorems,

and the material of #250 that does not construct the Artin map — the local Brauer group and cohomological Hilbert symbol, local Tate duality and Euler characteristics, local conductors, the cyclic Hasse norm theorem, Hilbert/narrow/ray/ring class fields, Kronecker–Weber, and Hilbert reciprocity — is kept as Layers 8–10 on top of that spine, together with the local Weil group and quadratic reciprocity as the explicit reciprocity law. The frozen names consumed by LocalGaloisGroups, GlobalQuadraticForms and QuadraticFormInvariants are unchanged.

Finite-group Tate cohomology and continuous profinite cohomology are consumed from Mathlib, the kbuzzard/ClassFieldTheory development, and ProfiniteCohomology. They are not redefined here.

Main design decisions

• ClassFormation contains the invariant maps and their compatibility, but no chosen fundamental class. The fundamental class is the unique class of invariant 1/[U:V].
• tateIso — Tate's theorem for the class formation (Artin–Tate's Main Theorem; the M = ℤ case, not the Tate–Nakayama tensor-product generalization) — is required to have cup product with the fundamental class as its underlying homomorphism in every integer degree.
• The degree -2 → 0 cup-product direction is nakayamaNegTwo : (U/V)^ab ≃ A^U/N(A^V); the Artin reciprocity direction is its inverse artinEquiv, and artinMap is the composite with the quotient map. In Suggested.lean these are ordinary definitions with bodies, so artinMap_apply and artinEquiv_eq_tateIso are rfl; only the leaves carry sorry. The character formula χ(artinMap a) = inv(a₀ ∪ δχ) is also required and fixes the sign independently.
• The finite local and global Artin maps are transparent transports of the abstract map; normResidue is the multiplicative form of localArtinEquiv, not a second construction. The absolute local artinMap, unramifiedCoordinate and cyclotomicCharacter_artinMap (with the field norm) are kept as in Add roadmap: Class field theory #250.
• Arithmetic Frobenius everywhere: a uniformizer in an unramified local extension maps to arithmetic Frobenius, and Art((ℓ))(ζ_m) = ζ_m^ℓ.

Regression tests

The roadmap requires explicit tests, stated in Suggested.lean: the trivial layer; kernel/quotient and cyclic-layer formulae; an unramified local extension; a quadratic extension and its norm subgroup; ℚ(i)/ℚ (primes 1 mod 4 trivial, 3 mod 4 complex conjugation); ℚ(√5)/ℚ; ℚ(ζ_m)/ℚ with Art((ℓ))(ζ_m) = ζ_m^ℓ; the local example ℚ₂(ζ₅)/ℚ₂ where 2 maps to ζ₅ ↦ ζ₅²; and compatibility between ℚ(ζ₅) and ℚ(√5). The cyclotomic test is essential because a quadratic example cannot distinguish Frobenius from its inverse.

Lean status

Suggested.lean (1500 lines, 199 declarations, 147 sorry targets, no other warnings) imports the four supplier Suggested.lean files, like #250. It type-checks against those files at their current heads (#188 60fe818, #189 8ffd411, #191 041929b, #245 351636e) on this repository's Mathlib pin 05ae0103; CI will stay red until the suppliers merge, exactly as for #250. Everything is stated in universe 0, because Mathlib's tateCohomology keeps the finite group and the coefficient ring in one universe.

The def_wanted/theorem_wanted idiom of an earlier draft does not exist in Lean/Batteries (only proof_wanted does, and it discards the declaration); the file uses ordinary definitions with bodies for the derived Artin maps instead, which is what makes the chain definitional.

Also registers ClassFieldTheory in the issue-template area dropdowns, as .github/scripts/check_roadmap_areas.py requires.

Files

• TauCetiRoadmap/ClassFieldTheory/README.md: normative roadmap
• TauCetiRoadmap/ClassFieldTheory/Suggested.lean: representative public contracts and acceptance tests
• .github/ISSUE_TEMPLATE/*.yml: area dropdown entries

🤖 Generated with Claude Code