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.
Support of a section of a sheaf
Definition
Let be a topological space, let be a presheaf of -vector spaces (or of abelian groups) on (A presheaf on a topological space), let be open and let . The support of is where denotes the germ of at in the stalk (The stalk of a presheaf at a point, Germs of sections). A section is compactly supported when its support is a compact subspace of (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right). For a subspace and a presheaf on , the support of is defined by the same condition using the stalks of . The support is not assumed closed in nor compact.
When is a sheaf of abelian groups (in particular of -vector spaces) the following three consistency facts hold; they are immediate consequences of the definitions above and are recorded here because every later compact-support statement uses them.
- is closed in . Indeed, if then in the stalk; equality of germs means that and the zero section agree on some open neighbourhood of (Germs of sections), so vanishes on the open neighbourhood of , and is therefore open in .
- if and only if . If every germ of is zero then by the locality axiom of a sheaf applied to the cover of by its open subsets (A section of a sheaf of groups is zero exactly when all of its germs are zero); the converse is immediate, since the zero section has zero germ at every point.
- for every open . Restriction is compatible with the germ maps, so for every (Germs of sections).
For a sheaf, a section whose support is contained in a compact subset is compactly supported: its support is closed in by fact 1, hence compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact). For a global section (), this applies to any compact subset of . For a local section, containment in a compact subset of alone does not suffice: the constant nonzero section of the constant sheaf (The constant sheaf is the sheaf of locally constant functions) on has support , which is not compact although it is contained in the compact (A subset of with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology, ). The open cover of has no finite subcover. No choice principle is used: germs, stalks, supports and restrictions are elementary.
Remarks
- For a sheaf of abelian groups and sections one has and : if both germs vanish at then and vanish on a common open neighbourhood of , hence so does , and if vanishes on a neighbourhood of then so does . These inclusion facts are used silently in the patching arguments of the compact-support calculus.
Depends on
A presheaf on a topological space
The stalk of a presheaf at a point
Germs of sections
A section of a sheaf of groups is zero exactly when all of its germs are zero
Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right
A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact
A subset of with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology
The constant sheaf is the sheaf of locally constant functions