LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-27

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.

Intersections of affine opens admit principal affine covers

Statement

If $U, V$ are affine open subschemes of a scheme $X$ , then $U \cap V$ is covered by open subschemes which are principal opens in $U$ and are also principal opens in affine open charts of $V$ .

Facts & Assumptions

Given: Affine open subschemes $U, V \subseteq X$ .

[L1]

Distinguished opens form a basis in an affine scheme, and sections on $D (f) \subseteq Spec A$ are $A_{f}$ (A principal localization identifies its spectrum with a distinguished open, Sections and restrictions on distinguished opens of an affine scheme).

Proof

technique · direct

1.1L1givenchoose

Fix $x \in U \cap V$ , and write $U = Spec A$ and $V = Spec B$ . The basis property in [L1] gives $f \in A$ and $g \in B$ such that $x \in D_{U} (f) \subseteq V$ and $x \in D_{V} (g) \subseteq U$ . Put $W = D_{U} (f) \cap D_{V} (g)$ ; it is an open neighbourhood of $x$ .

2.1L1step 1.1

The function $g$ on $V$ restricts to a section on $D_{U} (f)$ . By [L1], write that restriction as $a / f^{n}$ for some $a \in A$ and $n \geq 0$ . On $D_{U} (f)$ , its nonvanishing locus is $D_{U} (a) \cap D_{U} (f) = D_{U} (f a)$ . Hence $W = D_{U} (f a)$ is principal in $U$ .

2.2L1step 1.1

Symmetrically, the restriction of $f$ to $D_{V} (g)$ is a section $b / g^{m}$ for some $b \in B$ and $m \geq 0$ . Its nonvanishing locus there is $D_{V} (g b)$ , so the same open $W$ is principal in $V$ .

3.1step 2.1step 2.2∎

Every $x \in U \cap V$ has such a common principal neighbourhood $W$ . These neighbourhoods cover the intersection and prove the claim.

Depends on

Used by

Dependency tree · two levels

11 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

Ravi Vakil, Foundations of Algebraic Geometry, Section 6.3 (standard reference, not scraped)