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.
A principal localization identifies its spectrum with a distinguished open
Statement
For , the morphism induced by identifies with the open locally ringed subspace of .
Facts & Assumptions
Given: A commutative ring and .
The map on prime spectra induced by is a homeomorphism onto (The spectrum of a principal localisation is the distinguished open D(f)).
The structure-sheaf sections on a distinguished open are the corresponding localizations (Sections and restrictions on distinguished opens of an affine scheme).
Proof
By [F1], the underlying map is a homeomorphism from onto .
On the relevant section rings are and , canonically isomorphic and compatible with restrictions.
The basic opens cover , so the preceding identifications give an isomorphism of locally ringed spaces.
Depends on
Used by
- A nonseparated affine cover can have nonaffine intersection Counterexample
- DVR uniqueness need not detect nonseparatedness Counterexample
- Finite type need not be locally free Counterexample
- Projective scheme of a homogeneous quotient and its standard affine charts Definition
- Relative projective space from standard charts Definition
- Strict transform of a closed subscheme Definition
- A basic open of the affine line Example
- Finite power map of the affine line Example
- Open immersions are etale Example
- Restricting an associated sheaf to a localization Example
- Acyclicity on intersections of a standard affine cover Lemma
- Affine pushforward algebra localizes Lemma
- Affineness is local on the target Lemma
- An affine scheme of finite type over a field has a finitely generated coordinate ring Lemma
- Birational morphisms restrict to isomorphisms between principal affine opens Lemma
- Closed gluing of two projective three-spaces is proper Lemma
- Closed immersions are affine quotients and survive base change Lemma
- Every distinguished open of an affine spectrum is quasi-compact Lemma
- Finite is affine and local on its target Lemma
- Glue relative spectra of affine-local algebras Lemma
- Integrality and reducedness of blowups from the Rees charts Lemma
- Intersections of affine opens admit principal affine covers Lemma
- Nonzero maps from an invertible sheaf to a locally free sheaf are injective Lemma
- Properness is local on the target Lemma
- Rational maps from a smooth curve to a proper scheme are morphisms Lemma
- Schematic closure and agreement on a dense open Lemma
- Scheme pullback preserves quasi-coherence Lemma
- Tensor product preserves quasi-coherence Lemma
- The spectrum of a finite product ring is the disjoint union of the factor spectra Lemma
- Valuation lifts detect universal closedness Lemma
- Affine acyclicity of quasi-coherent sheaves Theorem
- Closed immersions into affine schemes are quotient spectra Theorem
- Coherent sheaves on a locally Noetherian scheme Theorem
- Kernels and cokernels of quasi-coherent modules Theorem
- Projective n-space has quasi-coherent cohomological dimension at most n Theorem
Dependency tree · two levels
12 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, Lemma 26.6.6 (standard reference, not scraped)