Hⁿ(Pⁿ, O(d)) = 0 for n ≥ 1 and d ≥ 0 #
The headline of #340. Everything difficult happened earlier: the block decomposition, the
contracting homotopy, and the cochain-level computation cechPrimitive_isPrimitive that every
positive-degree cocycle of the variable Čech complex is a coboundary. This file only converts:
the cochain statement becomes exactness of the algebraic Čech complex through
ShortComplex.ab_exact_iff and polynomialVariableCechComplex_d_apply, exactness becomes
vanishing homology, and vanishing homology becomes the vanishing of Hⁿ(Pⁿ, O(d)) through the
comparison polynomialVariableCechComplex_computesCohomology of #495.
The H⁰ companion is not restated here: degree-zero global sections of O(d) are the
degree-d homogeneous polynomials by polynomialTwistingGlobalSectionsModuleIso, which
remains the canonical statement and is deliberately not reproved.
The HasExt witness is passed positionally, as everywhere in this lane: Sheaf.H lands in
the HasExt universe, and letting instance search pick would allow the small-site
HasExt.{u} to name different groups.
Tags #
Čech cohomology, projective space, twisting sheaf, vanishing
The algebraic Čech complex of O(d) is exact in every positive degree. This is the
cochain-level homotopy computation cechPrimitive_isPrimitive, read through the coordinate
formula for the differential.
The homology of the algebraic Čech complex vanishes in every positive degree.
Hⁿ(Pⁿ, O(d)) = 0 for n ≥ 1 and d ≥ 0, stated as the triviality of the derived
sections group. The twist is a natural number, which is the whole of the d ≥ 0 hypothesis;
the projective space is Proj of a polynomial ring in an arbitrary — possibly infinite —
variable set over a field.
Twists of either sign, below the top degree #
The nonnegative statements above vanish in every positive degree, because a nonnegative twist makes the block of all variables empty outright. At a negative twist that block is not empty — it is exactly where the top cohomology lives — so the same contracting homotopy closes only the degrees whose tuples are too short to meet every variable.
That is not a weakening of the argument but a sharpening of its hypothesis: cechPrimitive now
takes the vanishing of the full block as an input, and the two statements differ only in which
lemma discharges it. The consequence is the expected one — over Fintype.card ι = N + 1
variables, Hⁱ vanishes for 0 < i < N at either sign, and degree N is left open.
The algebraic Čech complex of an integer twist is exact below the top degree.
hcard is the whole of the difference from polynomialVariableCechComplex_exactAt: a cochain in
degree n + 1 is indexed by tuples of length n + 2, and once that is smaller than the number of
variables, cechBlockProj_eq_zero_of_card_lt supplies the vanishing of the full block that the
nonnegative case got from the degree of the twist. Nothing else changes, and in particular the
sign of d is never mentioned.
The homology of the integer-twist Čech complex vanishes below the top degree.
Hⁱ(Pⁿ, O(d)) = 0 for 0 < i < n and either sign of d.
With Fintype.card ι = n + 1 the hypothesis i + 1 < Fintype.card ι reads i < n, so this is
vanishing strictly between the two ends: H⁰ is the global sections and Hⁿ is the group the
dévissage of #332 consumes, and neither is claimed here.
The nonnegative companion polynomialTwisting_H_subsingleton is stronger where it applies — it
needs no finiteness and reaches every positive degree — and is not a corollary of this.