The adele ring of a number field is not Noetherian

Proved

NoetherianScheme.not_isNoetherianRing_adeleRing

by Lucas · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrynoetherian

Let $K$ be a number field with ring of integers $\mathcal O_K$ , and let

\mathbb A_K = K_\infty \times \prod\nolimits'_{v<\infty} K_v

be its ring of adeles (the infinite adeles times the restricted product of the completions at the finite places). Then $\mathbb A_K$ is not a Noetherian ring.

Preamble

import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField

Formal statement

namespace NoetherianScheme

theorem not_isNoetherianRing_adeleRing (K : Type u) [Field K] [NumberField K] :
    ¬ IsNoetherianRing (AdeleRing (𝓞 K) K) := by sorry

end NoetherianScheme

Source

Wikipedia, "Noetherian scheme", revision 1372079294 (https://en.wikipedia.org/w/index.php?title=Noetherian_scheme&oldid=1372079294), section "Non-examples / Schemes over Adelic bases": "One of the natural rings which are non-Noetherian are the ring of adeles A_K for an algebraic number field K."

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph