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.
Global sections need not preserve surjections
Statement refuted
If is an epimorphism of sheaves of abelian groups on a space , then the induced map on global sections
is always surjective.
Facts & Assumptions
Given: The circle .
Global sections need not preserve epimorphisms in general (Global sections are left exact but need not preserve epimorphisms).
Counterexample
Let be the sheaf of continuous real-valued functions on , and let be the subsheaf of locally constant integer-valued functions. Let be the sheafification of the presheaf quotient . Every germ of is represented locally by a continuous function, so the canonical map is locally surjective and hence an epimorphism of sheaves.
Cover the circle by the two arcs and . Choose continuous angle functions and with . Their quotient classes agree on , because the difference is locally constant integer-valued there. Thus they glue to a section . If came from a global continuous real function , then would be an integer-valued continuous function on the connected set , hence constant. On the two connected components of this would force the same constant difference to be both and , which is impossible. So is not surjective.
Therefore an epimorphism of sheaves can fail to become surjective on global sections. This is exactly the phenomenon asserted in [F1], so the statement is refuted.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
4 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
- Ravi Vakil, The Rising Sea, Exercise 2.6.F (standard reference, not scraped)
- The Stacks Project, Section 17.3 (standard reference, not scraped)