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.
Morphisms to an affine scheme and global sections
Statement
For a scheme and a ring , taking global sections induces a natural bijection
Facts & Assumptions
Given: A scheme and a commutative ring .
Proof
A morphism induces the ring map on global sections .
Conversely, a ring map gives the canonical morphism from to the affine scheme , checked on affine opens by the affine anti-equivalence and glued over an affine cover of .
On each affine open the two constructions are inverse by the affine anti-equivalence; equality of scheme morphisms is local on the source, hence they are mutually inverse and natural.
Depends on
Used by
- Maps from proper integral schemes to the affine line have closed-point image Corollary
- Global generation does not imply very ampleness Counterexample
- A nilpotent thickening of an affine scheme is affine Lemma
- A proper geometrically integral affine scheme is a point Lemma
- Affine neighbourhood containing component generic points Lemma
- Affineness and properness descend under finite purely inseparable scalar extension Lemma
- Affineness from a finite principal cover Lemma
- Affineness of a field form of a diagonalizable group Lemma
- An affine open in a smooth integral variety has Cartier boundary Lemma
- Cartan subgroups: conjugacy, density and normalizers Lemma
- Closed immersions are affine quotients and survive base change Lemma
- Fibrewise constant morphisms from an abelian scheme factor through the base Lemma
- Field-valued points and local-ring points Lemma
- Finite Galois descent of morphisms of schemes Lemma
- Fixed loci and centralizers of torus actions are connected Lemma
- Good quotients are local on the target and are categorical quotients Lemma
- Immersions and affine localizations are monomorphisms Lemma
- Morphisms descend under a finite field extension with the full descent identity Lemma
- Morphisms from complete connected schemes to affine schemes are constant Lemma
- Proper normal curve rational function map Lemma
- Rational maps from a smooth curve to a proper scheme are morphisms Lemma
- Rigidity for a proper geometrically integral factor Lemma
- Rigidity for an integral factor with only constant functions Lemma
- Schematic closure and agreement on a dense open Lemma
- Scheme morphisms satisfy fppf descent Lemma
- Affine fibre products are spectra of tensor products Theorem
- Closed immersions into affine schemes are quotient spectra Theorem
- Generating line-bundle sections define a morphism to projective space Theorem
- Global functions on proper integral schemes form a finite extension of the base field Theorem
- Irreducible classical varieties and integral separated finite-type schemes Theorem
- Representability and smoothness of concentrator subschemes Theorem
- Smooth proper curves, dominant morphisms and function fields Theorem
Dependency tree · two levels
11 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
- Ravi Vakil, Foundations of Algebraic Geometry, Section 7.3.F (standard reference, not scraped)