CorollaryStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05

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.

Every distinguished open subset is compact

Statement

Assume the Axiom of Choice.

Let $R$ be a commutative ring and let $f \in R$ . Then the distinguished open subset $D (f) \subseteq Spec (R)$ is compact in its subspace topology.

Facts & Assumptions

Given: A commutative ring $R$ , an element $f \in R$ , an open cover $U$ of $D (f)$ , and the Axiom of Choice.

[L1]

The localization map $R \to R_{f}$ induces a homeomorphism $h : Spec (R_{f}) \to D (f)$ (The spectrum of a principal localisation is the distinguished open D(f)).

[L2]

The spectrum of every commutative ring is compact (The prime spectrum is compact in the library's non-Hausdorff sense).

[L3]

A topological space is compact when every open cover has a finite subcover (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[A1]

If $h : X \to Y$ is a homeomorphism and $V$ is an open cover of $Y$ , then ${h^{- 1} (V) : V \in V}$ is an open cover of $X$ ; a finite subcover of the latter pushes forward to a finite subcover of the former.

Proof

technique · direct

1.1

By [L1], there is a homeomorphism $h : Spec (R_{f}) \to D (f)$ . By [L2], the domain $Spec (R_{f})$ is compact.

L1L2

2.1

Apply [A1] to the open cover $U$ of $D (f)$ . The inverse images $h^{- 1} (U)$ with $U \in U$ form an open cover of $Spec (R_{f})$ , so compactness from step 1.1 gives finitely many $U_{1}, \dots, U_{n} \in U$ whose inverse images cover $Spec (R_{f})$ . Then $U_{1}, \dots, U_{n}$ cover $D (f)$ .

A1step 1.1choose

3.1

Thus every open cover of $D (f)$ has a finite subcover, so $D (f)$ is compact by [L3].

L3step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Proposition (13.20) (standard reference, not scraped)
The Stacks Project, Lemma 10.17.9 (standard reference, not scraped)