The top degree keeps exactly one block

Cech/Vanishing.lean closes every degree strictly between the two ends, and it does so by contracting every block: cechPrimitive needs a cone point i₀ ∉ F for each block F, and below the top the only block without one — the full block F = univ — is unreachable, because a tuple of length n + 2 supports at most n + 2 variables and so cannot contain all of them.

At the top degree that counting argument runs out: a tuple can meet every variable, and the full block is exactly what survives. This file separates the surviving block from the rest.

The splitting

cechFace_cechBlockProj says the differential preserves every block, so a cocycle splits into its full-block part and the remainder, each again a cocycle. The remainder carries no full block at all, and cechPrimitive_isPrimitive — whose block hypothesis constrains only the cochain handed to it, rather than every term — contracts it. So the two differ by a coboundary, which is exists_fullBlock_add_coboundary: every class is carried by the full block.

Nothing here is about the top degree specifically; the statement holds in every degree, and it is only at the top that it says anything the vanishing theorem does not already say better.

What is not here

Finiteness. The full block of one term is spanned by the monomial fractions whose Laurent exponent is negative in every variable and has total degree d, a finite set by finite_setOf_degree_eq_of_neg — but turning that into Module.Finite k needs the base-field action, and the interface it has to meet is cechCohomologyModule through module_finite_linearCoherentH_of_cech. That is #666's remaining half, and none of it is claimed here.

Scope

Fintype ι is genuine here — Finset.univ is the full block — and this is the statement in the lane the issue means when it says finiteness of the variable set enters at the top.

noncomputable def AlgebraicGeometry.Proj.intCechFullBlock (ι k : Type u) [Field k] [Fintype ι] (d : ℤ) {m : ℕ} (s : (x : Fin (m + 1) → ι) → ↥(MvPolynomial.polynomialVariableIntCechTerm ι k d m x)) (y : Fin (m + 1) → ι) : ↥(MvPolynomial.polynomialVariableIntCechTerm ι k d m y)

The full-block part of a Čech cochain, index by index.

Equations

• AlgebraicGeometry.Proj.intCechFullBlock ι k d s y = (MvPolynomial.cechBlockProj ι k ⋯ y Finset.univ) (s y)

theorem AlgebraicGeometry.Proj.intCechFullBlock_cocycle (ι k : Type u) [Field k] [Fintype ι] (d : ℤ) {m : ℕ} (s : (x : Fin (m + 1) → ι) → ↥(MvPolynomial.polynomialVariableIntCechTerm ι k d m x)) (hs : ∀ (x : Fin (m + 2) → ι), ∑ j : Fin (m + 2), (-1) ^ ↑j • (MvPolynomial.cechFace ι k (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d) x j) (s (x ∘ j.succAbove)) = 0) (x : Fin (m + 2) → ι) : ∑ j : Fin (m + 2), (-1) ^ ↑j • (MvPolynomial.cechFace ι k (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d) x j) (intCechFullBlock ι k d s (x ∘ j.succAbove)) = 0

The full-block part of a cocycle is a cocycle: the faces commute with the projections.

theorem AlgebraicGeometry.Proj.exists_fullBlock_add_coboundary (ι k : Type u) [Field k] [Fintype ι] (d : ℤ) {n : ℕ} (s : (x : Fin (n + 2) → ι) → ↥(MvPolynomial.polynomialVariableIntCechTerm ι k d (n + 1) x)) (hs : ∀ (x : Fin (n + 3) → ι), ∑ j : Fin (n + 3), (-1) ^ ↑j • (MvPolynomial.cechFace ι k (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d) x j) (s (x ∘ j.succAbove)) = 0) : ∃ (p : (y : Fin (n + 1) → ι) → ↥(MvPolynomial.polynomialVariableIntCechTerm ι k d n y)), ∀ (x : Fin (n + 2) → ι), s x = intCechFullBlock ι k d s x + ∑ j : Fin (n + 2), (-1) ^ ↑j • (MvPolynomial.cechFace ι k (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d) x j) (p (x ∘ j.succAbove))

Every class is carried by the full block.

Splitting a cocycle into its full block and the rest leaves a cocycle that misses the full block outright, and cechPrimitive_isPrimitive — whose block hypothesis constrains only the cochain handed to it — contracts that remainder. So the two differ by a coboundary.