Alphabeta MathHow 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.
Principal localisation
Definition
For a commutative ring and , the powers form a multiplicative subset. The principal localisation of at is Its elements may be written . In particular, is canonically isomorphic to , while is the zero ring.
Depends on
Used by
- Primes of a principal localization Corollary
- Quasi-finite algebras are source locally localizations of finite algebras Corollary
- The quasi-finite locus of a finite-type algebra is open Corollary
- Quasi-finite does not imply finite Counterexample
- A finite algebra is its own Zariski Main factor Example
- The punctured affine line as an open finite factorization Example
- ℤ[1/6] consists exactly of rationals a/6ⁿ and inverts precisely the primes 2 and 3 Example
- Finite normalization commutes with principal localization Lemma
- Finite-type field extensions with zero Ω Lemma
- Localisation at a homogeneous element is graded, with graded kernels and dehomogenised degree-zero parts Lemma
- One-variable integral correction after leading-coefficient localization Lemma
- The spectrum of a finite product ring is the disjoint union of the factor spectra Lemma
- Localising twice is localising once at the multiplicative set generated by both denominator sets Proposition
- A quasi-finite algebra factors openly through a finite algebra Theorem
- Algebraic Zariski Main localization at a quasi-finite prime Theorem
- Global regular functions on a classical affine variety are its coordinate ring Theorem
- Regular functions on a principal open are the principal localization Theorem
- Regular functions on a principal open are the principal localization of the coordinate ring Theorem
- Two coprime projective plane forms meet in total length equal to their degree product Theorem
Dependency tree · two levels
4 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, Section 10.9: Localization (standard reference, not scraped)