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

An immersion with closed image is a closed immersion

Statement

Let $i : Z \to X$ be an immersion of schemes. If the image $i (Z)$ is closed in $X$ , then $i$ is a closed immersion.

Facts & Assumptions

Given: An immersion $i : Z \to X$ with $i (Z)$ closed in $X$ , and a factorization $i = j \circ c$ with $c : Z \to U$ a closed immersion into an open subscheme $j : U ↪ X$ .

[F1]

A morphism $i$ is an immersion if there exist an open subscheme $j : U ↪ X$ and a closed immersion $c : Z \to U$ with $i = j \circ c$ ; the property depends only on $i$ , and $j$ is a homeomorphism onto $U$ , so $i (Z) = c (Z)$ as subsets of $X$ . (Immersion of schemes)

[F2]

A morphism $i : Z \to X$ is a closed immersion if its underlying map is a homeomorphism onto a closed subset of $X$ and $O_{X} \to i_{*} O_{Z}$ is surjective; a closed immersion $c$ has $O_{U} \to c_{*} O_{Z}$ surjective, and for an open immersion $j : U ↪ X$ the stalk maps of $O_{X} \to j_{*} O_{U}$ are isomorphisms at points of $U$ . (Closed immersions of schemes)

Proof

1.1

By [F1] the underlying map of $i$ is the composite of the homeomorphism $Z \to c (Z)$ induced by $c$ and the inclusion $c (Z) \subseteq U \subseteq X$ ; hence it is a homeomorphism onto the subset $i (Z) = c (Z)$ of $X$ , which is closed in $X$ by hypothesis.

F1given

2.1

It remains to check the structure sheaf map $O_{X} \to i_{*} O_{Z}$ of [F2] on stalks. For $x \in X$ with $x \notin i (Z)$ one has $(i_{*} O_{Z})_{x} = 0$ , so surjectivity at $x$ is automatic.

F2step 1.1

2.2

For $x \in i (Z) \subseteq U$ the stalk map factors through the open-immersion stalk isomorphism $O_{X, x} \to O_{U, x}$ followed by the stalk at $x$ of the surjection $O_{U} \to c_{*} O_{Z}$ of [F2], hence is surjective; the identifications $(i_{*} O_{Z})_{x} = (c_{*} O_{Z})_{x}$ hold because $j$ maps $U$ homeomorphically onto the open set $U$ containing $x$ .

F2step 1.1

3.1

Steps 1.1, 2.1 and 2.2 verify both clauses of [F2]: the underlying map is a homeomorphism onto the closed subset $i (Z)$ and the structure sheaf map is surjective, so $i$ is a closed immersion.

F2step 1.1step 2.1step 2.2∎

Depends on

Used by

Valuative uniqueness detects separatedness Theorem

Dependency tree · two levels

5 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, Schemes, Lemma 26.10.4, printed p.18 (standard reference, not scraped)