we-solve (beta)

Math-2796 · mathematics · Number theory

Bogomolov-Pop pro-ell reconstruction

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Let K/k and L/l have transcendence degree at least two over arbitrary algebraically closed constants of characteristic different from ell. Does the maximal abelian pro-ell Galois quotient, equipped with its commutator-lifting structure from the abelian-by-central quotient, determine every isomorphism of their perfect closures, with the canonical bijection using Frobenius equivalence on fields and a common $Z_\ell -unit$ scalar on Galois maps?

Short English statement

Let K/k and L/l have transcendence degree at least two over arbitrary algebraically closed constants of characteristic different from ell. Does the maximal abelian pro-ell Galois quotient, equipped with its commutator-lifting structure from the abelian-by-central quotient, determine every isomorphism of their perfect closures, with the canonical bijection using Frobenius equivalence on fields and a common $Z_\ell -unit$ scalar on Galois maps?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2796

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 009; 2026-09-23).

Bogomolov-Pop pro-ell reconstruction

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-09-23), the asserted result is that for function fields of dimension at least two with algebraically closed constant fields, if $\ell$ is unequal to the characteristic, its pro-$\ell$ abelian-by-central quotient determines both the constant field and the function field's perfect closure.

Mathematical statement of the claimed result

Manuscript 1.
For a fixed prime $\ell$ and fields of characteristic different from $\ell$, let $G_F^{(\ell)}$ be the maximal pro-$\ell$ absolute Galois quotient, $\Pi_F^a=G_F^{(\ell)}/[G_F^{(\ell)},G_F^{(\ell)}]$ and $\Pi_F^c=G_F^{(\ell)}/[[G_F^{(\ell)},G_F^{(\ell)}],G_F^{(\ell)}]$, using closed commutator subgroups. A continuous $\mathbb Z_{\ell}$-linear isomorphism of abelian quotients is compatible when it carries the induced alternating commutator pairing to the other pairing through an isomorphism of central kernels. For function fields $K/k,L/l$ over algebraically closed constants with transcendence degrees at least two, the claimed bijection is \[ \operatorname{Isom}_{\rm F}^{i}(K,L)\xrightarrow{\sim} \operatorname{Isom}^{c}(\Pi_L^a,\Pi_K^a)/\mathbb Z_{\ell}^{\times}. \] The left uses perfect-closure field isomorphisms carrying constants onto constants, modulo integral Frobenius powers in positive characteristic; the right identifies compatible maps up to unit scaling. This includes transcendence degree two and $\ell=2$.

Outline of the argument

For manuscript 1 (family 009; 2026-09-23), commutator relations detect valuations through alternating characters. Kummer tests and uniformly bounded pencils identify curve subfields and rational quotients, from which incidence reconstruction yields the field with exactly the scalar and Frobenius ambiguities.

Formal verification

For manuscript 1 (family 009; 2026-09-23), the documented Lean scope is uniqueness of perfect-closure field maps modulo Frobenius once the induced Galois correspondence agrees up to an $\ell$-adic unit; existence for every admissible correspondence is not included.

The selected formal statement has narrower scope than the full manuscript claim.

The linked family Comparator checks are BogomolovPopInjectivity.lean.

Their named declarations include OAI.BogomolovPop.main_graph_injective.

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 →