we-solve (beta)

Math-2518 · mathematics · Algebra

Integral K5 injectivity for regular local domains

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every Noetherian regular local domain A with fraction field F, is the canonical map on integral algebraic K-groups $K_{5}(A)\to K_{5}(F)$ injective, including ramified mixed characteristic?

Short English statement

For every Noetherian regular local domain A with fraction field F, is the canonical map on integral algebraic K-groups $K_{5}(A)\to K_{5}(F)$ injective, including ramified mixed characteristic?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2518-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2518

The ring has Krull dimension two and is regular, local, and ramified in characteristic pair $(0,5)$. A nonzero integral class in degree five becomes zero in the fraction field, which already contradicts the unrestricted first Gersten injection. This is presented as a claimed negative answer.

Integral K5 injectivity for regular local domains

OpenAI's claim

OpenAI presents a counterexample in the selected manuscript. A ramified regular local ring of dimension two in characteristic pair $(0,5)$ is claimed to have a nonzero integral $K_5$ class that dies over its fraction field.

Mathematical statement of the claimed result

Result 1.
Let $V$ be the integer ring of the unramified degree-eight extension of $\mathbb Q_5$. For \[ A=(V[x,y]/(5+x^4+y^4))_{(5,x,y)}, \] the source claims $A$ is a two-dimensional Noetherian regular local domain and \[ \ker(K_5(A)\to K_5(\operatorname{Frac}A))\ne0. \] The failure is for integral Quillen $K_5$, without tensoring with the rationals.

Outline of the argument

Cyclotomic Bott classes on a quartic model are lifted integrally using a $K_4$ vanishing statement. Supported pushforward guarantees generic disappearance, while character averaging and Picard specialization on an elliptic quotient detect the surviving class modulo five.

Formal verification

Family 209 has no Lean scope page in this release. Its selected result is not presented as formalized. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

Go to contribution →