Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30
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 g:Z→Y, the image g(Z) is closed if and only if it is stable under specialization in Y.

Facts & Assumptions

Given: AC and a quasi-compact morphism of schemes g:Z→Y.

[F1]

A morphism g is quasi-compact when the inverse image of every quasi-compact open of Y is quasi-compact. (Quasi-compact and quasi-separated morphisms)

[F2]

Every affine scheme is quasi-compact. (Every affine scheme is quasi-compact)

[F3]

Every point of a scheme has an affine open neighbourhood. (Schemes)

[F4]

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)

[F5]

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)

[F6]

The points of Spec⁡A are prime ideals, and its basic opens are D(f)={p:f∉p}. (The underlying space of an affine spectrum)

[F7]

D(f)={p∈Spec⁡(R):f∉p}. (Principal distinguished subsets of the prime spectrum)

[F8]

A point y is a specialization of x when y∈{x}‾. (Specialisations, generalisations, and generic points)

[F9]

A morphism Spec⁡B→Spec⁡A corresponds to a ring map φ:A→B. (Affine schemes are contravariantly equivalent to commutative rings)

[F10]

A homomorphism φ:A→B induces the contraction map Spec⁡B→Spec⁡A, q↦φ−1q. (The map of affine spectra induced by a ring homomorphism)

[F11]

For a prime p⊂A, A∖p is multiplicative, and its image under φ is multiplicative in B. (Localisation at a prime ideal: Rp=(R∖p)−1R, Multiplicative subsets and the localisation S−1R as equivalence classes of fractions)

[F12]

The localization S−1B is a commutative ring, and every s/1 for s∈S is a unit. (The localisation relation is an equivalence relation and fraction arithmetic is well defined)

[F13]

A localization S−1B is the zero ring exactly when 0∈S. (Equality, vanishing, and the kernel of the localisation map)

[F14]

The Axiom of Choice states that every family of nonempty sets has a choice function. (The Axiom of Choice)

[F15]

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)

[F16]

Every maximal ideal of a commutative ring is prime. (Every maximal ideal of a commutative ring is prime)

Proof

technique · direct
1.1F8

If g(Z) is closed and x∈g(Z), then {x}‾⊆g(Z). Thus every specialization of a point of g(Z) is again in g(Z), so the image is stable under specialization.

1.2F3given

Assume that g(Z) is stable under specialization, and let y∈g(Z)‾. Choose an affine open U=Spec⁡A⊆Y containing y by [F3]. Since U is open, every open neighbourhood of y in U is also open in Y; therefore y lies in the closure in U of g(Z)∩U.

2.1F1F2F3F4F5step 1.2

The affine open U is quasi-compact by [F2], so [F1] makes ZU=g−1(U) quasi-compact. It is an open subscheme of Z by [F4]. Its affine open neighbourhoods cover it by [F3], and [F5] gives a finite affine open cover ZU=⋃i=1nWi; empty members may be discarded.

3.1F3F9step 1.2step 2.1

The image g(Z)∩U is the finite union of the images g(Wi). Some g(Wi) has y in its closure in U: otherwise, for each of the finitely many i there would be an open neighbourhood of y disjoint from g(Wi), and the finite intersection of those neighbourhoods would miss their union, contradicting step 1.2. Fix such an i and write Wi=Spec⁡B. By [F9] the restricted morphism is induced by a ring map φ:A→B, and its image in U has y in its closure.

4.1F6F7F10F11F13step 3.1algebra

Let p⊂A be the prime corresponding to y, and put S=φ(A∖p). Suppose S−1B=0. By [F13], 0∈S, so φ(f)=0 for some f∉p. Every prime q⊂B then contains φ(f), and [F10] shows its image lies outside D(f). But D(f) is a basic open neighbourhood of y by [F6, F7], contradicting that y lies in the closure of the image of Spec⁡B. Thus S−1B is nonzero.

5.1F10F12F14F15F16step 4.1algebra

The zero ideal of the nonzero commutative ring S−1B is proper. By [F14, F15], AC supplies a maximal ideal m of S−1B, which is prime by [F16]. Its contraction q⊂B along B→S−1B is prime by [F10]. It avoids S, since each s/1 with s∈S is a unit by [F12] and a proper prime ideal contains no unit. Hence p′:=φ−1(q) is a prime contained in p: every a∉p has φ(a)∈S and so is not in q.

6.1F6F7F8step 5.1

The point p′ lies in the image of Spec⁡B. Since p′⊆p, every basic open D(f) containing p also contains p′, by [F6, F7]. Thus p∈{p′}‾ in U, so y is a specialization of the image point in Y as well: every open neighbourhood of y in Y restricts to one in the open set U. Stability under specialization then gives y∈g(Z).

7.1step 1.1step 1.2step 2.1step 4.1step 5.1step 6.1∎

Every point of g(Z)‾ belongs to g(Z) by steps 1.2--6.1, so g(Z) 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 A is a field, then p=(0) is its only prime, so the inclusion p′⊆p 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

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