we-solve (beta)

Math-2327 · mathematics · Algebraic geometry

Affine Fibrations as Affine-Space Bundles

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
Let $f:X\to Y$ be an affine, faithfully flat $\mathbb{A}^n$-fibration whose closed fibers are geometrically integral. Must $f$ be an $\mathbb{A}^n$-bundle?

Formulation references: [S1], [S2].

Short English statement

Let $f:X\to Y$ be an affine, faithfully flat $\mathbb{A}^n$-fibration whose closed fibers are geometrically integral. Must $f$ be an $\mathbb{A}^n$-bundle?

Sources

Catalogue entry

Statement licence: CC-BY-SA-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2327

The affine-fibration corollary gives morphisms onto complex affine line and plane whose every geometric fiber is affine three-space, while neither morphism is locally a product in the Zariski topology. Both morphisms are affine, smooth and surjective, so they are faithfully flat and have geometrically integral closed fibers. They therefore supply counterexamples within the exact class specified in this question.

Affine Fibrations as Affine-Space Bundles

OpenAI's claim

An explicit complex affine fourfold is claimed to become affine five-space after one stabilization while itself failing to be affine four-space, with stable-coordinate and nontrivial affine-fibration consequences. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.
In $P=\mathbb C[p,s,u,F,J]$, define \[ x=s^2+u^3+p^2F,\qquad H=x^2F-(1+2sx)J-p^2J^2-pu,\qquad A=P/(H). \] OpenAI claims that $A$ is integral of dimension four and for an independent variable $w$, \[ A[w]\simeq\mathbb C^{[5]},\qquad A\not\simeq\mathbb C^{[4]}. \] The notation $\mathbb C^{[j]}$ denotes a polynomial algebra in $j$ variables. It also claims that $H$ is a coordinate of $P[w]$ but not of $P$, where coordinate means an element belonging to a polynomial coordinate system. These assertions give one-variable cancellation and stable-coordinate counterexamples in the indicated dimensions. Writing $X=\operatorname{Spec}A$, the affine-fibration corollary claims that \[ \pi:X\to\mathbb A^1,\quad x\mapsto p(x),\qquad \rho:\mathbb A^5\to\mathbb A^2,\quad z\mapsto(p(z),H(z)) \] are smooth and surjective with relative dimension three; every fiber over a base point $y$ is $\mathbb A^3_{\kappa(y)}$, yet neither map is locally a product with $\mathbb A^3$ in the Zariski topology. Thus the examples satisfy faithful flatness and geometric integrality of the fibers.

Outline of the argument

Manuscript 1 (family 047, 2026-09-23): A locally nilpotent derivation and an explicit inverse polynomial change give the cylinder isomorphism. To obstruct cancellation, a valuation along the exceptional parameter computes the associated graded affine modification; the resulting rigidity distinguishes the original coordinate ring from a polynomial algebra.

Formal verification

For family 047, the scope page documents the following selections. The selected construction is a four-dimensional complex domain whose one-variable polynomial extension is a five-variable polynomial ring, while the original ring is not polynomial. The other affine-fibration and stable-coordinate consequences are separate. The documented statement covers the main claim of manuscript 1. Comparator files: ComplexCancellation.lean. Declarations: OAI.ComplexCancellation.main.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

Go to contribution →