O(-N) is the tensor inverse of O(N), and Serre's surjection ⊕ O(-N) ↠ F #
The L = O(N) case of #806, and with it the literal deliverable of #586.
The inverse is four isomorphisms #
twistingSheafTensorAddIso gives O(N) ⊗ O(-N) ≅ O(N + -N); the index is 0; O(0) is the
associated sheaf of 𝒜 over itself (twistingSheafZeroIso); and that is the unit
(associatedSheafSelfIso). twistingSheafTensorNegIso is the composite. As #806 records, this
composite did not typecheck before #821 put both factors in one graded setting; it does now, and
nothing about it is specific to the sign of N.
Untwisting an arbitrary F #
tensorTwistNegIso : (F ⊗ O(N)) ⊗ O(-N) ≅ F is the associator, the inverse above under F ⊗ -,
and the right unitor. F is arbitrary -- TensorTwist.lean's warning about F(d)(e) ≅ F(d+e)
concerned an associator that then carried invertibility hypotheses; tensorAssocIso no longer
does, so the only invertible factors needed are the two twists, and they are invertible.
From free I ↠ F(N) to ⊕ O(-N) ↠ F #
exists_epi_free_tensorTwist produces p : free I ↠ F ⊗ O(N). Tensoring by O(-N) on the left
keeps it an epimorphism (epi_tensorHom_id_of_invertible), the symmetry and tensorTwistNegIso
carry the target to F, and tensorLeftFreeIso identifies the source with ∐ O(-N). That is
Hartshorne II.5.17 in the form #586 states: every coherent F on Proj 𝒜 is a quotient of a
finite direct sum of copies of one O(-N).
Its specialization to projective space and lift to a coherent short exact sequence is
exists_shortExact_coproduct_twist in Cohomology/Finiteness/Projective.lean, completing the
parent issue #570.
What is not here #
The general IsInvertible L → ∃ L', L ⊗ L' ≅ unit, which still needs the per-chart
trivializations glued. For an explicit LineBundleData, the formerly blocked hom-equivalence
Hom(L ⊗ M, N) ≃ Hom(M, L⁻¹ ⊗ N) now lives at LineBundleData.tensorLeftHomEquiv:
associator naturality is available from the monoidal structure. Its scalar-linear refinement
lives downstream at LineBundleData.tensorLeftHomLinearEquiv.
O(N) ⊗ O(-N) ≅ O. The tensor inverse of the twisting sheaf, for degree-one generated
𝒜: the twist-addition isomorphism at N + -N = 0, then the identification of O(0) with the
unit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The twisting sheaf with its opposite twist as a chosen tensor inverse.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The projective twisting-sheaf specialization of the line-bundle Hom/sections comparison:
Hom(O(N), F) ≃ Γ(O(-N) ⊗ F).
This file records the categorical equivalence at the neutral line-bundle layer. The generic
scalar-linear refinement is LineBundleData.lineHomTopLinearEquivOver, and the projective
Hom-finiteness reduction using it lives in Cohomology.Finiteness.Hom.
Equations
Instances For
Untwisting: (F ⊗ O(N)) ⊗ O(-N) ≅ F, for an arbitrary module sheaf F.
The associator, the inverse of O(N) under F ⊗ -, and the right unitor. This is the
isomorphism GlobalGeneration.lean records as the gap between free I ↠ F(N) and
⊕ O(-N) ↠ F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Serre's theorem: a coherent sheaf on Proj 𝒜 is a quotient of a finite direct sum of
copies of O(-N), for 𝒜 generated over 𝒜 0 by finitely many degree-one elements.
Hartshorne II.5.17 / EGA II 2.7.9 in the form #586 states. The surjection is
exists_epi_free_tensorTwist's free I ↠ F ⊗ O(N) tensored by O(-N), untwisted by
tensorTwistNegIso, and read on ∐ O(-N) through tensorLeftFreeIso. No global-generation or
resolution hypothesis, and no instance supplies the surjection. The exponent can be pushed above
any N₀; the dévissage on Pⁿ takes N ≥ 1 so that H⁰(O(-N)) = 0.
Serre's theorem in the ∐ O(-N) ↠ F form, with the exponent unconstrained.