Alphabeta Math
LemmaStatement: AI-generatedProof: AI-generated
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.

Functions extend across codimension two

PDF p. 9: Equality of functions and units on the smooth locus

Statement

Assume the Axiom of Choice. Let X be a noetherian normal scheme and let j:U↪X be an open immersion whose image contains every point of codimension at most one in its irreducible component. Then restriction is an isomorphism of sheaves of rings OX≅j∗OU. Consequently restriction gives isomorphisms on global functions and on groups of global units.

Here a noetherian normal scheme is a scheme with a finite cover by spectra of noetherian rings and with all local rings integrally closed domains. The codimension of a point in its irreducible component is the supremum of the lengths of chains of strict specializations from that component's generic point to the given point. A global unit is a global function admitting a multiplicative inverse.

Facts & Assumptions

[F1]

Under the Axiom of Choice, every affine open of a noetherian normal scheme is the spectrum of a finite product of noetherian integrally closed domains; the corresponding factor spectra are open and closed integral subschemes (Normal noetherian schemes reduce to integral components).

[F2]

Under the Axiom of Choice, a noetherian integrally closed domain A with fraction field K equals the intersection of its height-one localizations inside K (A normal Noetherian domain is the intersection of its height-one localizations). If there are no height-one primes, the intersection is understood to be K.

[A1]

The Axiom of Choice is assumed for [F1] and [F2] (The Axiom of Choice).

Proof

Given: A noetherian normal scheme X, an open immersion j:U↪X containing all points of component codimension at most one, and the Axiom of Choice.

Goal: Show that OX→j∗OU is an isomorphism and obtain the asserted global isomorphisms.

1.1F1A1given

It suffices to prove that restriction OX(V)→OU(U∩V) is an isomorphism on a basis of affine opens V: the kernel and cokernel sheaves then have zero stalks. By [F1], each such V is a finite disjoint union of affine spectra of noetherian integrally closed domains. These factor spectra form a basis as V varies, and restriction to a factor preserves its structure sheaf. Thus it is enough to consider V=Spec⁡A for such a domain A. Its generic point and each point corresponding to a height-one prime of A belong to U: codimension is unchanged when passing to an open neighborhood, since chains of generalizations of a point in an open set remain in that open set.

2.1F2A1step 1.1given

Put W=U∩V and let K=Frac⁡(A). Since W contains the generic point, it is dense in the integral scheme V. A section s on W determines an element z∈K by its generic stalk. For every height-one prime p, the point p lies in W, so the germ of s there belongs to Ap and maps to z in K. Hence z lies in every height-one localization, and [F2] gives z∈A. The section defined by z agrees with s on W: on any principal open D(f)⊆W, both are elements of the domain Af and have the same image in K, so they are equal; such opens cover W. Thus restriction from A to OU(W) is surjective. It is injective because W contains the generic point and A↪K is injective. This also covers the case that A is a field.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 show that the restriction morphism is an isomorphism on a basis and therefore an isomorphism of sheaves of rings. Taking sections over X gives Γ(X,OX)≅Γ(U,OU). A ring isomorphism carries precisely the invertible elements to invertible elements, with inverses preserved, so it also gives an isomorphism of global unit groups.

Depends on

Used by · 2

Dependency tree · 3 levels

Arrows run from prerequisites to the items that use them. External source nodes link directly to the cited text. The view shows up to three dependency steps; open a prerequisite to continue.