Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck 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 regular point lies on one irreducible component

Statement

Assume the Axiom of Choice (The Axiom of Choice). A regular point of a reduced Noetherian scheme lies on exactly one irreducible component.

Facts & Assumptions

Given: A reduced Noetherian scheme X and a point x∈X whose local ring is regular.

[F1]

AC says every family of nonempty sets has a choice function (The Axiom of Choice).

[F2]

A Noetherian scheme has a finite affine open cover by spectra of Noetherian rings (Locally Noetherian and Noetherian schemes).

[F3]

An open subscheme has the restricted structure sheaf, and an affine open subscheme is affine with that structure sheaf (Affine open subschemes).

[F4]

For U=Spec⁡A and x↔p∈Spec⁡A, the stalk is OU,x≅Ap (The stalk of the affine structure sheaf at a prime is A_p).

[F5]

A point is regular when its local ring is regular local (Regular points of locally Noetherian schemes).

[F6]

Under AC, every regular local ring is a domain (regular local rings are domains and cohen macaulay).

[F7]

An irreducible component of a scheme is a maximal irreducible closed subset of its underlying space (Irreducible components as schemes).

[F8]

In an irreducible space, every nonempty open subset is dense (Irreducibility via nonempty open subsets, connectedness and open subspaces).

[F9]

Under AC, the closure of an irreducible subset is irreducible (Existence and basic properties of irreducible components).

[F10]

Under AC, the irreducible components of Spec⁡A are exactly V(q) for minimal prime ideals q of A (Irreducible components of the spectrum correspond to minimal prime ideals).

[F11]

For a multiplicative set S⊆A, primes of S−1A correspond bijectively and in an inclusion-preserving way to primes of A disjoint from S; the inverse is extension (Prime ideals of a localization are exactly the primes disjoint from the denominator set).

[F12]

V(q) consists of the primes containing q (The prime spectrum and vanishing sets).

[F13]

A nonempty open subset of an irreducible space is irreducible (Irreducibility via nonempty open subsets, connectedness and open subspaces).

[F14]

Under AC, every point lies in an irreducible component (Existence and basic properties of irreducible components).

[F15]

Proof

1.1F1F2F3F4F5F6F15given

Fix x. By the AC assumption [F1] and [F2], choose an affine open neighbourhood U=Spec⁡A of x with A Noetherian. Write x as the prime p⊂A. The open-scheme structure in [F3] and the affine stalk calculation [F4] identify OX,x with Ap. Since x is regular, this is a regular local ring by [F5], and therefore a domain by [F6]. Put S=A∖p; by [F15], Ap=S−1A. These are pointwise choices of one chart and its corresponding prime; no family of charts is chosen.

1.2F7F8F9F10F12F13given

Let C be any irreducible component of X containing x. By [F7], C is closed and irreducible. The subset C∩U is a nonempty open subset of C, so [F8] makes it dense in C and [F13] makes it irreducible. It is closed in U because C is closed in X. To see it is maximal irreducible in U, let Z be an irreducible closed subset of U containing C∩U. Its closure Z‾ in X is irreducible by [F9]. Since C∩U⊆Z⊆Z‾ and C∩U is dense in C, we have C⊆Z‾. The maximality of C then gives C=Z‾. As Z is closed in U, Z‾∩U=Z, so C∩U=Z. Thus C∩U is an irreducible component of U. By [F10], there is a unique minimal prime qC of A with C∩U=V(qC). Since x corresponds to p and lies in this vanishing set, [F12] gives qC⊆p.

2.1F8F11F15step 1.1step 1.2

The prime correspondence [F11] identifies the primes of Ap with primes of A contained in p. Since qC is minimal in A, its extension qCAp is minimal in Ap: a prime properly below it would contract to a prime properly below qC. But Ap is a domain by step 1.1, so its only minimal prime is (0). Hence qCAp=(0). The localization correspondence is one-to-one, so all components C through x have the same prime qC. Their intersections with U are therefore the same; each such intersection is dense in its component by [F8], so taking its closure in X recovers that component. Thus there is at most one component through x.

3.1F1F6F10F14step 1.1step 2.1given∎

Under the assumed AC [F1], [F14] gives at least one irreducible component through x. Together with step 2.1 this proves there is exactly one. If X is empty, there is no point x and the assertion is vacuous. If the local dimension is zero, Ap is a zero-dimensional local domain and hence a field; the same minimal-prime argument still gives one component. No dimension restriction was used in steps 1.1–2.1. AC is also used through [F6] and [F10] for the local-domain theorem and the affine minimal-prime correspondence. For the fixed point x, the proof chooses one chart and makes no simultaneous choices. The statement is a uniqueness-and-existence claim, not an iff criterion; no endpoint parameter is present.

Depends on

Used by

Dependency tree · two levels

52 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