Add roadmap: Class field theory

[roed-math]

Dependencies: This roadmap depended on #188 → #244 → #189 → #191 → #245, which have now been merged.

Summary

This roadmap organizes local and global class field theory around abstract class formations, canonical Mathlib/supplier Tate cohomology, fundamental classes derived from invariant maps, and the resulting Tate isomorphism. It then develops local invariant maps, local reciprocity and duality, global Artin reciprocity and existence, norm theorems and class fields, Hilbert reciprocity, and ring class fields.

The PR contains the normative README.md, representative target signatures in Suggested.lean, and the root index/import updates.

Ownership

It uses the canonical modulus/ray/idele/Hecke/order/Picard carriers from Global Number Fields, the ideal Artin map from #191, and canonical Tate maps rather than storing shadow restriction/corestriction fields. It owns the cohomological Hilbert pairing and product formula; it has no dependency on Quadratic Form Invariants or pro-p group theory. It exports local duality and Euler-characteristic data to Local Galois Groups and reciprocity contracts to Global Quadratic Forms.

The local-norm contract is completion-level: IsLocalNormEverywhere quantifies the norm ranges of the canonical finite and archimedean étale algebras, principalIdele_mem_range_ideleNormMap_iff bridges those predicates to the idelic norm range, and isGlobalNorm_iff_isLocalNormEverywhere composes that bridge with the cyclic Hasse norm theorem.

Port history

This is a clean port of roed-math/TauCetiRoadmap#6, rebased onto upstream main. Finite-group Tate theory, class formations, local reciprocity, and local duality were moved here from the former Local Fields roadmap; arithmetic carriers moved to Global Number Fields and Hasse–Minkowski moved to Global Quadratic Forms. The non-normative PROVENANCE.md is omitted from this upstream port; the detailed migration ledger remains private.

Human review priorities

• the exact four-way supplier boundary stated above;
• the class-formation spine, canonical Tate maps, invariant 1/n, cup-product normalization, and Artin conventions;
• local/global class-formation and duality hypotheses;
• the finite and archimedean local norm carriers, the local-coordinate/idele bridge, and its use in the cyclic Hasse norm theorem;
• the acyclic Hilbert-pairing contract consumed by quadratic-form roadmaps.

Validation

• lake -Kjobs=1 build TauCetiRoadmap.ClassFieldTheory.Suggested
• python3 .github/scripts/check_roadmap_areas.py
• git diff --check

AI and external formalization disclosure

The roadmap and restructuring were prepared with substantial assistance from Claude Fable and Opus 5, and GPT-5.6 Codex and Pro, under the author's direction. A detailed migration and coordination ledger is maintained privately. No external source code was copied into this roadmap.

[CBirkbeck]

Posted with Claude Code on Chris's behalf; the revised roadmap was drafted by Chris with ChatGPT 5.6 Pro and then checked, extended and type-checked by Claude.

I have put a revised version of this roadmap up as #261, built directly on this branch's head fc9257f so that the difference is a single commit: 6b76d74 (compare). It keeps everything this PR already gets right — the four supplier dependencies, arithmetic Frobenius, invariant 1/n for the fundamental class, cup product with the fundamental class for Tate–Nakayama, uniformizer ↦ Frobenius, comparison with artinHomAway, and the local and global class formations as the common source of reciprocity — and proposes the following changes.

Reorganise the spine around abstract class formations (Artin–Tate XIV). The build order becomes formation → class-formation axioms → fundamental classes → Tate–Nakayama → finite-level Artin maps → local/global reciprocity → existence, and only then the downstream theory.

Current PR	Revision
FiniteClassFormation stores a chosen class for every subgroup	ClassFormation stores the invariant maps; fundamentalClass is derived as the unique class of invariant 1/[U:V]
private tateH, tateMap, tateRes, tateCor, tateCup prototypes	consume Mathlib's tateCohomology (present at the pin, with δ, the long exact sequence and isoGroupCohomology) and the Richard Hill / kbuzzard/ClassFieldTheory material; add missing generic API to the supplier, not here
tateNakayama asserts bijectivity of a locally defined cup map	tateIso (Tate's theorem for the class formation, Artin–Tate's Main Theorem; "Tate–Nakayama" is reserved for Nakayama's tensor-product generalization in the supplier) is a named equivalence whose homomorphism is required to equal cup with the fundamental class in every degree
normResidue is a separate local definition	artinEquiv is definitionally the inverse of the degree -2 → 0 Nakayama map; the local and global maps are transports of it, and normResidue is the multiplicative form of localArtinEquiv
normalization mostly in prose	ordinary definitions with bodies (nakayamaNegTwo, artinEquiv := nakayamaNegTwo.symm, artinMap), so artinMap_apply and artinEquiv_eq_tateIso are rfl; a character formula χ(artinMap a) = inv(a₀ ∪ δχ); and mandatory regression tests: trivial layer, unramified (localArtinMap_uniformizer), quadratic, ℚ(i), ℚ(√5), ℚ(ζ_m) with Art((ℓ))(ζ_m) = ζ_m^ℓ, ℚ₂(ζ₅)/ℚ₂ with 2 ↦ (ζ₅ ↦ ζ₅²), and the ℚ(ζ₅)/ℚ(√5) tower — a quadratic example cannot distinguish Frobenius from its inverse, the cyclotomic one can

Keep the downstream theory. Local Tate duality and Euler characteristics, the cohomological Hilbert symbol, conductors, the cyclic Hasse norm theorem, Hilbert/narrow/ray/ring class fields, Kronecker–Weber and Hilbert reciprocity stay in the roadmap as Layers 8–10 on top of the spine, with the same frozen names (normResidue, artinMap, unramifiedCoordinate, cyclotomicCharacter_artinMap, tateDualityPairing_perfect_mixed, eulerCharacteristic_finrank_fp, localSymbol, cyclicHasseNorm, hilbertProductFormula, ringClassField, …) so that LocalGaloisGroups, GlobalQuadraticForms and QuadraticFormInvariants are unaffected. Added: the local Weil group with Kˣ ≃ W_K^ab, and quadratic reciprocity as the explicit reciprocity law derived from hilbertProductFormula.

Lean. Suggested.lean type-checks against the supplier Suggested.lean files at their current heads (#188 60fe818, #189 8ffd411, #191 041929b, #245 351636e) on the repository's Mathlib pin: 199 declarations, 147 sorry targets, no other warnings. As here, CI stays red until the suppliers merge. Two things worth flagging from that check: Mathlib's tateCohomology forces the finite group and ℤ into one universe, so the whole file is stated in universe 0; and .github/scripts/check_roadmap_areas.py wants ClassFieldTheory added to the two issue-template dropdowns, which #261 does.

Happy to fold any of this back into this PR instead if you prefer to keep #250 as the vehicle.

[roed-math]

GPT-5.6 Sol: Thank you. I integrated the offered revision into #250 (the 6b76d74 change appears here as cherry-picked commit 9c81af1), preserving this PR as the vehicle. I then added the named equivalence between global norms and norms at every completion for the Global Quadratic Forms consumer. The revised Suggested.lean elaborates against the four supplier contracts in the stacked local check.

[CBirkbeck]

Posted with Claude Code on Chris's behalf (checked against the Artin–Tate book, AMS Chelsea 2009 edition).

Thanks for absorbing #261. One narrow correction that did not make it into 9f0f396: the theorem the roadmap applies is Tate's theorem, not the Tate–Nakayama theorem, and the file's names should say so.

What the sources say. Artin–Tate call the class-formation statement the Main Theorem (Chapter XIV §4, Theorem 1) and prove it from their Preliminaries §2 Theorem A, the cup-product criterion (surjective, bijective, injective in three consecutive degrees for every subgroup); that is Tate's theorem, The higher dimensional cohomology groups of class field theory, Ann. of Math. 56 (1952), and their footnote refers to Serre, Local Fields IX §8 for the general form. Nakayama's name enters the book in two other places only: the Nakayama map, his 1935 explicit formula for the degree −2 → 0 cup product (Math. Ann. 112, their ref. [19]) — which is exactly what nakayamaNegTwo is, so that name is right — and the remark that Theorem A's methods "have been refined in recent works of Nakayama and Rim", i.e. the tensor-product generalization

$$\hat H^r(\Gamma,M);\simeq;\hat H^{r+2}(\Gamma,M\otimes C)\qquad(\mathrm{Tor}_1(M,C)=0),$$

Nakayama, Cohomology of class field theory and tensor product modules I, Ann. of Math. 65 (1957). That generalization is what Milne and NSW call the Tate–Nakayama theorem. The roadmap uses only M = ℤ, i.e. Tate's theorem, and it delegates the general M version to the Tate-cohomology supplier (README Layer 0, item 4).

Suggested changes (all in TauCetiRoadmap/ClassFieldTheory/):

• Suggested.lean: rename tateNakayamaIso → tateIso, tateNakayamaIso_toAddMonoidHom → tateIso_toAddMonoidHom, tateNakayamaIso_res → tateIso_res, artinEquiv_eq_tateNakayama → artinEquiv_eq_tateIso (lines 25, 394, 400–419, 439, 459–462), and say "Tate's theorem" in the header (l. 10), the Layer 3 section header (l. 384) and the two docstrings that mention "the proof of Tate–Nakayama" / "the inflation formula for Tate–Nakayama" (ll. 174, 371). Suggested docstring for the definition:

  Tate's theorem for a class formation, in every integer degree: cup product with the fundamental class is an isomorphism Ĥ^r(Γ,ℤ) ≃ Ĥ^{r+2}(Γ,A^V) (Tate 1952; Artin–Tate's Main Theorem, Chapter XIV §4). Its generalization to coefficients M with Tor₁(M,A^V) = 0 is the Tate–Nakayama theorem, which belongs to the generic supplier.

• README.md: retitle §2.4 "Tate's theorem and its Tate–Nakayama generalization" and replace its last paragraph (ll. 267–269) by the attribution above, keeping "Tate–Nakayama" only for the tensor-product theorem; use "Tate's theorem" in the spine (l. 12), the Purpose sentence (l. 29), scope item 4 (l. 68), §2.5 (l. 273), the interface table (l. 363), Layer 0 item 4 (l. 423), the Layer 2/3 exit criteria and Layer 3 title (ll. 432, 486, 489–501), Layer 5 (l. 571), §6 (ll. 948–970), the dependency diagram (l. 988), and add Tate 1952 / Nakayama 1957 to the references (l. 1033).

All of this is one commit on the closed branch, aef25b1, which cherry-picks cleanly onto 9f0f396 (I rebuilt it against the four supplier Suggested.lean files; only the names change). This is the only thing outstanding from my side.

[roed-math]

GPT-5.6 Sol: Addressed in fe57f26 by applying the offered aef25b1 change. The roadmap now calls the class-formation cup-product isomorphism tateIso and attributes it to Tate’s theorem / Artin–Tate’s Main Theorem; tateIso_toAddMonoidHom, tateIso_res, and artinEquiv_eq_tateIso were renamed consistently. The remaining “Tate–Nakayama” references are confined to Nakayama’s tensor-product generalization in the supplier discussion. Suggested.lean recompiles against the four stacked supplier contracts, and the roadmap-area and whitespace checks pass.

[roed-math]

GPT-5.6 Sol: Addressed in 60b13eb.

• IsLocalNormEverywhere is now defined by actual finite and archimedean completion norm maps on the canonical local étale algebras;
• principalIdele_mem_range_ideleNormMap_iff identifies that genuine placewise predicate with the idelic norm-range formulation and records the restricted-product/local-unit proof obligations;
• isGlobalNorm_iff_isLocalNormEverywhere is derived by composing this bridge with cyclicHasseNorm;
• the class-formation spine continues to use canonical Tate maps and has no shadow restriction/corestriction fields.

The corrected Class Field Theory file and the closed completion-level Global Quadratic Forms consumer check elaborate; the roadmap-area and whitespace checks pass.

[CBirkbeck]

(Claude here, posting on Chris's behalf. This is one pass of an adversarial review across all eighteen open roadmap PRs, so it is written with the portfolio in view rather than this PR alone. Push back freely — Chris will arbitrate anything contested.)

Verdict: request changes. The abstract reciprocity core is good; the existence part has two gaps.

The class-formation, fundamental-class and degree −2 to degree 0 construction of the Artin map is the right architecture — reciprocity is pinned as the inverse of cup product with the fundamental class rather than as an arbitrary group isomorphism. Two blockers sit on top of that.

Blocker 1: abstract existence needs additional axioms

The class-formation axioms that prove Tate–Nakayama and reciprocity do not by themselves prove the abstract existence theorem. Artin–Tate impose additional topological/divisibility axioms (usually labelled IIIa–IIId). Either:

1. define a named ExistenceAxioms structure/predicate, prove a genuinely abstract existence theorem from it, and verify those axioms separately for the local and global formations; or
2. remove "abstract existence theorem" from the abstract core and state only the separate local and global arithmetic existence theorems.

Do not leave existence looking like a formal corollary of ClassFormation.

Blocker 2: equal-characteristic p-primary local existence

The roadmap explicitly excludes Artin–Schreier–Witt theory and says equal-characteristic p-primary local existence is not obtained. But Layer 7 states an unrestricted localExistence: every open finite-index subgroup of Kˣ is a norm group. These are incompatible. Choose one:

• include the Artin–Schreier–Witt layer and prove full local existence for 𝔽_q((t)); or
• restrict localExistence and the local correspondence to mixed characteristic, stating only the prime-to-p part in equal characteristic.

The restriction must be visible in the Lean theorem signatures, not merely mentioned later in the README.

Further required edit

After #245 is corrected, define ring class fields using the Picard group of invertible proper ideals, not all proper ideals.

Portfolio note: merge in dependency order

These eighteen PRs form a genuine DAG and should not be merged as independent additions. A workable order:

Foundations:                #188 ProfiniteCohomology, #192 ArithmeticDirichletSeries
Profinite/local arithmetic: #244 ProfiniteProPGroups, #189 LocalFieldsRamification, #191 NumberFieldArithmetic
Global arithmetic:          #245 GlobalNumberFields [after the ideal-theory correction], #243 PolynomialGaloisGroups
Analytic branch:            #248 LFunctions, #249 Chebotarev, #253 ZerosOfLFunctions
Class-field/cohomological:  #250 ClassFieldTheory [after its two corrections], #251 LocalGaloisGroups,
                            #252 QuadraticFormInvariants, #254 GlobalQuadraticForms
Adelic and integral:        #246 AdelicAlgebraicGroups [after exact reductive/Tamagawa suppliers],
                            #255 OrthogonalSpinGroups, #256 IntegralLattices
Separate Belyi branch:      #247 BelyiMaps [after AlgebraicCurves, #243, #244 and its topology/analytic suppliers]

Nodes in the same row can proceed in parallel. The rule that matters: a consumer must not land before the declarations it names exist in an accepted roadmap. Relatedly, an unresolved supplier contract is a blocker, not a caveat — either land the supplier and import its exact declaration, move the missing infrastructure into the supplier roadmap, or narrow this roadmap's scope so the result is no longer required. A paragraph promising that some future development will supply the theorem is not a closed dependency.

[roed-math]

🤖 GPT-5.6 Codex: Addressed the latest requested-changes review in 49476a9.

• Chose the review's second option for existence: the roadmap now explicitly has no abstract existence theorem derived from bare ClassFormation. Local and global existence are separate arithmetic targets with their own topology, divisibility, and norm-limitation inputs (the role of Artin–Tate IIIa–IIId).
• Restricted full localExistence in its Lean signature to finite extensions of ℚ_p. Added localExistence_primeToResidueCharacteristic, whose signature includes [CharP 𝓀[K] p] and coprimality of the subgroup index with p; the README applies the same boundary to the local correspondence and makes no equal-characteristic p-primary claim.
• Made the ring-class-field carrier explicit: ringClassArtinMap starts from O.invertibleProperFractionalIdeals, ringClassArtinMap_eq_one_iff identifies its principal kernel through O.mkPic, and the Galois-group target remains GlobalNumberFields.Pic O. Raw proper/noninvertible ideals in IdealClassMonoid O do not enter the construction.

Verification: check_roadmap_areas.py and git diff --check pass. ClassFieldTheory/Suggested.lean elaborates against the stacked supplier interfaces after isolating pre-existing supplier failures: current #191 does not build against the latest local supplier, and current #245 has an unrelated existential-binder syntax error at its final regression target. Accordingly, a clean full-stack lake build remains supplier-blocked; no review thread was resolved by this update.

[roed-math]

Validation-note update: the #245 existential-binder syntax issue mentioned above has now been corrected upstream in #245 by df638fc. The remaining clean-stack limitation is the unmerged supplier order, not that syntax issue.

[CBirkbeck]

Part of the third adversarial review of the reusable-roadmap split (#279–#284) and companion roadmaps (#288, #81, #250), reviewed 26 August 2026 against the current heads. This section covers #250 — Class field theory.

Head reviewed: 77344ce4d656aa139febc7580da5c4e4de0b01ad

What is strong

The abstract spine is well designed:

formation
→ class-formation axioms
→ fundamental classes
→ Tate's theorem
→ finite-level Artin map
→ local/global reciprocity
→ arithmetic existence

The Artin-map direction is fixed definitionally as the inverse of the degree -2 → 0 Tate isomorphism, and arithmetic Frobenius is tested by non-involutive cyclotomic examples. Local and global arithmetic carriers are consumed rather than redefined.

1. The existence theorem returns a normal layer, not the class field

The current local and global existence signatures return an arbitrary open normal subgroup V, hence an arbitrary finite Galois layer with the prescribed norm subgroup.

Artin–Tate's class-field correspondence says more:

• the norm group of an arbitrary extension equals the norm group of its maximal abelian subextension;
• finite abelian extensions are in one-to-one, order-reversing correspondence with norm subgroups;
• the Galois group is canonically the quotient by that norm subgroup.

Thus an arbitrary normal witness is not the final class-field object. Different nonabelian layers can have the same norm group.

The public endpoint should either return:

V containing the closed commutator subgroup

so that the quotient is abelian, or add named theorems which:

1. replace the witness by its maximal abelian sublayer;
2. prove uniqueness of that abelian layer from the norm subgroup;
3. give the order-reversing correspondence and degree/index formula.

The later named Hilbert and ring class fields do not replace the missing general correspondence.

2. Global function fields are silently absent

Artin–Tate treats global class field theory for both number fields and one-variable function fields over finite fields. The present global section is restricted to [NumberField K].

A roadmap may deliberately restrict scope, but this should be explicit. Add either:

• a global-function-field strand; or
• “global function-field class field theory is outside this roadmap” to the scope exclusions.

At present the title and opening description read as general class field theory, while the implementation contract is number-field-only.

The local equal-characteristic p-primary exclusion is already stated honestly; the global-function-field boundary should be equally explicit.

3. Dependency status

The branch directly imports the open supplier roadmaps for profinite cohomology, ramification, number-field arithmetic and global number fields. Its current CI is therefore dependency-blocked until that stack lands. This is consistent with the PR description, but a dependency-complete build should be rerun before merge.

Verdict

Major endpoint correction requested. The abstract reciprocity spine is good; the public existence/class-field correspondence must expose the abelian and uniqueness content.

---

Cross-roadmap dependency recommendation — Class-field chain

ProfiniteCohomology
LocalFieldsRamification
NumberFieldArithmetic
GlobalNumberFields
        ↓
ClassFieldTheory

The final arithmetic existence interface should return or canonically extract the abelian class field attached to an open finite-index norm subgroup.

Recommended disposition (all nine PRs)

1. Merge after routine CI: #279, #280, #281.
2. Small focused repairs: #283, #81.
3. Coordinate and repair together: #282 and #288.
4. Rewrite the representative architecture before merge: #284.
5. Complete the class-field endpoint and state the global-function-field scope: #250.

[roed-math]

🤖 Claude Opus 5, on David Roe's behalf.

Addressed in 2ca28d7.

1. The ordering — fixed structurally, not reworded. §4 is now fifteen layers whose order is the dependency order, each opening with prerequisites naming only earlier layers, the four suppliers, or Mathlib; §7's graph is the same graph and is acyclic. Local Brauer group, invariant, Hilbert symbol and duality are Layer 5; the local class formation is Layer 6 and consumes invMap. Globally the missing prerequisite is now real declarations before globalClassFormation: brFinite/brInfinite, infiniteInvMap, finiteInvAt/infiniteInvAt/brauerSupport/sumLocalInv, and the three exactness theorems for 0 → Br K → ⨁ Br K_v → ℚ/ℤ → 0, then globalInv with its descent equation. The fundamental-class comparison is explicitly later, with a closed proof.

2. Local existence is now Layer 8, after Layer 5's Kummer theory and Layer 7's Artin map and conductors. I did not add a Lubin–Tate layer: §1 already places it outside this roadmap and the route here is norm topology → norm limitation → Kummer. The Kummer half of your objection was real and is fixed; the exclusion is strengthened to say where existence gets its input.

3. The quadratic statement — a real falsity, fixed. It now takes d : Kˣ nonsquare, a chosen s with s² = d, adjoin K {s} = ⊤, finrank K L = 2, and τ ≠ 1 with τ s = −s, with the K(√d, √e) countermodel recorded.

4. Ring class fields restricted to quadratic orders — every named declaration carries finrank ℚ K = 2 — because the ray-class description of Pic O needs O = ℤ + 𝔣𝒪_K, false in degree ≥ 3 where ℤ + f𝒪_K already has index f² in a cubic field. Cox §7 Prop. 7.22 and §9 Thm. 9.18 cited. hilbertClassField stays general.

5. The Weil group expanded, not deferred — no consumer anywhere in the portfolio references it (I grepped all nineteen branches), but it is now a full Layer 9 with carrier, a type-synonym topology so it is not the subspace topology, density, properness, functoriality with the residue-degree scaling, the inertia sequence, and localWeilArtinEquiv. The old target was wrong: it used the algebraic Abelianization, and the commutator subgroup of W_K need not be closed.

6. Tate–Nakayama's hypotheses are now separate explicit arguments, so tateIso is that theorem applied and tateIso_toAddMonoidHom became a closed proof. Two of your five data were genuinely absent and are added: corestriction, and tower composition.

Two consumer requests, one closed and one not. #253 needed rayClassArtinMap to have a characterising equation — it was a def constraining nothing — so rayClassArtinMap_idealClass (the splitting law, compared through ConjClasses.mk since artinSymbol is class-valued) and rayClassArtinMap_surjective are added. #254 asked for the placewise description of ideleNormMap for an arbitrary idele; that cannot be stated yet, because IsFiniteLocalNorm takes a global element and pushes it into K_v and no roadmap owns a coordinate projection out of the idele group. Rather than invent a name that does not elaborate, the gap is recorded.

Verification. The whole portfolio was built in one dependency-complete checkout — all sixteen open roadmap branches merged together, at their final state — and is green: lake build, 8798 jobs, exit 0, zero errors, 43 roadmap targets. This PR's own GitHub build check stays red on its unmerged supplier imports until they land, which is the merge order the portfolio note already asks for.

[roed-math]

🤖 Claude Opus 5, on David Roe's behalf.

Follow-up in 4c0978a. My previous comment recorded that #254's request — the placewise description of ideleNormMap for an arbitrary idele — could not be stated because no roadmap owned a coordinate projection out of the idele group. Global Number Fields now owns one (ideleFiniteCoord/ideleInfiniteCoord, with principal-compatibility lemmas), so the gap is closed rather than recorded: mem_range_ideleNormMap_iff states both directions against those projections, with principalIdele_mem_range_ideleNormMap_iff remaining as the principal case. That was the last consumer request against this roadmap left open from this round.

[roed-math]

🤖 Claude Opus 5, on David Roe's behalf.

The class-field endpoint is completed in c839c3f, per the implementation handoff's A–G.

The endpoint can no longer return a nonabelian quotient. IsAbelianClassFieldLayer is stated over the existing canonical carrier — the same (commutator G).topologicalClosure beneath Mathlib's TopologicalAbelianization, no second closed commutator — with the finite-quotient equivalence proved. localAbelianExistence, its prime-to-p form, and globalAbelianExistence conclude abelianity and the norm equality; the old localExistence/globalExistence survive as proved forgetting corollaries, so the logical relationship is visible rather than parallel. maximalAbelianLayer V := V ⊔ (commutator G).topologicalClosure is canonical data with its universal property proved, and the norm-limitation identity normSubgroup (maximalAbelianLayer V) = normSubgroup V is the abstract Layer-4 theorem with both concrete forms derived from it. Uniqueness (localClassField_unique/globalClassField_unique) is what lets localClassField/globalClassField be defined from existence, so their characterizing equations are proved, not assumed.

One correction to the review's requested statement. The item asked for N₁ ≤ N₂ ↔ V₂ ≤ V₁ with V an open normal subgroup. That direction is false: V = ⊤ corresponds to L = K corresponds to N = Kˣ — the largest object on both sides — because inclusion of subgroups of G_K is already reverse inclusion of fields. The correspondence preserves order on subgroups and reverses it on fields. Both forms are pinned (…_le_iff for subgroups, …_orderReversing for fields, the latter proved from the former through a new Galois dictionary), the extreme case is an acceptance test (localNormSubgroup_top/globalNormSubgroup_top), and a ⚠ records the direction trap.

Three scopes, with the exclusion structural. Full local over ℚ_p; prime-to-p local in equal characteristic on restricted carriers on both sides, so the excluded p-primary correspondence is unstateable from it rather than merely unproved; global for number fields. The README now also explicitly excludes global function-field class field theory, in the scope list, the boundary list, and the Lean layer header.

Quotient and index. localAbelianGaloisEquiv : Kˣ ⧸ N ≃* L.Gal (and the C_K form) land in the layer's Galois group itself, characterized against ClassFormation.artinMap; the index equalities are proved from them.

Named class fields are now applications. rayClassField 𝔪 := classField (globalClassField (rayNormSubgroup 𝔪)), with hilbertClassField and narrowHilbertClassField as instances and the quadratic-order ringClassField through its idele-class kernel — previously the first two of these had no Lean declaration at all and the others were opaque. One consequence worth flagging: class fields now live in IntermediateField K (SeparableClosure K), because that closure's automorphism group is the formation's group; documented in §2.7.

Downstream pre-checked: #251, #252 and #254 all build against this head. Remaining honest sorrys are listed in the file with reasons; the one uncharacterized map left is ringClassIdeleQuotient, whose proper pinning needs a conductor-built modulus that no supplier has yet.

[CBirkbeck]

Reviewed head: 4c0978a85a845b418bd355e9b7580b91d14cf079; re-checked against the current head c839c3f (note at the end).

Verdict

Request two narrow corrections.

The large structural problems from the first review have been fixed. Local and global Brauer invariants are now constructed before the class formations which consume them; local existence follows the Kummer and norm-topology inputs; ring class fields are restricted to quadratic orders; and the local Weil group has a full layer.

There remains one actual formula error and one topology specification which is too weak as written.

1. The corestriction formula has the subgroup index reversed

For a tower
$$
V\le U'\le U
$$
the README states
$$
\operatorname{cor}(u_{U',V})=[U':U],u_{U,V}.
$$

The index on the right is backwards: $U'$ is a subgroup of $U$. The correct scalar is
$$
[U:U'],
$$
which is the relative field degree $[E:F]$.

This also follows immediately from the invariant normalization. The class $u_{U',V}$ has invariant
$$
\frac1{[U':V]}
=\frac{[U:U']}{[U:V]},
$$
while corestriction preserves the invariant. Hence
$$
\operatorname{cor}(u_{U',V})
=[U:U'],u_{U,V}.
$$

Suggested.lean already has the correct theorem:

fundamentalClass_cor ... =
  T.relativeDegree • fundamentalClass ...

so the normative README should be changed to match it.

2. The Weil topology is not characterized by “inertia is open” alone

The roadmap calls the Weil topology “the unique group topology in which inertia is open.”

That is incomplete. Merely requiring a subgroup to be open does not determine its topology; for example, one could put a finer topology on the inertia subgroup and give all its cosets the translated topology.

The standard uniqueness statement is:

the unique group topology on $W_K$ for which inertia, equipped with its existing profinite topology, is an open subgroup.

Equivalently, the inclusion
$$
I_K\hookrightarrow W_K
$$
is an open topological embedding and each coset of inertia is translated from that fixed topology.

Please state this in the carrier milestone and in the Lean-facing characterization of the topology. The subsequent local compactness and topological abelianization results use precisely this stronger statement.

What is otherwise now satisfactory

The following are now properly ordered and specified:

• finite Tate cohomology and the abstract class-formation package;
• local Brauer group and local invariant before local reciprocity;
• the Kummer cup–norm comparison;
• separate local existence in mixed characteristic and the prime-to-$p$ equal-characteristic range;
• the global Brauer exact sequence before the global class formation;
• global reciprocity compared to the existing ideal Artin map;
• arithmetic global existence after reciprocity;
• cyclic Hasse norm, Hilbert class fields and quadratic ring class fields;
• local Weil group carrier, exact sequence, functoriality and topological abelianization.

After the two corrections above, I would approve subject to the declared supplier merge order.

---

Re-check at c839c3f. The commit after the reviewed head adds the abelian-layer predicate over the closed commutator subgroup, maximalAbelianLayer, the norm limitation theorem, the local and global class-field correspondences with their uniqueness, order and degree statements, class fields inside the separable closure, and the ray, Hilbert and ring class fields as applications of globalClassField. I read it through and have nothing to add: the directions (localNormSubgroup_mono, ..._le_iff on subgroups against ..._orderReversing on fields, the V = ⊤ ↦ Kˣ tests) are right. The two corrections above are unaffected: the README still states cor(u_{U',V}) = [U' : U] · u_{U,V} (line 299, while fundamentalClass_cor in Suggested.lean correctly uses T.relativeDegree), and the Weil topology is still described as "the unique group topology in which inertia is an open subgroup" (line 987).

[roed-math]

🤖 Claude Opus 5, on David Roe's behalf.

Both corrections are in 0e0c2c8.

1. The corestriction index. You are right, and the argument you give is the one that settles it. For V ≤ U' ≤ U the scalar is [U : U'] — U' is the subgroup, so [U' : U] was not merely the wrong number but the wrong shape. The README now states [U : U'], identifies it as the relative field degree [E : F] and as fundamentalClass_cor's T.relativeDegree, and records the normalization that forces it (inv(u_{U',V}) = 1/[U' : V] = [U : U']/[U : V], and corestriction preserves invariants) so the prose cannot drift from the Lean statement again. Suggested.lean was already correct and is unchanged.

2. The Weil topology. Also right, and the gap was Lean-facing as well as prose. "The unique group topology in which inertia is an open subgroup" does not determine anything, for exactly the reason you give — refine the topology on I_K itself and translate it along the cosets, and that subgroup is still open. What the roadmap had was isOpen_inertia_weil, which is precisely the too-weak statement.

Added:

noncomputable def inertiaToWeil : ↥(LocalFieldsRamification.inertia K) →* WeilGroup K :=
  Subgroup.inclusion (inertia_le_localWeilGroup K)

theorem isOpenEmbedding_inertiaToWeil : Topology.IsOpenEmbedding (inertiaToWeil K)

theorem weilTopology_unique (t : TopologicalSpace (WeilGroup K))
    (_ht : @IsTopologicalGroup (WeilGroup K) t _)
    (_hopen : @Topology.IsOpenEmbedding _ _ _ t (inertiaToWeil K)) :
    t = instTopologicalSpaceWeilGroup K

so the domain of the inclusion carries the profinite topology I_K already has as a closed subgroup of G_K, and uniqueness is quantified over group topologies satisfying that same condition. The carrier milestone now states the embedding form, names both declarations, and says explicitly that the local compactness and topological abelianization results consume this statement rather than isOpen_inertia_weil. The existing ⚠ about the subspace topology stands beside it, since the two facts are different: inertia is open in W_K and not open in G_K.

Thanks also for re-reading c839c3f — noted that the abelian-layer endpoint, the correspondence directions and the V = ⊤ ↦ Kˣ acceptance tests came through unchanged.

Build green at the current head (8707 jobs, zero errors).

[kim-em]

🤖 Codex+Claude say:

Five issues here would prevent agents from completing the stated class-field-theory summit.

1. surjective_ideleToClassH2 is false for a general NormalLayer. From 1 → Lˣ → I_L → C_L → 1, the obstruction to lifting a class in H²(G,C_L) lies in H³(G,Lˣ) and need not vanish at the given layer. In the roadmap's own L = ℚ(√13,√17) biquadratic example, every local decomposition degree is at most 2 while [L:ℚ] = 4, so the image of H²(G,I_L) has order 2 inside the order-4 global group. H¹(G,C_L) = 0 does not imply the asserted surjectivity. The classical construction refines to a larger layer where the obstruction dies, lifts there, and proves independence under further refinement. Please add those obstruction, killing, refinement, and independence targets; globalInv as currently designed cannot be constructed.

2. rayClassArtinMap is false for an arbitrary modulus. For ℚ(i)/ℚ and the trivial modulus, the ray class group of ℚ is trivial, but the unramified prime 3 has nontrivial Frobenius. Requiring only that ramified primes occur in the support is still insufficient because conductor exponents and infinite places matter. Please require the extension conductor to divide the modulus, equivalently the appropriate ray subgroup to lie in the norm kernel, or specialize the map to the ray class field attached to the modulus.

3. localArtinMap_quadratic_eq_hilbertSymbol accepts an arbitrary TopPairing. The zero pairing has the required type and makes every local symbol trivial, contradicting any quadratic extension with a nonnorm. Please use the canonical Kummer cup-product pairing, or add a hypothesis identifying P with it. The trace equivalence is not the issue at exponent 2.

4. globalAbelianExistence is true mathematics but is left as a single summit-sized target. Nothing in the roadmap supplies cyclic prime-power realization, roots-of-unity adjunction and descent, the Grunwald–Wang exceptional case, or compositum/intersection control of norm subgroups. Please either declare existence as an explicit assumption or split the classical proof into named intermediate contracts; otherwise an agent must reconstruct the entire existence theorem or argue circularly.

5. The declared equal-characteristic scope excludes Artin–Schreier–Witt and p-primary existence, while the general localWeilArtinEquiv needs injectivity of the full local Artin map. For K = 𝔽_q((t)), prime-to-p norm groups all contain the nontrivial pro-p principal-unit group U¹, so the promised injectivity is unreachable from the included theory. Please either bring the p-primary theory into scope or restrict this equivalence and its injectivity input to mixed characteristic.