Hⁱ(Pⁿ, O(d)) is finite-dimensional in every positive degree

Cech/Vanishing.lean kills every degree whose tuples are too short to meet all the variables, by contracting every Laurent block. The top degree is exactly where that fails, and Cech/TopDegree.lean separates the surviving block instead: every class is carried by the full block. Algebra/MvPolynomial/Cech/Finite.lean shows those full blocks form a finite-dimensional k-space. This file joins the algebraic result to the geometric Čech complex and discharges the finiteness interface.

The argument

intCechBlockCocycles is the space of full-block cocycles of a degree — a submodule of the finite-dimensional space of full-block cochains, hence finite-dimensional. intCechBlockClass sends such a cocycle to its cohomology class, and the two halves are:

• intCechBlockSmul_comp_class — the class map is k-linear. The action on cohomology is the map a sheaf endomorphism induces, so this is homologyπ naturality once the cycle map is known to intertwine the actions, which is intCechCochainsDegreewiseAddEquiv_smul from the file below;
• intCechBlockClass_surjective — it is onto. exists_fullBlock_add_coboundary splits a cocycle into its full block and a coboundary; the full block is again a cocycle and lands in cechBlockSpan, and the coboundary dies in homology by toCycles_comp_homologyπ.

Module.Finite.of_surjective then gives finiteness on the Čech side, and module_finite_linearCoherentH_of_cech carries it to the group the interface names.

Two spellings that have to be pinned

cechCohomologyFunctor takes its space as an implicit argument, and cechCohomologyModule supplies the module instance at whatever spelling its U was elaborated with. Writing the chart family as polynomialVariableChart ι k fixes that space to ProjectiveSpectrum.top _, while the finiteness interface asks for Y; the two are definitionally equal, so the instance is inhabited, and not reducibly so, so instance search never finds it. intChart and intTwistModules are the same objects presented at the variety, and they exist only to make the one instance search meets be the one that is there. This is the transparency rule of .claude/references/instance-transparency.md, technique 5.

The same effect appears twice more, and is handled the same way: the AddCommGroup, Module and Module.Finite instances on intCechBlockCocycles are named rather than searched for, because it is a submodule of a product of submodules and search will not assemble that on its own.

Scope

Positive degrees only. exists_fullBlock_add_coboundary splits a cocycle in degree n + 1, and the splitting is useful because the remainder is a coboundary — which needs a degree below. Degree 0 has none, and H⁰ is not a subquotient but the module of global sections outright; its finiteness is the finite-dimensionality of a graded piece of the polynomial ring and is a separate argument. So Hⁿ(Pⁿ, O(d)) is covered for every n ≥ 1, at either sign of d, and P⁰ is not.

theorem AlgebraicGeometry.Proj.intCechCochainsDegreewiseAddEquiv_symm_smul (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (r : k) (s : MvPolynomial.polynomialVariableIntCechCochains ι k d n) : (intCechCochainsDegreewiseAddEquiv ι k d n).symm (r • s) = (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.cechComplexFunctor (polynomialVariableChart ι k)).map (intTwistScalarHom ι k d r)).f n)) ((intCechCochainsDegreewiseAddEquiv ι k d n).symm s)

theorem AlgebraicGeometry.Proj.intCech_d_apply_eq_zero_iff (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (t : ↑((intCechComplexOfTwist ι k d).X n)) : (CategoryTheory.ConcreteCategory.hom ((intCechComplexOfTwist ι k d).d n (n + 1))) t = 0 ↔ ∀ (x : Fin (n + 2) → ι), ∑ j : Fin (n + 2), (-1) ^ ↑j • (MvPolynomial.cechFace ι k (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d) x j) ((intCechCochainsDegreewiseAddEquiv ι k d n) t (x ∘ j.succAbove)) = 0

The abstract cocycle condition, read as the explicit alternating sum.

noncomputable def AlgebraicGeometry.Proj.intCechBlockIncl (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : ((x : Fin (n + 1) → ι) → ↥(MvPolynomial.cechBlockSpan ι k (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d) d x)) →ₗ[k] MvPolynomial.polynomialVariableIntCechCochains ι k d n

The full blocks of a Čech degree, included into all cochains.

No finiteness of ι is needed: cechBlockSpan is defined without it, and only its finite generation is not.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.intCechBlockD (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : ((x : Fin (n + 1) → ι) → ↥(MvPolynomial.cechBlockSpan ι k (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d) d x)) →ₗ[k] MvPolynomial.polynomialVariableIntCechCochains ι k d (n + 1)

The Čech differential, read on full-block cochains through the degreewise comparison.

k-linearity is not assumed of the explicit differential: it is intCechCochainsDegreewiseAddEquiv linearity on both sides of the chain-map square that the scalar endomorphism satisfies.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.intCechBlockCocycles (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : Submodule k ((x : Fin (n + 1) → ι) → ↥(MvPolynomial.cechBlockSpan ι k (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d) d x))

The full-block cocycles of a Čech degree.

Equations

• AlgebraicGeometry.Proj.intCechBlockCocycles ι k d n = (AlgebraicGeometry.Proj.intCechBlockD ι k d n).ker

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Proj.addCommGroupIntCechBlockCocycles (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : AddCommGroup ↥(intCechBlockCocycles ι k d n)

Equations

• AlgebraicGeometry.Proj.addCommGroupIntCechBlockCocycles ι k d n = (AlgebraicGeometry.Proj.intCechBlockCocycles ι k d n).addCommGroup

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Proj.moduleIntCechBlockCocycles (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : Module k ↥(intCechBlockCocycles ι k d n)

Equations

• AlgebraicGeometry.Proj.moduleIntCechBlockCocycles ι k d n = (AlgebraicGeometry.Proj.intCechBlockCocycles ι k d n).module

instance AlgebraicGeometry.Proj.module_finite_intCechBlockCocycles (ι k : Type u) [Field k] [Fintype ι] (d : ℤ) (n : ℕ) : Module.Finite k ↥(intCechBlockCocycles ι k d n)

noncomputable def AlgebraicGeometry.Proj.intCechBlockCocycleHom (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : AddCommGrpCat.of ↥(intCechBlockCocycles ι k d n) ⟶ (intCechComplexOfTwist ι k d).X n

A full-block cocycle, as a map of abelian groups into the Čech cochains.

Built as a composite of maps that already exist, so map_add and map_zero come for free.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.intCechBlockCocycleHom_apply (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (b : ↥(intCechBlockCocycles ι k d n)) : (CategoryTheory.ConcreteCategory.hom (intCechBlockCocycleHom ι k d n)) b = (intCechCochainsDegreewiseAddEquiv ι k d n).symm ((intCechBlockIncl ι k d n) ↑b)

theorem AlgebraicGeometry.Proj.intCechBlockCocycleHom_comp_d (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : CategoryTheory.CategoryStruct.comp (intCechBlockCocycleHom ι k d n) ((intCechComplexOfTwist ι k d).d n (n + 1)) = 0

noncomputable def AlgebraicGeometry.Proj.intCechBlockCycle (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : AddCommGrpCat.of ↥(intCechBlockCocycles ι k d n) ⟶ HomologicalComplex.cycles (intCechComplexOfTwist ι k d) n

The cycle a full-block cocycle determines.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.intCechBlockCycle_i (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : CategoryTheory.CategoryStruct.comp (intCechBlockCycle ι k d n) (HomologicalComplex.iCycles (intCechComplexOfTwist ι k d) n) = intCechBlockCocycleHom ι k d n

noncomputable def AlgebraicGeometry.Proj.intCechBlockClass (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : AddCommGrpCat.of ↥(intCechBlockCocycles ι k d n) ⟶ HomologicalComplex.homology (intCechComplexOfTwist ι k d) n

The class of a full-block cocycle in Čech cohomology.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.intCechBlockSmul (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (r : k) : AddCommGrpCat.of ↥(intCechBlockCocycles ι k d n) ⟶ AddCommGrpCat.of ↥(intCechBlockCocycles ι k d n)

Scalar multiplication on the full-block cocycles, as a map of abelian groups.

Equations

• AlgebraicGeometry.Proj.intCechBlockSmul ι k d n r = AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↥(AlgebraicGeometry.Proj.intCechBlockCocycles ι k d n)) r)

theorem AlgebraicGeometry.Proj.intCechBlockSmul_comp_cocycleHom (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (r : k) : CategoryTheory.CategoryStruct.comp (intCechBlockSmul ι k d n r) (intCechBlockCocycleHom ι k d n) = CategoryTheory.CategoryStruct.comp (intCechBlockCocycleHom ι k d n) (((CategoryTheory.cechComplexFunctor (polynomialVariableChart ι k)).map (intTwistScalarHom ι k d r)).f n)

theorem AlgebraicGeometry.Proj.intCechBlockSmul_comp_cycle (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (r : k) : CategoryTheory.CategoryStruct.comp (intCechBlockSmul ι k d n r) (intCechBlockCycle ι k d n) = CategoryTheory.CategoryStruct.comp (intCechBlockCycle ι k d n) (HomologicalComplex.cyclesMap ((CategoryTheory.cechComplexFunctor (polynomialVariableChart ι k)).map (intTwistScalarHom ι k d r)) n)

The cycle a full-block cocycle determines intertwines the two scalar actions.

set_option maxHeartbeats 1000000 in Reduced to iCycles by monomorphism, where it is intCechBlockSmul_comp_cocycleHom.

theorem AlgebraicGeometry.Proj.intCechBlockSmul_comp_class (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (r : k) : CategoryTheory.CategoryStruct.comp (intCechBlockSmul ι k d n r) (intCechBlockClass ι k d n) = CategoryTheory.CategoryStruct.comp (intCechBlockClass ι k d n) (HomologicalComplex.homologyMap ((CategoryTheory.cechComplexFunctor (polynomialVariableChart ι k)).map (intTwistScalarHom ι k d r)) n)

The class map is k-linear.

set_option maxHeartbeats 1000000 in The action on cohomology is the map the sheaf endomorphism induces, so this is homologyπ naturality once the cycle map is known to intertwine the actions.

theorem AlgebraicGeometry.Proj.intCechBlockClass_surjective (ι k : Type u) [Field k] [Fintype ι] (d : ℤ) (n : ℕ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (intCechBlockClass ι k d (n + 1)))

Every class is the class of a full-block cocycle.

exists_fullBlock_add_coboundary splits a cocycle into its full block and a coboundary; the full block is again a cocycle and lies in cechBlockSpan, and the coboundary dies in homology.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Proj.intTwistModules (ι k : Type u) [Field k] (d : ℤ) : (Proj (MvPolynomial.polynomialGrading ι k)).Modules

The twist O(d) as a sheaf of modules on projective space as a variety.

The type ascription is the point: associatedSheaf lands in (Proj 𝒜).Modules, and the finiteness interface asks for Y.Modules. Those are the same term, but only the second spelling lets cechCohomologyModule's instance be found.

Equations

• AlgebraicGeometry.Proj.intTwistModules ι k d = AlgebraicGeometry.Proj.associatedSheaf (MvPolynomial.polynomialGrading ι k) (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Proj.intChart (ι k : Type u) [Field k] : ι → TopologicalSpace.Opens ↥(Proj (MvPolynomial.polynomialGrading ι k))

The variable charts, typed as opens of the variety.

Same ascription trick as intTwistModules: cechCohomologyFunctor takes its space as an implicit argument, so the chart family has to be presented at Y for the module instance cechCohomologyModule supplies to be the one instance search meets.

Equations

• AlgebraicGeometry.Proj.intChart ι k = AlgebraicGeometry.Proj.polynomialVariableChart ι k

noncomputable def AlgebraicGeometry.Proj.intCechBlockClassLinear (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : ↥(intCechBlockCocycles ι k d (n + 1)) →ₗ[k] ↑((Cohomology.cechCohomologyFunctor (intChart ι k) (n + 1)).obj ((Scheme.Modules.toSheaf (Proj (MvPolynomial.polynomialGrading ι k))).obj (intTwistModules ι k d)))

The class map, as a k-linear map into Čech cohomology.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.module_finite_cechCohomology_intTwist (ι k : Type u) [Field k] [Fintype ι] (d : ℤ) (n : ℕ) : Module.Finite k ↑((Cohomology.cechCohomologyFunctor (intChart ι k) (n + 1)).obj ((Scheme.Modules.toSheaf (Proj (MvPolynomial.polynomialGrading ι k))).obj (intTwistModules ι k d)))

Hⁿ⁺¹ of an integer twist is finite-dimensional, on the Čech side.

theorem AlgebraicGeometry.Proj.module_finite_linearCoherentH_projectiveSpaceTwist (ι k : Type u) [Field k] [Fintype ι] (d : ℤ) (n : ℕ) : Module.Finite k ↑((Cohomology.linearCoherentH k (Proj (MvPolynomial.polynomialGrading ι k)) (n + 1)).obj (projectiveSpaceTwist ι k d))

Hⁿ⁺¹(Pⁿ, O(d)) is a finite-dimensional k-vector space.

The interface group is linearCoherentH, and the finite spanning set lives on the Čech side; module_finite_linearCoherentH_of_cech carries it across, and it is the k-linearity of the comparison that makes the transfer legitimate.

set_option maxHeartbeats 1000000 in The injective resolution is chosen rather than supplied: the site of opens is small, so canonicalInjectiveResolution produces one. The HasExt witness is instantiated at HasExt.standard _, which is the reconciliation module_finite_linearCoherentH_of_cech's docstring describes.