Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Line bundles over an affine-space parameter open come from the smooth factor

Statement

Assume the Axiom of Choice. Let X be a smooth geometrically integral finite-type k-scheme and V⊂Akd a nonempty open. Every invertible sheaf M on X×kV is isomorphic to the pullback of an invertible sheaf N on X. Consequently after any field extension its restrictions at all rational parameter points are isomorphic to that same base extension of N.

Facts & Assumptions

[F1]

Smooth schemes are locally factorial; invertible sheaves on integral schemes have rational sections and hence Cartier divisor representatives. On locally factorial schemes Cartier and Weil divisors, and their principal-divisor classes, agree. (Regular local rings are unique factorization domains, Rational sections of line bundles are Cartier divisors, Under AC, Cartier and Weil divisors agree on a locally factorial Noetherian integral scheme)

[F2]

Finite-variable polynomial rings over fields are UFDs, and their height-one primes are principal; codimension and transcendence-degree dimension formulas hold for finite-type affine domains. (Every finite-variable polynomial ring over a field is a UFD, with prime irreducibles and principal height-one primes, The dimension formula for affine domains)

Proof

Given: AC, X, V, and M as in the statement.

1.1F1givenconstruct

Represent M by a Cartier divisor and then by a Weil divisor on X×V using [F1]. Close each of its finitely many prime components in X×Ad with the same coefficient. The closures have codimension one because this is an open extension of varieties. The product is smooth and integral, so [F1] makes this extended Weil divisor a Cartier divisor E. Its restriction represents M.

2.1F1F2step 1.1algebra

Write K=k(X). The components of E which dominate X restrict to codimension-one primes of Spec⁡K[t1,…,td], by [F2]. This is a UFD, so choose their irreducible defining polynomials and form their product, with integer exponents given by the coefficients of E. View that product as a nonzero rational function h on X×Ad. The divisor E−div⁡(h) has no component dominating X. A remaining codimension-one component has image closure of codimension at most one in X, since its fibre dimension is at most d and [F2] gives the total dimension as dim⁡X+d−1. Its image is therefore a prime divisor T on X, and its generic fibre over T has dimension d. The affine-space fibre is integral; a closed subset of full dimension is the whole fibre. Consequently this component is precisely T×Ad. Its multiplicity as a pullback divisor is one: at the generic point the base DVR uniformizer remains a uniformizer after the purely transcendental residue-field extension.

3.1F1step 1.1step 2.1algebra∎

Thus E−div⁡(h)=pr⁡X∗D for a Weil divisor D on X. By [F1], D is Cartier and defines N=OX(D). The principal divisor does not change the invertible-sheaf class, so O(E)≅pr⁡X∗N. Restricting to X×V proves the assertion. Base extension and then restriction to a rational parameter point returns N after that base extension, proving parameter constancy. This argument neither assumes a k-rational point of V nor assumes k infinite or perfect.

Depends on

Used by

Dependency tree · two levels

78 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources