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.
Scheme-theoretic image of a quasi-compact morphism
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be a quasi-compact morphism of schemes and put . Then is a quasi-coherent ideal sheaf, and the closed subscheme is the scheme-theoretic image of . For every open , its restriction is the scheme-theoretic image of .
Facts & Assumptions
Given: The Axiom of Choice and a quasi-compact morphism .
A morphism is quasi-compact when inverse images of quasi-compact opens are quasi-compact Quasi-compact and quasi-separated morphisms.
Under AC, for a scheme, quasi-coherent ideal sheaves and closed subschemes are in mutually inverse correspondence Quasi-coherent ideals and closed subschemes.
Localization of modules is exact, so it preserves kernels; it also commutes with finite products, including the empty product. Localisation of modules is exact
For an affine scheme and , the structure-sheaf sections on are . Sections and restrictions on distinguished opens of an affine scheme
Proof
Let be an affine open of . By [F1], is quasi-compact, so its affine-open cover has a finite subcover ; when is empty, take the finite empty cover. The finite-subcover step and the correspondence used below are licensed by the given AC.
Write and let be induced by . The sheaf condition makes inject into , so the kernel of equals the ideal . For , the opens cover , and [F4] identifies their section rings with . The sheaf condition therefore makes the kernel of equal to . By [F3], localizing the exact sequence identifies this kernel with : localization commutes with the finite product. The same argument includes the empty cover, for which both kernels are the whole source ring.
Thus is the ideal sheaf associated to on every affine , so is quasi-coherent.
By [F2], defines a closed subscheme . On each affine , the map factors through , so factors through it. If a closed subscheme defined on by also receives , then ; hence factors through that competing closed subscheme. This proves minimality.
Repeating the kernel computation on an open gives the restriction of to . The correspondence in [F2] therefore identifies with the scheme-theoretic image of .
Depends on
The Axiom of Choice
Scheme-theoretic image
Quasi-compact and quasi-separated morphisms
Quasi-coherent ideal sheaves
Quasi-coherent ideals and closed subschemes
Morphisms of schemes are local on compatible open covers
Localisation of modules is exact
Sections and restrictions on distinguished opens of an affine scheme