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.
O(-1) has no global generator
Counterexample
Assume the Axiom of Choice (The Axiom of Choice). Let be a field and let be the twisting sheaf on (Invertible twists for degree-one generated rings, Projective space is Proj of a polynomial ring). Then so the evaluation morphism is the zero morphism, which is not surjective because is a nonzero sheaf. Hence is not globally generated (Global generation by the evaluation map), even though it is invertible.
Facts & Assumptions
Given: The Axiom of Choice, A field , the graded ring with , the scheme with charts , , and the sheaf .
with and ; the overlap is , and restriction of sections is the canonical localisation. (Projective space is Proj of a polynomial ring, Twisting sheaf on Proj)
On one has and on one has : in the localisation, and are units of degree , with . (Twisting sheaf on Proj)
is invertible, in particular nonzero on the nonempty scheme : its restriction to is free of rank one with frame . (Invertible twists for degree-one generated rings)
A global section of a sheaf on is exactly a pair of chartwise sections on and whose restrictions to agree; the global section is zero exactly when both chartwise sections are zero. (Twisting sheaf on Proj)
A sheaf is globally generated if the evaluation morphism is surjective; the zero morphism out of a zero module is not surjective onto a sheaf with a nonzero stalk. (Global generation by the evaluation map)
The Axiom of Choice is the choice-function principle (The Axiom of Choice). It licenses the AC-qualified supplier used at step 1.1.
Refutation
A global section has two chart expressions. Let . Under the AC premise [F6], by [F2] its restriction to has the form with , and its restriction to has the form with ; these are finite polynomials and with .
Agreement on the overlap. By [F4] the two expressions agree on , where is invertible. Substituting turns the agreement into the identity in . The right-hand side is a finite sum of monomials with , so it involves only strictly positive powers of ; the left-hand side involves only nonpositive powers of . Comparing coefficients in the basis of gives for all and for all .
Vanishing of all global sections. By step 1.1 every global section is given by its two chart expressions, and by step 1.2 those expressions have and ; hence and , so by [F4]. Therefore .
Failure of global generation. With the evaluation morphism of [F5] is the zero morphism; since is invertible and , it has a nonzero stalk at every point and the zero morphism is not surjective. Hence is not globally generated, although it is invertible by [F3]. This is the standard contrast with the positive twists: is generated by its two coordinate sections . [F3, F5, step 2.1] \qed
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
18 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, 29 August 2022, Sections 4.5, 7.4, 9.3, 10.6, 17.4, 17.6, 18.2 (standard reference, not scraped)
- Gao-Zhang, Lectures on Algebraic Geometry, Chapter 5 (standard reference, not scraped)