The Anderson Conjecture: A Weakly Quasi-Complete Ring Need Not Be Quasi-Complete

Source: doi:10.1007/978-1-4939-0925-4_2 Authors: FrenzyMath Status: verified Main declarations: anderson_main_theorem Tags: commutative-algebra, ring-theory MSC: 13B35, 13H10

Mathematical overview

A Noetherian local ring (R, M) is quasi-complete if for every antitone sequence of ideals Aₙ and every k there is s with A s ≤ (⨅ n, A n) ⊔ Mᵏ, and weakly quasi-complete if this holds whenever ⨅ n, A n = ⊥. Anderson (2014) asked whether weak quasi-completeness implies quasi-completeness (Problem 8a of Open Problems in Commutative Ring Theory).

The answer is no. The main result, anderson_main_theorem, exhibits a weakly quasi-complete Noetherian local ring that is not quasi-complete: a two-dimensional local UFD A whose M-adic completion is the complete local domain T = ℂ[[x, y, z]]/(x² − yz), built via the Jensen–Heitmann–Loepp transfinite construction. The trivial generic formal fiber of A makes A weakly quasi-complete, while a height-one prime element a ∈ A yields a quotient A/aA that fails weak quasi-completeness, so A is not quasi-complete.

Provenance

Imported from https://github.com/frenzymath/Anderson-Conjecture; the Lean code was automatically generated by Archon. Upstream contains no sorrys outside its separate Challenge.lean statement file (which is not vendored here). Ported from Lean v4.29.0-rc8 to Lean Pool's v4.30.0-rc2.