LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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.

Affine finite-type source immerses into relative projective space

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $S$ be a scheme and let $f : U \to S$ be a locally finite-type morphism with $U$ affine. Then there are $N \geq 0$ and an $S$ -immersion $j : U \to P_{S}^{N}$ . The assertion includes $U = \emptyset$ . No separatedness or Noetherian hypothesis on $S$ is needed.

Facts & Assumptions

Given: The Axiom of Choice, a scheme $S$ , an affine scheme $U = Spec B$ , and a locally finite-type morphism $f : U \to S$ .

[F1]

Every point of an affine scheme has a distinguished-open neighbourhood inside any prescribed open neighbourhood, and an affine scheme is quasi-compact. (Every point of a Zariski-open set has a distinguished-open neighbourhood inside it, Affine open subschemes)

[F2]

If $D (a) = Spec B_{a} \subseteq U$ maps into an affine open $V = Spec R \subseteq S$ and $f$ is locally finite type, then $R \to B_{a}$ is a finite-type ring map: locally finite type is affine-local on source and target, and the affine source is quasi-compact. (Finite type is affine-local on source and target, Locally finite type and finite type morphisms)

[F3]

Under AC, global sections $s_{0}, \dots, s_{N}$ generating an invertible sheaf $L$ on an $S$ -scheme $U$ define a unique $S$ -map $j : U \to P_{S}^{N}$ . Its inverse image of the standard chart $D_{+} (T_{i})$ is the nonvanishing open of $s_{i}$ , and on it $T_{k} / T_{i}$ pulls back to $s_{k} / s_{i}$ . (Generating line-bundle sections define a morphism to projective space, The Axiom of Choice)

[F4]

Over an affine base open $V = Spec R$ , the standard chart $D_{+} (T_{i})$ of $P_{V}^{N}$ is $Spec R [T_{k} / T_{i} : k \neq i]$ . A surjection of coordinate rings defines a closed immersion of affine schemes. (Relative projective space from standard charts, Closed immersions into affine schemes are quotient spectra)

[F5]

A morphism is a closed immersion if its restrictions over an open cover of its target are closed immersions. Composing a closed immersion into an open subscheme with that open immersion gives an immersion. (Closed immersions are local on the target, Immersion of schemes)

Proof

technique · direct: use finitely many principal source opens over affine base opens, clear denominators in their coordinate generators, and obtain closed immersions on the corresponding projective charts

1.1F1given

If $U = \emptyset$ , take $N = 0$ and the unique empty immersion into $P_{S}^{0}$ . Suppose $U \neq \emptyset$ . For each $u \in U$ choose an affine open $V_{u} \subseteq S$ containing $f (u)$ and then a distinguished open $D (a_{u}) \subseteq U$ with $u \in D (a_{u}) \subseteq f^{- 1} (V_{u})$ by [F1]. Quasi-compactness gives finitely many pairs $(a_{i}, V_{i})$ , $1 \leq i \leq m$ , with $U = ⋃_{i} D (a_{i})$ , so $(a_{1}, \dots, a_{m}) = B$ .

2.1F2step 1.1algebra

Write $V_{i} = Spec R_{i}$ . By [F2], $R_{i} \to B_{a_{i}}$ is finite type. Choose finitely many generators of $B_{a_{i}}$ as an $R_{i}$ -algebra and write them as $b_{i j} / a_{i}^{e_{i j}}$ , with $b_{i j} \in B$ and $e_{i j} \geq 0$ ; an empty generator list is allowed. Choose $d \geq 1$ exceeding every exponent $e_{i j}$ , and define $s_{i} = a_{i}^{d}$ and $t_{i j} = b_{i j} a_{i}^{d - e_{i j}}$ in $B = Γ (U, O_{U})$ .

3.1F3step 1.1step 2.1

The sections $s_{i}$ and $t_{i j}$ of the trivial line bundle $O_{U}$ generate it: the nonvanishing opens $D (s_{i}) = D (a_{i})$ cover $U$ by step 1.1. By [F3] they give an $S$ -morphism $j : U \to P_{S}^{N}$ , where $N = m + \sum_{i} r_{i} - 1 \geq 0$ and $r_{i}$ is the number of $t_{i j}$ . On $D (a_{i})$ the projective coordinate ratios for $t_{i j}$ are $t_{i j} / s_{i} = b_{i j} / a_{i}^{e_{i j}}$ .

4.1F3F4step 1.1step 2.1step 3.1

Let $W_{i} = D_{+} (T_{i}) \cap P_{V_{i}}^{N}$ , with $T_{i}$ the coordinate for $s_{i}$ . By [F3], $j^{- 1} (W_{i}) = D (a_{i})$ : $j^{- 1} D_{+} (T_{i}) = D (s_{i}) = D (a_{i})$ , and this open maps into $V_{i}$ by step 1.1. Both $W_{i}$ and $D (a_{i})$ are affine by [F4], and the coordinate map $O (W_{i}) = R_{i} [T_{k} / T_{i} : k \neq i] \to B_{a_{i}}$ is surjective because the ratios $t_{i j} / s_{i}$ are the chosen $R_{i}$ -algebra generators from step 2.1. Hence $D (a_{i}) \to W_{i}$ is a closed immersion.

5.1F3F5step 1.1step 4.1∎

The opens $W_{i}$ cover the image $j (U)$ because their inverse images $D (a_{i})$ cover $U$ . Put $W = ⋃_{i} W_{i} \subseteq P_{S}^{N}$ . By [F5], the restrictions of $j : U \to W$ over the cover $W_{i}$ make it a closed immersion. Its composite with $W ↪ P_{S}^{N}$ is therefore an immersion. The empty case was handled in step 1.1, and AC permits the pointwise affine-neighbourhood choices in 1.1 and is also inherited through the projective-map construction [F3].

Depends on

Used by

Chow lemma for proper Noetherian schemes Lemma

Dependency tree · two levels

34 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, Morphisms of Schemes, Lemma 29.40.3 (Tag 01VS), affine-source case (standard reference, not scraped)