Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

Stalks of the scheme-theoretic fibre

Statement

For f:XS and xX with s=f(x), use the corresponding point of Xs. There are canonical local-ring isomorphisms OXs,xOX,x/msOX,xOX,xOS,sκ(s).

Facts & Assumptions

Given: The objects, hypotheses and conventions in the statement above.

[F1]

For f:XS and sS, the projection XsX is a homeomorphism onto f1(s) with the subspace topology and preserves the residue field at every point. In compatible affine charts AB, s=p, its points correspond exactly to primes qB contracting to p; no extra embedding choice occurs. Also X×SSpecOS,sX is a homeomorphism onto the inverse image of the set of generalizations of s. (Points and topology of a fibre)

[F2]

Let AB be a ring map, pSpecA, and M=Ap, acting on B through the ring map. The fibre over p is canonically Spec(BAκ(p))Spec(M1B/pM1B). The residue field is κ(p)=Ap/pAp. No reduction of the tensor ring is taken. (Coordinate ring of an affine fibre)

[F3]

For pSpecA, there is a canonical isomorphism OSpecA,pAp. (The stalk of the affine structure sheaf at a prime is A_p)

Proof

1.1

Choose compatible affine neighbourhoods AB, with primes p,q representing s,x. F1 identifies the relevant fibre point, and F2 gives the ring (Ap)1B/p(Ap)1B.

givenF1F2
2.1

Localize at that point, using F3. All elements of Ap are already units in Bq, so the result is Bq/pBq. Under the stalk identifications, the extended ideal is exactly msOX,x.

F3step 1.1
3.1

For any ring map RH and ideal J, the maps hrhrmodJH and hmodJHh1 are well-defined inverse ring maps HRR/JH/JH. Apply this with R=OS,s, H=OX,x and J=ms. The ideal is contained in mx, so this stalk is nonzero; if there is no point over s, the assertion has no instance. Nilpotents are not removed, and J=0 gives the unchanged stalk.

step 2.1algebra

Depends on

Used by

Dependency tree · two levels

14 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