Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

The prime spectrum is compact in the library's non-Hausdorff sense

Statement

Assume the Axiom of Choice.

For every commutative ring R, the topological space Spec⁡(R) is compact.

Facts & Assumptions

Given: A commutative ring R, an open cover U of Spec⁡(R), and the Axiom of Choice.

[L1]

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).

[L2]

Every point of a Zariski-open set has a distinguished-open neighbourhood inside it (Every point of a Zariski-open set has a distinguished-open neighbourhood inside it).

[L3]

A distinguished-open cover of the spectrum forces the covering ideal to be the unit ideal (A distinguished-open cover of the spectrum forces the covering ideal to be the unit ideal).

[L4]

A finite unit expression 1=∑aifi yields the finite cover Spec⁡(R)=⋃D(fi) (A finite unit-ideal expression yields a finite distinguished-open subcover).

Proof

technique · direct
1.1L1given

If Spec⁡(R)=∅, then the empty subfamily of U already covers it. By [L1], the spectrum is compact in this case.

1.2L2givenchoose

Assume now that Spec⁡(R)≠∅. For each p∈Spec⁡(R), choose Up∈U with p∈Up. By [L2], choose fp∈R with p∈D(fp)⊆Up. Then {D(fp)}p∈Spec⁡(R) is a distinguished-open cover of the spectrum.

2.1L3step 1.2choose

By [L3], the ideal generated by the family {fp} is R. Hence there exist finitely many primes p1,…,pn∈Spec⁡(R) and coefficients a1,…,an∈R such that 1=a1fp1+⋯+anfpn.

3.1L4step 1.2step 2.1

Applying [L4] to this identity gives Spec⁡(R)=D(fp1)∪⋯∪D(fpn)⊆Up1∪⋯∪Upn. Thus U has a finite subcover.

4.1L1step 1.1step 3.1∎

Steps 1.1 and 3.1 show that every open cover of Spec⁡(R) has a finite subcover. Therefore Spec⁡(R) is compact by [L1].

Depends on

Used by

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