LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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.

Finite pullback preserves absolute ampleness

Statement

Assume the Axiom of Choice as inherited from the finite-morphism affineness interface (The Axiom of Choice). Let $g : Y \to X$ be a finite morphism of schemes (Finite morphisms of schemes) and let $L$ be an ample invertible $O_{X}$ -module (Absolute ampleness by affine section opens). Then the pullback $g^{*} L$ is an ample invertible $O_{Y}$ -module. The empty case is included: if $X = \emptyset$ then $Y = \emptyset$ and $g^{*} L$ is the (unique) invertible sheaf on the empty scheme, which is ample.

Facts & Assumptions

Given: A finite morphism $g : Y \to X$ , an ample invertible sheaf $L$ on $X$ , and the Axiom of Choice.

[A1]

The Axiom of Choice states that every family of nonempty sets has a choice function. (The Axiom of Choice)

[F1]

A morphism $g : Y \to X$ is finite if for every affine open $U = Spec A \subseteq X$ its inverse image is affine, $g^{- 1} (U) = Spec B$ , with $B$ module-finite over $A$ ; the zero ring is allowed, so an empty inverse image satisfies the condition. (Finite morphisms of schemes)

[F2]

Every finite morphism is affine: for every affine open $U \subseteq X$ the inverse image $g^{- 1} (U)$ is affine. (Finite is affine and local on its target)

[F3]

An invertible sheaf $L$ on $X$ is ample when $X$ is quasi-compact and for every $x \in X$ there are $n \geq 1$ and $s \in Γ (X, L^{n})$ with $x \in X_{s} = {image of s nonzero at x}$ and $X_{s}$ affine; the empty quasi-compact scheme is allowed, and $X_{s}$ is open. (Absolute ampleness by affine section opens)

[F4]

An invertible $O_{X}$ -module is a locally free sheaf of rank exactly one. (Invertible sheaves)

Proof

technique · direct: pull back the affine nonvanishing loci of the ampleness witness and use that a finite morphism onto an affine target has affine source

1.1F1F2F3given

$Y$ is quasi-compact. By [F1] the morphism $g$ is affine, hence quasi-compact: for an affine (therefore quasi-compact) open $U \subseteq X$ , the inverse image $g^{- 1} (U)$ is affine by [F2], hence quasi-compact. Since $L$ is ample, $X$ is quasi-compact by [F3]; the inverse image $Y = g^{- 1} (X)$ of the quasi-compact target $X$ is quasi-compact, by quasi-compactness of $g$ .

1.2F3F4algebra

Pullback of twists and of nonvanishing loci. The pullback $g^{*} L$ is invertible: over an open $V \subseteq X$ on which $L$ is trivial, $g^{*} L$ restricts to the trivial invertible sheaf on $g^{- 1} (V)$ , and these trivialisations are compatible on overlaps by [F4]. For $n \geq 1$ the canonical map $g^{*} (L^{n}) \to (g^{*} L)^{n}$ is an isomorphism, since pullback of modules commutes with tensor products. For $s \in Γ (X, L^{n})$ with pullback $g^{*} s \in Γ (Y, (g^{*} L)^{n})$ one has $Y_{g^{*} s} = g^{- 1} (X_{s}),$ because at $y \in Y$ with $x = g (y)$ the fibre of $(g^{*} L)^{n}$ at $y$ is $L^{n} (x) \otimes_{κ (x)} κ (y)$ , and the image of $g^{*} s$ is the scalar extension of the image of $s$ ; a vector in a one-dimensional space is nonzero exactly when its scalar extension to the field $κ (y)$ is nonzero.

2.1F1F2step 1.2

Pulled-back loci over affine witnesses are affine. Let $n \geq 1$ , $s \in Γ (X, L^{n})$ and suppose $X_{s}$ is affine. The restriction $g^{- 1} (X_{s}) \to X_{s}$ of $g$ is finite as a base change of the finite morphism $g$ , and its target $X_{s}$ is affine; by [F1] applied to the affine open $X_{s} \subseteq X_{s}$ of the target, the source $g^{- 1} (X_{s})$ is affine. By step 1.2 it equals $Y_{g^{*} s}$ .

3.1F3step 1.2step 2.1

The pulled-back witnesses cover $Y$ . Let $y \in Y$ and put $x = g (y)$ . By ampleness of $L$ there are $n \geq 1$ and $s \in Γ (X, L^{n})$ with $x \in X_{s}$ and $X_{s}$ affine. Then $y \in g^{- 1} (X_{s}) = Y_{g^{*} s}$ by step 1.2, and $Y_{g^{*} s}$ is affine by step 2.1.

4.1

Conclusion. By step 1.1 the scheme $Y$ is quasi-compact, and by step 3.1 every point of $Y$ lies in an affine nonvanishing locus of a global section of a positive power of the invertible sheaf $g^{*} L$ of step 1.2. Hence $g^{*} L$ is ample by [F3]. If $X = \emptyset$ then $Y = \emptyset$ since $g$ is a morphism, and the condition is vacuous; the Axiom of Choice [A1] is inherited only through the affineness interface of [F1], no choice being made here. [A1, F3, step 1.1, step 1.2, step 3.1] \qed

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

The Stacks Project, Properties of Schemes, Section 28.27 (Tag 01PS) (standard reference, not scraped)
Ravi Vakil, The Rising Sea, August 2022 draft, Section 17.6 (standard reference, not scraped)