Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge 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.

Fibre of a module sheaf at a point

Definition

Let X be a locally ringed space, let F be an OX-module in the sense of Modules on a ringed space, and let x∈X. Write Fx for the stalk of F at x (The stalk of a presheaf at a point); it is a module over the local ring OX,x, and the residue field is κ(x)=OX,x/mx with maximal ideal mx⊆OX,x (The residue field at a point of an affine scheme). The fibre of F at x is the tensor product of modules over the ring OX,x (The tensor product M⊗RN from the additive group underlying the free Z-module on M×N, elementary tensors, and finite tensor sums) F(x):=Fx⊗OX,xκ(x). The tensor product carries the κ(x)-module structure induced by the scalar action on the second factor, so F(x) is a vector space over the residue field κ(x).

Right exactness of the tensor product (Tensoring is right exact) applied to the exact sequence mx↪OX,x↠κ(x) identifies this vector space with the quotient of the stalk by the submodule mxFx: F(x)  ≅  Fx/mxFx,m⊗λˉ  ⟼  λm mod mxFx.

The fibre and the stalk are different objects: Fx is a module over the local ring OX,x and need not be a vector space, while F(x) is a vector space over κ(x) equipped with a canonical surjection Fx↠F(x). For the zero module F=0 one has Fx=0 and F(x)=0 at every point; for F=OX one has OX(x)=κ(x) at every point. The construction is functorial: a morphism F→G of OX-modules induces a κ(x)-linear map F(x)→G(x) for every x∈X, and restriction to an open U⊆X gives (F∣U)(x)=F(x) for x∈U.

Depends on

Used by

Dependency tree · two levels

25 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