Add roadmap: Global number fields, ray classes, adeles, and Hecke characters

[roed-math]

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

Summary

This roadmap develops reusable global arithmetic carried by a number field before reciprocity or L-function analysis: places and completions, mixed weak approximation, moduli and ray/narrow class groups, uniform ray-class counting, adeles and ideles, idele class groups and norm-one compactness, base change and norms, ray-class and Hecke characters, infinity types, cyclotomic arithmetic, and orders with wide and narrow Picard groups.

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

Ownership

It consumes idealsAway, the finite-completion dictionary, and related canonical arithmetic carriers from #191. It owns moduli, ray classes, field adeles/ideles, Hecke-character carriers, infinity types, orders, Pic, and NarrowPic. The order API now exports the canonical narrowToPic map, its value on classes, surjectivity, sign/unit kernel description, naturality, and maximal-order specialization.

It does not own reciprocity or class fields, L-function analysis, Chebotarev, adelic points of algebraic groups, Tamagawa measures, or global quadratic-form classification. It exports exact contracts to those downstream roadmaps.

Port history

This is a clean port of roed-math/TauCetiRoadmap#16, rebased onto upstream main. The arithmetic-carrier portions were extracted from the former Global Class Field Theory roadmap while Artin reciprocity and class fields remained with Class Field Theory. idealsPrimeTo is tied to #191's idealsAway, not duplicated. The non-normative PROVENANCE.md is omitted from this upstream port; the detailed migration ledger remains private.

Human review priorities

• the Add roadmap: Number fields and arithmetic invariants #191 completion and prime-to-set ideal contracts;
• topology and normalization of adeles, ideles, and idele class groups;
• modulus transitions, ray-class counting, and Hecke-character carriers;
• the canonical wide/narrow Picard comparison, its sign/unit kernel, naturality, and maximal-order specialization;
• the boundary between orders/Picard groups here and ring class fields downstream.

Validation

• lake -Kjobs=1 build TauCetiRoadmap.GlobalNumberFields.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]

(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. There is a genuine false statement in Layer 11.

The roadmap asks to define NumberFieldOrder.properIdeals, prove that proper ideals are equivalent to invertible ideals, and then build Pic O and NarrowPic O from those proper ideals. That equivalence is false for a general order in a number field. It holds for quadratic orders — and more generally for Gorenstein orders — but not for arbitrary orders.

For a nonmaximal order one must distinguish:

• the group of invertible ideal classes, which is the Picard group;
• classes of noninvertible ideals, which form an ideal class monoid and do not form a group at all.

Required edits

1. Replace properIdeals as the Picard carrier with the group of invertible proper fractional ideals.
2. Define Pic O from invertible proper fractional ideals modulo principal ideals.
3. Define NarrowPic O on the same invertible carrier, with positive principal ideals.
4. Restrict "proper iff invertible" to quadratic orders, Gorenstein orders, or another explicit hypothesis under which it is actually true.
5. If noninvertible proper ideals are wanted, introduce a separate ideal class monoid — do not force them into a group.
6. Audit extension/contraction, the conductor-prime correspondence, finiteness and the maximal-order comparison, so that every group-valued statement carries invertibility or prime-to-conductor hypotheses.
7. Add a regression example from a non-Gorenstein order containing a proper noninvertible ideal.
8. Correct the Cox citation: the equivalence in Cox is about quadratic orders, not arbitrary number-field orders.

Downstream consequences

The same correction has to propagate to #250 (the ring class field and Gal(H_O/K) ≃ Pic O) and #256 (the binary quadratic-form / order correspondence). Both are flagged on their own threads.

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]

Addressed the requested general-order correction in 1035a24.

Changes made:

• Pic O and NarrowPic O now explicitly use the group of invertible proper fractional ideals; raw proper ideals are no longer treated as a group.
• Properness is represented separately by NumberFieldOrder.IsProperFractionalIdeal. The only proper/invertible equivalences now carry an explicit Gorenstein hypothesis or the quadratic finrank = 2 specialization.
• Added a separate IdealClassMonoid O for homothety classes that include noninvertible ideals, together with the contract identifying its units with Pic O.
• Extension/contraction carriers now encode both invertibility and prime-to-conductor restrictions, and the prime correspondence is explicitly restricted away from the conductor.
• Audited the finiteness and maximal-order prose so group-valued claims remain on invertible carriers; the unrestricted comparison occurs only after specializing to the maximal order.
• Added the cubic regression K = ℚ(∛2), O = ℤ + 2ℤ∛2 + 2ℤ(∛2)², A = 8ℤ + 2ℤ∛2 + 2ℤ(∛2)², where A is proper but noninvertible, and pinned that its ideal-class-monoid class is a nonunit.
• Corrected the Cox citation so it is used only for quadratic orders, and added Kopp–Lagarias for the general-order ideal theory and counterexample.

Verification:

• python3 .github/scripts/check_roadmap_areas.py — passed
• git show --check HEAD — passed
• I also attempted Lean elaboration with PR Add roadmap: Number fields and arithmetic invariants #191 temporarily layered as the required supplier. The shared v4.34 environment did not finish loading even for an import-only diagnostic, so that run was bounded and stopped. The branch's GitHub build is independently blocked until Add roadmap: Number fields and arithmetic invariants #191 supplies TauCetiRoadmap.NumberFieldArithmetic.Suggested; the previous CI failure is exactly that missing import, not a reported error in these declarations.

There were no inline review threads on this review submission, so I have not resolved or otherwise changed any thread state.

[roed-math]

Follow-up: stacked validation from #250 exposed one Lean syntax issue in the newly added cubic regression target: square-bracket instance binders are not valid inside that existential binder sequence. Commit df638fc replaces them with explicitly typed anonymous binders. The roadmap-area and diff checks pass after the correction.

The branch's standalone GitHub build remains blocked earlier by the intentionally missing #191 supplier file TauCetiRoadmap.NumberFieldArithmetic.Suggested; that is separate from this corrected declaration.

[CBirkbeck]

Verdict

Request changes.

The roadmap contains important shared arithmetic carriers, but two of the public definitions are currently totalized outside their mathematical domain, and the analytic character layer needs a sharper boundary.

1. idealClass should not accept an arbitrary integral ideal

The proposed API has

idealClass (𝔪 : Modulus K) (I : Ideal (𝓞 K)) : RayClassGroup 𝔪

although the ray class of an integral ideal is defined only when I is nonzero and coprime to the finite modulus. Later theorems add 𝔪.IsCoprimeTo I, but the definition itself has already exported an arbitrary junk class for every bad ideal.

This is precisely the sort of totalization which later makes a false theorem typecheck.

Use a subtype:

def IntegralIdealPrimeTo (𝔪 : Modulus K) :=
  {I : Ideal (𝓞 K) // 𝔪.IsCoprimeTo I}

idealClass (I : IntegralIdealPrimeTo 𝔪) : RayClassGroup 𝔪

or take the proof as an explicit argument. Then multiplication and the class-map compatibility are definitionally on the correct domain.

2. The ray-class triviality criterion should use the actual principal generator condition

The current representative theorem expresses triviality through two integral elements a,b and an identity

I * (b) = (a).

This can be a useful denominator-clearing lemma, but it should be derived from the intrinsic statement:

[
[I]=1 \iff I=(x)
\quad\text{for some }x\in K^\times
\text{ with }x\equiv1\bmod\mathfrak m_0
\text{ and }x>0\text{ at }\mathfrak m_\infty.
]

Make the fractional-principal formulation primary and prove the integral a,b version separately. Otherwise downstream proofs are tied to one denominator-clearing presentation.

3. Clarify which Hecke characters the infinity-type carrier describes

A continuous idele-class character at infinity is not determined in general by a list of integer exponents. At a real place one also has a continuous real parameter through |x|^{it}; at a complex place there are modulus and angular parameters.

If the roadmap's InfinityType is intended only for algebraic Hecke characters, say so in the type and in every theorem:

AlgebraicInfinityType

If it is intended for arbitrary continuous Hecke characters, the carrier is incomplete and must include the continuous spectral parameters. The finite-order characters consumed by the L-functions roadmap are a third, simpler subcase and should be identified explicitly.

4. The ray-class counting theorem hides a major geometry-of-numbers argument

The claimed uniform power saving

[
A_c(x)=C_\mathfrak m x+O(x^{1-\delta})
]

for every ray class is much stronger than finiteness of the ray class group. Its proof needs an exact lattice-counting/fundamental-domain argument involving:

• ideal lattices under the Minkowski embedding;
• the unit action and a fundamental domain for logarithmic units;
• boundary estimates;
• congruence and sign conditions;
• uniformity over the finite ray class group.

These should be milestones, not one theorem with “geometry of numbers” as a prerequisite. This theorem is the arithmetic input to Chebotarev and deserves a complete route.

The main term should also be stated explicitly, including the Euler factors at primes dividing the finite modulus.

5. Pin the adelic tensor-product theorem topologically

The comparison

[
\mathbb A_L \cong L\otimes_K\mathbb A_K
]

is not merely an algebra equivalence. The roadmap should state:

• the completed/topological tensor product or the finite-dimensional algebraic tensor product with the induced topology;
• continuity and openness of the equivalence;
• compatibility with finite and infinite components;
• naturality in towers.

Without these, the displayed equivalence is too weak for later topological idele arguments.

6. Order functoriality should be restricted

Any maps on Pic or NarrowPic induced by a homomorphism of orders require more than an arbitrary algebra homomorphism. One needs a compatible embedding of fraction fields and, for narrow classes, control of real places and positivity. If such functorial maps remain in scope, their hypotheses should be stated exactly.

What is good

The single ownership of idealsAway, the modulus carrier, the distinction between Pic and NarrowPic, the proper/noninvertible ideal regression example, and the separation between ray class characters and idelic Hecke characters are all valuable.

Recommendation

I would request:

1. make ray classes proof-correct by construction;
2. make the intrinsic principal-ray criterion primary;
3. split algebraic, finite-order and general continuous infinity types;
4. expand the ray-class counting proof;
5. pin the topological adelic tensor-product statement;
6. restrict order/Pic functoriality to valid morphisms.

[roed-math]

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

Addressed in 647fb9f. All six, with one correction to the framing of item 3.

1. idealClass proof-correct by construction. Its domain is now the supplier's own NumberFieldArithmetic.integralIdealsAway, abbreviated integralIdealsPrimeTo 𝔪, with mem_integralIdealsPrimeTo as Iff.rfl — so no second monoid appears. It is a MonoidHom, which makes idealClass_mul literally map_mul _ _ _, an actual proof where there was a sorry. Your diagnosis was the right one: the junk class for every bad ideal is what later makes a false theorem typecheck.

2. Intrinsic criterion primary. idealClass_eq_one_iff is now ∃ x : Kˣ, IsCongrOne 𝔪 x ∧ ↑I = spanSingleton x; the a, b denominator-clearing form is derived, as idealClass_eq_one_iff_exists_integral.

3. Three infinity types — but not with the comparison you suggested. ContinuousInfinityType, AlgebraicInfinityType, FiniteOrderInfinityType are split as you ask. However, defining IsAlgebraic as a.toContinuous = χ.infinityType would make the odd quadratic character mod 4 non-algebraic. Weil's type A₀ compares only on the identity component, so the roadmap uses ContinuousInfinityType.EqOnIdentityComponent, with a ⚠ giving the reason and normCharacter K t as a regression witness.

4. Counting expanded into 3A–3F with named Lean targets: Lipschitz parametrizability, the count with its error term, the congruence lattice and its index, the unit congruence subgroup, the ray fundamental domain and its frontier, and the limit. The main term is explicit, including the Euler factors at primes dividing the finite modulus.

5. Adelic tensor product pinned topologically, as a ContinuousAlgEquiv under a module-topology hypothesis, with openness, the finite/infinite component compatibility, and tower naturality. All instance binders are inline rather than section variables, because a sorry-bodied def drops a Prop class absent from its type.

6. Order functoriality restricted: NumberFieldOrder.Hom now carries the fraction-field map and maps_mem, with the real-place and positivity lemmas that make mapNarrowPic well defined.

The earlier-round corrections are intact. Consumers were told: #248 needed four call-site updates and has them.

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 e16d4be, closing a gap two consumers hit after the last round: nobody owned a coordinate projection out of the idele group, so Class Field Theory could state the placewise description of its idelic norm only for a principal idele, and Global Quadratic Forms had to cite a milestone number instead of a declaration for its kernel computation on N(I_E).

Added, next to IdeleGroup: ideleFiniteCoord v : IdeleGroup K →* (K_v)ˣ and ideleInfiniteCoord w, each with the principal-compatibility lemma (ideleFiniteCoord_principal, ideleInfiniteCoord_principal) that keeps the arbitrary-idele and principal-idele statements one theory. #250 now states mem_range_ideleNormMap_iff against them, and #254 cites that declaration by name.

Also for the record, resolving my earlier open note: Modulus.support's characterization (v ∈ 𝔪.support ↔ v.asIdeal ∣ 𝔪.finitePart), which #248 asked for, remains to be pinned here — flagged, not forgotten.

[roed-math]

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

Follow-up in b9f1b76, closing the one supplier request left open from the last round: Modulus.mem_support_iff pins v ∈ 𝔪.support ↔ v.asIdeal ∣ 𝔪.finitePart as the characterizing theorem of the sorry-bodied support, with Modulus.support_one (a real proof from the characterization — the coherence check between the two pinned statements) and Modulus.support_mono against the file's existing Dvd (Modulus K) instance. The README's conventions table and analytic-interface list cite the name. #248 consumes it in the same round.

One ownership note for a later pass rather than this one: #250 now states isOpen_raySubgroup and finiteIndex_raySubgroup as properties of this roadmap's RaySubgroup; if those should live supplier-side, they are two named theorems to move.

[CBirkbeck]

Reviewed head: e16d4be06d4e0b43ef8b68937786a46665933d94; re-checked against the current head b9f1b76 (note at the end).

Verdict

Approve after its Number-Field Arithmetic dependency lands.

The current version has fixed the carrier and scope problems from the first review. I do not see a remaining mathematical error.

What I checked

The ray-class carrier is now safe. idealClass accepts a nonzero integral ideal together with its prime-to-modulus proof; it cannot be applied to the zero ideal or to an ideal meeting the finite modulus. The triviality criterion is the intrinsic fractional-generator statement, with the denominator-cleared integral version derived separately.

The ray-class counting theorem is no longer hidden under the phrase “geometry of numbers.” It has a real proof plan:

• a Lipschitz-boundary lattice-point theorem with $O(c^{n-1})$ error;
• the congruence sublattice and its index;
• the congruence-unit fundamental domain;
• assembly uniform over the finite ray class group;
• the exact main term, including the Euler factors at primes dividing the modulus;
• cancellation for nontrivial ray-class characters.

The adelic and idelic layers have the right topology:

• $K$ is dense in the finite adeles and discrete in the full adeles;
• the additive quotient is compact;
• the idele group carries the units topology;
• the norm-one idele class group, rather than the whole idele class group, is compact;
• the base-change comparison is a ContinuousAlgEquiv for the module topology, with tower compatibility.

The Hecke-character layer now has the correct archimedean carriers. It distinguishes:

• arbitrary continuous infinity types with complex parameters;
• algebraic infinity types with integral embedding exponents;
• finite-order infinity types, which have only real signs.

The type-$A_0$ condition is imposed on the identity component, so odd finite-order real characters are not incorrectly excluded.

Finally, the order theory now distinguishes invertible proper ideals from arbitrary proper ideals. Pic, NarrowPic and the ideal class monoid have different carriers; extension of ideals is attached to a homomorphism of the ambient number fields; and the real-place positivity lemma is named before the narrow map is defined.

Merge condition

The finite-place and ideal-theoretic vocabulary comes from #191. Rebase after #191 and type-check the exact imports. Subject to that stack, I would approve.

---

Re-check at b9f1b76. The one commit after the reviewed head adds Modulus.mem_support_iff (v ∈ 𝔪.support ↔ v.asIdeal ∣ 𝔪.finitePart) with support_mono and support_one derived from it — exactly the support characterization #248 now consumes. It is correct and changes nothing above.