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.
Flasque sheaf
Definition
Let be a topological space and let be a sheaf of abelian groups on (A sheaf on a topological space, Sheaves of abelian groups, and likewise sheaves of modules on a ringed space, form abelian categories). For open subsets write for the restriction map of (Sections, restrictions, and global sections of a presheaf).
Then is flasque, also called flabby, when each of these restriction maps is surjective: for all open the map is onto. Equivalently, is flasque when every section of over an open subset extends to every larger open subset , that is, when for every there is with .
The same condition on restriction maps defines flasque sheaves of sets and flasque sheaves of modules over a sheaf of rings; on this page the notion is used for sheaves of abelian groups.