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.
Affineness is local on the target
Statement
A morphism is affine if and only if there exists an affine open cover for which every is affine.
Facts & Assumptions
Given: The objects, hypotheses and conventions in the statement above.
A morphism of schemes is affine when is affine for every affine open subscheme . Here the inverse image carries the restricted structure sheaf, as in def-affine-open-subscheme, and is a morphism of locally ringed spaces as in def-morphism-of-schemes. The empty scheme is affine, being . Affineness of a morphism does not require its total source or target to be affine. (Affine morphisms)
Let be a scheme, , and . Write for the open locus where the germ of is a unit. If and each is affine, then is affine. In fact the canonical morphism is an isomorphism. Empty and are allowed. (Affineness from a finite principal cover)
For , the morphism induced by identifies with the open locally ringed subspace of . (A principal localization identifies its spectrum with a distinguished open)
Every affine scheme is quasi-compact. (Every affine scheme is quasi-compact)
Assume the Axiom of Choice (def-axiom-of-choice). In a nonzero commutative ring, every proper ideal is contained in a maximal ideal. (In a nonzero commutative ring, every proper ideal is contained in a maximal ideal)
Proof
If is affine, F1 gives the condition on any affine cover. Conversely suppose such a cover is given and let be arbitrary affine open. For , choose a principal open containing and contained in . Choose a principal open containing and contained in . On the affine the restriction of is , so is also , a principal open of .
F4 gives finitely many such covering . Their functions generate the unit ideal of : if the ideal were proper F5 supplies a maximal, hence prime, ideal containing it would lie outside the cover, contrary to . Each is principal in the affine , so it is affine by F3.
The pullbacks of the are global sections of on generating 1. F2 shows that is affine. Since was arbitrary, F1 proves affine. Empty , a singleton cover, nilpotents, and an empty source are included by F2 and the same formulas.
Depends on
Used by
Dependency tree · two levels
24 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
- Stacks 29.11.3(1) iff (2), Remark 29.11.4; 26.11.5–6 (standard reference, not scraped)