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.
Module sheaf on an affine scheme
Definition
Let be a commutative ring with , let be an -module, and put with its distinguished-open basis (The underlying space of an affine spectrum). For write for the localisation of at the multiplicative subset , as in Localisation of a module at a multiplicative subset. The distinguished-open data of assign
Restriction maps. Suppose . Then , so for some and some ; hence the image of in is a unit and is an -module. The localisation map is -linear, so the universal property of module localisation (Universal property of localisation for modules) gives a unique -linear map with .
Well-definedness. The map depends only on the pair of open sets: it is characterised as the unique -linear map compatible with the canonical maps from . Consequently , and for distinguished opens one has , because both sides are -linear maps that agree after composition with . Moreover, if then the maps and are mutually inverse; the two inclusions and are available, and the composition rule gives and . Thus the data are functorial on distinguished opens, canonically up to these identifications.
Module structure. On the structure sheaf has and the ring restriction for is the canonical localisation (Sections and restrictions on distinguished opens of an affine scheme). The map is -linear by construction, so the data form an -module on the distinguished-open basis: sections on are the -modules and restrictions are compatible with the ring restrictions.
Completion to a sheaf. A later result on this page proves that these distinguished-open data satisfy the sheaf conditions on the basis and extend uniquely to an -module, still denoted , whose sections on are the given modules ; the notation always refers to that -module.
Degenerate cases. For one has and , the localisation in which is inverted; this is the zero module. For a unit one has and . If then and is the zero sheaf on the empty space, whose module of sections on is . The construction is functorial in : an -linear map induces -linear maps commuting with all restriction maps.