ExampleConstruction: Literature-sourcedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

The scheme-theoretic image of a dense open immersion

Example

Let $X$ be an integral scheme and let $j : U ↪ X$ be a dense open immersion. Then the scheme-theoretic image of $j$ is $X$ itself. This does not assume that $j$ is quasi-compact.

Facts & Assumptions

Given: An integral scheme $X$ and a dense open immersion $j : U ↪ X$ .

[F1]

Every nonempty affine open of an integral scheme is the spectrum of a domain Integral schemes.

[F2]

The scheme-theoretic image, when it exists, is the smallest closed subscheme through which the morphism factors Scheme-theoretic image.

Verification

technique · direct

1.1given

Let $Z ↪ X$ be a closed subscheme through which $j$ factors, and let $I$ be its ideal sheaf. On a nonempty affine open $V = Spec A$ , every $a \in I (V)$ restricts to zero on the dense open $U \cap V$ .

2.1F1step 1.1choose

Choose a nonempty principal open $D (f) \subseteq U \cap V$ . By [F1], $A$ is a domain and $f \neq 0$ ; the equality $a / 1 = 0$ in $A_{f}$ gives $f^{n} a = 0$ for some $n$ , hence $a = 0$ . Thus $I ∣_{V} = 0$ .

3.1F2step 2.1∎

The same holds on every nonempty affine open, while the empty opens carry only the zero ideal. Hence $I = 0$ , so every closed factorization of $j$ contains $X$ itself. By [F2], the smallest such factorization is $X$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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.6.7 (standard reference, not scraped)