Cohomological boundedness from a finite affine cover

The generic finite-cover boundedness theorem is applied to a compact scheme using affine vanishing and affine intersections.

noncomputable def AlgebraicGeometry.Cohomology.affineBasicOpenBasisAt {X : Scheme} (U : X.Opens) (hU : IsAffineOpen U) : CategoryTheory.Sheaf.CompactOpenBasis ↑X.toPresheafedSpace

The compact distinguished-open basis lying below one fixed affine open of a scheme.

Equations

• AlgebraicGeometry.Cohomology.affineBasicOpenBasisAt U hU = { carrier := Set.range X.basicOpen, isCompact := ⋯, finite_refinement := ⋯, inf_mem := ⋯ }

theorem AlgebraicGeometry.Cohomology.mem_affineBasicOpenBasisAt {X : Scheme} (U : X.Opens) (hU : IsAffineOpen U) : U ∈ (affineBasicOpenBasisAt U hU).carrier

The target affine open belongs to its own distinguished-open basis as D(1).

theorem AlgebraicGeometry.Cohomology.modulesSpec_isCechAcyclicOnCompactBasis {R : CommRingCat} (G : (Spec R).Modules) [SheafOfModules.IsQuasicoherent G] : CategoryTheory.Sheaf.IsCechAcyclicOnCompactBasis (affineBasicOpenBasis R) ((Scheme.Modules.toSheaf (Spec R)).obj G)

Quasi-coherent module sheaves on an affine spectrum are Cech-acyclic on its distinguished open basis.

theorem AlgebraicGeometry.Cohomology.modules_isCechAcyclicOn_affineBasicOpenBasisAt {X : Scheme} (G : X.Modules) [SheafOfModules.IsQuasicoherent G] (U : X.Opens) (hU : IsAffineOpen U) : CategoryTheory.Sheaf.IsCechAcyclicOnCompactBasis (affineBasicOpenBasisAt U hU) ((Scheme.Modules.toSheaf X).obj G)

The underlying abelian sheaf of a quasi-coherent module is Cech-acyclic on the local distinguished-open basis below an affine open.

theorem AlgebraicGeometry.Cohomology.modules_HPrime_subsingleton_of_isAffineOpen {X : Scheme} (G : X.Modules) [SheafOfModules.IsQuasicoherent G] (U : X.Opens) (hU : IsAffineOpen U) (n : ℕ) (hn : 0 < n) [hExt : CategoryTheory.HasExt (TopCat.Sheaf AddCommGrpCat ↑X.toPresheafedSpace)] : Subsingleton ↑(((Scheme.Modules.toSheaf X).obj G).H' n U)

Positive local cohomology of a quasi-coherent module vanishes on an affine open. The cohomology group here is the actual ambient Sheaf.H', not cohomology of an unrelated sheaf on an abstract affine model.

theorem AlgebraicGeometry.Cohomology.modules_intersectionAcyclic_of_forall_isAffineOpen {X : Scheme} (G : X.Modules) [SheafOfModules.IsQuasicoherent G] [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] [hExt : CategoryTheory.HasExt (TopCat.Sheaf AddCommGrpCat ↑X.toPresheafedSpace)] (L : List X.Opens) (hL : ∀ V ∈ L, IsAffineOpen V) : CategoryTheory.Sheaf.IntersectionAcyclic ((Scheme.Modules.toSheaf X).obj G) hExt L

If every member of a finite list of opens is affine and the diagonal is affine, then a quasi-coherent module is acyclic on every nonempty intersection generated by the list.

noncomputable def AlgebraicGeometry.Cohomology.finiteAffineCoverOpens (X : Scheme) [CompactSpace ↥X] : List X.Opens

A fixed nonempty finite affine cover used to state an explicit cohomological bound. The empty affine open is prepended so the list remains nonempty even for the empty scheme.

Equations

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

@[simp]

theorem AlgebraicGeometry.Cohomology.finiteAffineCoverOpens_ne_nil (X : Scheme) [CompactSpace ↥X] : finiteAffineCoverOpens X ≠ []

theorem AlgebraicGeometry.Cohomology.opensUnion_finiteAffineCoverOpens (X : Scheme) [CompactSpace ↥X] : CategoryTheory.Sheaf.opensUnion (finiteAffineCoverOpens X) = ⊤

The chosen finite list really covers the scheme.

theorem AlgebraicGeometry.Cohomology.isAffineOpen_of_mem_finiteAffineCoverOpens (X : Scheme) [CompactSpace ↥X] (U : X.Opens) (hU : U ∈ finiteAffineCoverOpens X) : IsAffineOpen U

Every member of the chosen finite cover is affine.

noncomputable def AlgebraicGeometry.Cohomology.cohomologicalBound (X : Scheme) [CompactSpace ↥X] : ℕ

The explicit finite-affine-cover bound.

Equations

• AlgebraicGeometry.Cohomology.cohomologicalBound X = (AlgebraicGeometry.Cohomology.finiteAffineCoverOpens X).length

theorem AlgebraicGeometry.Cohomology.modules_H_subsingleton_of_cohomologicalBound {X : Scheme} (G : X.Modules) [SheafOfModules.IsQuasicoherent G] [CompactSpace ↥X] [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] [hExt : CategoryTheory.HasExt (TopCat.Sheaf AddCommGrpCat ↑X.toPresheafedSpace)] (n : ℕ) (hn : cohomologicalBound X < n) : Subsingleton (((Scheme.Modules.toSheaf X).obj G).H n)

Cohomology of a quasi-coherent module vanishes strictly above the explicit finite affine cover bound. Only quasi-compactness and an affine diagonal are used.

theorem AlgebraicGeometry.Cohomology.coherent_H_subsingleton_of_cohomologicalBound {X : Scheme} (F : Coh X) [CompactSpace ↥X] [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] (n : ℕ) (hn : cohomologicalBound X < n) : Subsingleton ↑((coherentH X n).obj F)

Coherent sheaves inherit the same explicit finite-affine-cover bound.

noncomputable def AlgebraicGeometry.Cohomology.FiniteDimensionalCohomology.toFiniteCohomology {k : Type u} [Field k] {Y : Scheme} [Y.Over (Spec (CommRingCat.of k))] [IsVariety k Y] (D : FiniteDimensionalCohomology k Y) [IsNoetherian Y] [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from Y))] : FiniteCohomology k Y

Add the independent finite-affine-cover vanishing theorem to degreewise finite-dimensional cohomology. This is the constructor which turns the output of #29 into the FiniteCohomology package consumed by Euler characteristics.

Equations

• D.toFiniteCohomology = { toFiniteDimensionalCohomology := D, bound := fun (x : AlgebraicGeometry.Coh Y) => AlgebraicGeometry.Cohomology.cohomologicalBound Y, vanishesAbove := ⋯ }