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.
The image sheaf is the sheafification of the presheaf image
Statement
Let be a morphism of sheaves of sets on a topological space , and let be the presheaf image Define the image sheaf by Then is a subsheaf of , factors through , and the canonical map is an isomorphism. In particular, the image sheaf is the sheafification of the objectwise image presheaf.
Facts & Assumptions
Given: A morphism of sheaves .
A subsheaf is a sheaf whose sections embed objectwise into the ambient sheaf (Subsheaves).
A morphism of presheaves is a compatible family of component maps (Morphisms of presheaves).
Maps from a presheaf to a sheaf factor uniquely through sheafification (Sheafification is left adjoint to the inclusion of sheaves into presheaves).
Proof
The assignment is a subpresheaf of : if and , then by [F2].
The assignment is a subsheaf of . Indeed, restriction clearly preserves local representability. If sections on an open cover of agree on overlaps, then because is a sheaf they glue to a unique . The local witnesses for each also witness that lies in . Thus is a sheaf, and [F1] makes it a subsheaf. The factorization is immediate from the definition of .
Since maps into the sheaf , [L1] gives a unique morphism extending the inclusion .
Conversely, let . Choose an open cover and sections with . Then the sections are compatible on overlaps because they all come from . Hence they define a section by the very construction of sheafification. These assignments are compatible with restriction, so they define a morphism .
The composites and are identities, because both are identities locally on the chosen image sections that generate and , and both targets are sheaves. Therefore is an isomorphism.