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 quasi-compact image stable under specialization is closed
Statement
Assume AC. For a quasi-compact morphism , the image is closed if and only if it is stable under specialization in .
Facts & Assumptions
Given: AC and a quasi-compact morphism of schemes .
A morphism is quasi-compact when the inverse image of every quasi-compact open of is quasi-compact. (Quasi-compact and quasi-separated morphisms)
Every affine scheme is quasi-compact. (Every affine scheme is quasi-compact)
Every point of a scheme has an affine open neighbourhood. (Schemes)
A scheme morphism is a morphism of locally ringed spaces, hence has a continuous underlying map; an open subset of a scheme carries its open subscheme structure. (Morphisms of schemes, Morphisms of ringed spaces, Affine open subschemes)
A scheme is quasi-compact when its underlying topological space is quasi-compact, so every open cover of it has a finite subcover. (Quasi-compact and quasi-separated schemes)
The points of are prime ideals, and its basic opens are . (The underlying space of an affine spectrum)
A point is a specialization of when . (Specialisations, generalisations, and generic points)
A morphism corresponds to a ring map . (Affine schemes are contravariantly equivalent to commutative rings)
A homomorphism induces the contraction map , . (The map of affine spectra induced by a ring homomorphism)
For a prime , is multiplicative, and its image under is multiplicative in . (Localisation at a prime ideal: , Multiplicative subsets and the localisation as equivalence classes of fractions)
The localization is a commutative ring, and every for is a unit. (The localisation relation is an equivalence relation and fraction arithmetic is well defined)
A localization is the zero ring exactly when . (Equality, vanishing, and the kernel of the localisation map)
The Axiom of Choice states that every family of nonempty sets has a choice function. (The Axiom of Choice)
Under AC, every proper ideal of a nonzero commutative ring is contained in a maximal ideal. (In a nonzero commutative ring, every proper ideal is contained in a maximal ideal)
Every maximal ideal of a commutative ring is prime. (Every maximal ideal of a commutative ring is prime)
Proof
If is closed and , then . Thus every specialization of a point of is again in , so the image is stable under specialization.
Assume that is stable under specialization, and let . Choose an affine open containing by [F3]. Since is open, every open neighbourhood of in is also open in ; therefore lies in the closure in of .
The affine open is quasi-compact by [F2], so [F1] makes quasi-compact. It is an open subscheme of by [F4]. Its affine open neighbourhoods cover it by [F3], and [F5] gives a finite affine open cover ; empty members may be discarded.
The image is the finite union of the images . Some has in its closure in : otherwise, for each of the finitely many there would be an open neighbourhood of disjoint from , and the finite intersection of those neighbourhoods would miss their union, contradicting step 1.2. Fix such an and write . By [F9] the restricted morphism is induced by a ring map , and its image in has in its closure.
Let be the prime corresponding to , and put . Suppose . By [F13], , so for some . Every prime then contains , and [F10] shows its image lies outside . But is a basic open neighbourhood of by [F6, F7], contradicting that lies in the closure of the image of . Thus is nonzero.
The zero ideal of the nonzero commutative ring is proper. By [F14, F15], AC supplies a maximal ideal of , which is prime by [F16]. Its contraction along is prime by [F10]. It avoids , since each with is a unit by [F12] and a proper prime ideal contains no unit. Hence is a prime contained in : every has and so is not in .
The point lies in the image of . Since , every basic open containing also contains , by [F6, F7]. Thus in , so is a specialization of the image point in as well: every open neighbourhood of in restricts to one in the open set . Stability under specialization then gives .
Every point of belongs to by steps 1.2--6.1, so is closed. Together with step 1.1 this proves both directions. The empty source has empty image and satisfies both conditions; if an affine chart is the zero ring it is empty and can be discarded. A zero localization in step 4.1 is excluded by the closure argument. If is a field, then is its only prime, so the inclusion in step 5.1 is equality and the same proof handles a one-point affine target. The only AC use is prime existence in step 5.1; only a finite affine cover and a single chart from its finite list are used.
Depends on
- The Axiom of Choice
- Morphisms of schemes
- Morphisms of ringed spaces
- Quasi-compact and quasi-separated morphisms
- Quasi-compact and quasi-separated schemes
- Schemes
- Affine open subschemes
- Every affine scheme is quasi-compact
- The underlying space of an affine spectrum
- Principal distinguished subsets of the prime spectrum
- Specialisations, generalisations, and generic points
- Affine schemes are contravariantly equivalent to commutative rings
- The map of affine spectra induced by a ring homomorphism
- Localisation at a prime ideal: $R_{\mathfrak p}=(R\setminus\mathfrak p)^{-1}R$
- Multiplicative subsets and the localisation $S^{-1}R$ as equivalence classes of fractions
- The localisation relation is an equivalence relation and fraction arithmetic is well defined
- Equality, vanishing, and the kernel of the localisation map
- In a nonzero commutative ring, every proper ideal is contained in a maximal ideal
- Every maximal ideal of a commutative ring is prime
Used by
Dependency tree · two levels
49 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, Schemes, Lemma 26.19.7 (tag 05JL) (standard reference, not scraped)
- The Stacks Project, Commutative Algebra, Lemma 10.41.5 (tag 00HY) (standard reference, not scraped)