H⁰(Pⁿ, O(d)) = 0 for a negative twist #
The degree-zero end of the integer-twist computation. Cech/Vanishing.lean closes the middle
degrees at either sign; this file closes the bottom one at d < 0.
The argument #
H⁰ of the Čech complex is the kernel of d⁰, and unfolding the differential at n = 0 says a
cocycle is a family (sᵢ) of degree-d fractions on the variable charts agreeing on every
overlap. Fixing i and choosing any j ≠ i, the overlap condition clears denominators to
X_j ^ b * p = X_i ^ a * q
with p the numerator of sᵢ. X_i and X_j are distinct variables, hence coprime, so
X_pow_dvd_of_cross_mul extracts X_i ^ a ∣ p. The numerator of a degree-d fraction with
denominator X_i ^ a is homogeneous of degree a + d, and at d < 0 that is smaller than a
— so a nonzero p would be a multiple of X_i ^ a of degree below a, which cannot happen.
Hence p = 0, hence sᵢ = 0.
Where the sign enters, and where it does not #
Only in the last step. Everything before it is the two-chart argument that
polynomialToNatGlobalSections_surjective runs for d : ℕ, and it is insensitive to the sign;
what changes is the conclusion drawn at the end, which for d ≥ 0 produces a representing
polynomial and for d < 0 produces 0.
The sign is spent in a single inequality. A fraction with denominator X_i ^ a has numerator
homogeneous of degree a + d, so d < 0 reads a + d < a, and
MvPolynomial.eq_zero_of_X_pow_dvd_of_isHomogeneous_of_lt closes.
GradedModule.intShiftPiece_eq_bot_of_neg states the neighbouring fact — intShift is
ℕ-indexed, so a piece whose degree n + d is negative is trivial outright — and is deliberately
not on that path: the cross equation kills the numerator while its degree is still a natural
number. It is what makes the ℕ-indexing of intShift legible, and nothing below depends on it.
Scope #
The abelian-group statement, per #665. The k-vector-space structure that
FiniteDimensionalCohomology.finite asks for is separate, and the comparison AddEquiv is not
assumed k-linear anywhere here.
Nontrivial ι is needed and is not cosmetic: with a single variable there is no second chart, the
overlap condition is vacuous, and the statement is false — P⁰ is a point and O(d) is free on
it. Fintype ι is not needed; the argument uses two charts, never all of them.
The two-chart step #
The overlap condition on two charts, once denominators are cleared, is exactly the cross
equation imported from Algebra/MvPolynomial/DivMonomial. That algebraic lemma is the
mathematical heart of the negative-twist vanishing; everything below is the geometric plumbing
that produces the cross equation from a Čech cocycle.
Reducing H⁰ to the kernel #
Degree 0 has no incoming differential, so the general exactAt machinery the middle degrees use
still applies — but it degenerates. (ComplexShape.up ℕ).prev 0 = 0 and d 0 0 = 0 by the shape,
so exactness at 0 says precisely that the kernel of d⁰ is trivial, with no image to quotient
by. Separating this out keeps the algebra below free of homological bookkeeping.
Triviality of ker d⁰ is exactly vanishing of H⁰ for the algebraic Čech complex.
From a Čech cocycle to the cross equation #
The Čech differential in degree zero is s ↦ (x ↦ face x 0 (s _) - face x 1 (s _)), so a cocycle
says the two charts of any pair agree after both are pushed to the overlap. faceMap_mk writes
each push explicitly — clearing X_i ^ a costs X_j ^ a in numerator and denominator — and
mk_eq_mk_iff then clears the localization outright. What is left is an equation in the polynomial
ring, and cancelling the common factor leaves exactly the cross equation
num_eq_zero_of_cross_of_neg consumes.
The overlap condition on the two charts of a Čech index, cleared of denominators.
x is a two-element Čech index; its faces are the single-chart indices, carrying cj on the
x 1-chart and ci on the x 0-chart. The hypothesis is that the two agree on the overlap,
which is the degree-zero cocycle condition at that index, and hij is what makes it say anything.
The denominators are X_(x 0) ^ a, X_(x 1) ^ b and (X_(x 0) X_(x 1)) ^ n; mk_eq_mk_iff
supplies the equation multiplied through by some u ∈ Submonoid.powers (X_(x 0) X_(x 1)), and
MvPolynomial ι k is a domain, so u and the common factor X_(x 0) ^ b X_(x 1) ^ a both
cancel.
The x 0-chart component of a degree-zero cocycle vanishes, in the localization rather than
in its numerator. Choosing representatives is all that separates this from
num_eq_zero_of_intCechFace_eq_of_neg.
The cocycle condition, chart by chart #
Only two charts are ever used, so Nontrivial ι is the whole hypothesis: a second variable has to
exist for the overlap condition to say anything. With one variable it is vacuous, and the statement
below is false rather than merely unproved.
A degree-zero cocycle of the integer-twist Čech complex vanishes when d < 0.
Each component is read off its own two-element index ![y 0, j], so the choice of j is local to
the component and no compatible choice across all of ι is needed.
H⁰ of the algebraic Čech complex vanishes at a negative twist.
H⁰(Pⁿ, O(d)) = 0 for d < 0.
The abelian-group statement of #665. Nontrivial ι is the only hypothesis on the variable set:
the argument compares two charts and never enumerates them, so no finiteness is needed, and at one
variable the statement is false rather than merely unproved.