we-solve (beta)

Math-2787 · mathematics · Number theory

Milnor K reconstruction at the characteristic prime

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Fix a prime $p$. Let $K/k$ and $L/l$ be finitely generated extensions of algebraically closed fields of characteristic $p$, with $\operatorname{trdeg}(K/k),\operatorname{trdeg}(L/l)\ge2$. For $F=K,L$, set \[ V_F=F^\times/(F^\times)^p,\qquad R_F=\operatorname{span}_{\mathbb F_p}\{[a]\otimes[1-a]:a\in F\setminus\{0,1\}\}. \] The class $[a]$ uses additive notation for the multiplicative quotient. The degree-two Milnor group is $(V_F\otimes_{\mathbb F_p}V_F)/R_F=K_2^M(F)/p$. Define \[ \operatorname{Isom}_{\mathrm M}(V_K,V_L) =\{\Theta:V_K\xrightarrow{\sim}V_L\text{ linear over }\mathbb F_p: (\Theta\otimes\Theta)(R_K)=R_L\}. \] The maps are required to be invertible, and to carry the relation space onto the target relation space. Let $\operatorname{Isom}(K,k;L,l)$ consist of field isomorphisms carrying $k$ onto $l$. Is the natural map \[ \operatorname{Isom}(K,k;L,l)\longrightarrow \operatorname{Isom}_{\mathrm M}(V_K,V_L)/\mathbb F_p^\times, \qquad\alpha\longmapsto[\alpha_*], \] a bijection, where $\alpha_*([a])=[\alpha(a)]$ and the quotient identifies linear isomorphisms differing by one nonzero scalar?

Short English statement

Do the first two Milnor groups modulo the characteristic recover these function fields and their constant-preserving isomorphisms, after identifying compatible linear isomorphisms that differ by a common nonzero scalar?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2787

The source requires invertible $\mathbb F_p$-linear maps and equality $(\Theta\otimes\Theta)(R_K)=R_L$, rather than arbitrary maps preserving only some relations. With those conventions, its theorem gives the entire reconstruction bijection in this question for relative transcendence degree at least two. The field maps carry the named constant field onto the target constant field; the common nonzero scalar quotient appears on the Milnor side.

Milnor K reconstruction at the characteristic prime

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 009; 2026-10-05), the asserted result is that Milnor $K$-theory modulo the characteristic recovers such function fields from degree-two Steinberg relations, up to one nonzero scalar.

Mathematical statement of the claimed result

Manuscript 1.
Fix characteristic $p>0$. For any field $F$ of that characteristic put \[ V_F=F^{\times}/(F^{\times})^p,\qquad R_F=\operatorname{span}_{\mathbb F_p}\{[f]\otimes[1-f]:f\ne0,1\}. \] A linear isomorphism $\Theta:V_K\to V_L$ is compatible if $(\Theta\otimes\Theta)R_K=R_L$, equivalently preserving degree-two Milnor products. For finitely generated $K/k,L/l$ with algebraically closed constants of characteristic $p$ and both relative transcendence degrees at least two, the asserted reconstruction bijection is \[ \operatorname{Isom}(K,k;L,l)\xrightarrow{\sim} \operatorname{Isom}_{\rm M}(V_K,V_L)/\mathbb F_p^{\times}. \] On the left, field isomorphisms carry $k$ onto $l$; on the right compatible maps are identified under nonzero scalar multiplication. Only the first two Milnor groups modulo the characteristic are used.

Outline of the argument

For manuscript 1 (family 009; 2026-10-05), vanishing symbols are interpreted through derivations over the subfield of $p$th powers. An intersection calculation recovers projective lines; one common power correction aligns these lines, and projective incidence gives the field operations.

Formal verification

No Lean formalization is listed at this snapshot for manuscript 1 (family 009; 2026-10-05).

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →