Geometric Euler characteristics of coherent sheaves

This file defines the geometric Euler characteristic

χ(X, F) = ∑ᵢ (-1)ⁱ dimₖ Hⁱ(X, F)

for coherent sheaves on a variety, relative to the two inputs that are not currently supplied by Mathlib:

• the natural k-vector-space structure on coherent sheaf cohomology, functorial in F;
• finite-dimensionality and eventual vanishing.

The first input and degreewise finite-dimensionality are packaged independently in FiniteDimensionalCohomology, the output interface for issue #29. FiniteCohomology extends that interface only with the eventual-vanishing data tracked separately in issue #30. All fields are hypotheses, never axioms. The projective finiteness and boundedness theorems can later construct them without changing the definition of χ.

The alternating sum reuses GradedObject.eulerChar from Mathlib. The support theorem below removes its possible infinite-support junk value, and eulerCharacteristic_eq_sum exposes the usual finite formula. Functoriality gives invariance under isomorphism of coherent sheaves.

Additivity in short exact sequences is the next layer, implemented in DerivedAlgGeo.AlgebraicGeometry.Cohomology.EulerCharacteristic.Additivity: it uses Mathlib's additive Ext sequence and requests precisely the scalar-linearity of its connecting maps.

structure AlgebraicGeometry.Cohomology.FiniteCohomology (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] extends AlgebraicGeometry.Cohomology.FiniteDimensionalCohomology k X : Type (u + 2)

Finite-dimensional coherent cohomology together with eventual vanishing.

The inherited data is exactly the linear comparison and degreewise finiteness output of #29. The two fields added here are the separate #30 boundedness input needed to make the Euler sum finite.

• moduleH : ℕ → CategoryTheory.Functor (Coh X) (ModuleCat k)
• comparison (i : ℕ) : (self.moduleH i).comp (CategoryTheory.forget₂ (ModuleCat k) AddCommGrpCat) ≅ coherentH X i
• finite (i : ℕ) (F : Coh X) : Module.Finite k ↑((self.moduleH i).obj F)
• bound : Coh X → ℕ

  A sheaf-dependent bound above which its cohomology vanishes.

• vanishesAbove (F : Coh X) (i : ℕ) : self.bound F < i → Subsingleton ↑((self.moduleH i).obj F)

  Cohomology vanishes strictly above bound F.

@[reducible, inline]

abbrev AlgebraicGeometry.Cohomology.FiniteCohomology.gradedModule {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) (F : Coh X) : CategoryTheory.GradedObject ℕ (ModuleCat k)

The coherent cohomology groups of F, regarded as a graded family of k-modules.

Equations

• D.gradedModule F i = (D.moduleH i).obj F

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Cohomology.FiniteCohomology.dimension {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) (F : Coh X) (i : ℕ) : ℕ

The dimension of degree-i coherent cohomology.

Equations

• D.dimension F i = D.dimension F i

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.upNat_sign (i : ℕ) : ↑((ComplexShape.up ℕ).χ i) = (-1) ^ i

The sign supplied by the cochain-complex shape is the usual (-1)ⁱ.

noncomputable def AlgebraicGeometry.Cohomology.FiniteCohomology.eulerCharacteristic {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) (F : Coh X) : ℤ

The geometric Euler characteristic of a coherent sheaf.

Equations

• D.eulerCharacteristic F = GradedObject.eulerChar (ComplexShape.up ℕ) (D.gradedModule F)

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.finrankSupport_subset_range {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) (F : Coh X) : GradedObject.finrankSupport (D.gradedModule F) ⊆ ↑(Finset.range (D.bound F + 1))

The finite-rank support of coherent cohomology lies below the supplied vanishing bound.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.eulerCharacteristic_eq_sum {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) (F : Coh X) : D.eulerCharacteristic F = ∑ i ∈ Finset.range (D.bound F + 1), (-1) ^ i * ↑(D.dimension F i)

The Euler characteristic is the ordinary finite alternating sum through any supplied vanishing bound. In particular, the finsum used by Mathlib has no junk value here.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.eulerCharacteristic_eq_sum_of_bound {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) (F : Coh X) (n : ℕ) (h : D.bound F ≤ n) : D.eulerCharacteristic F = ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(D.dimension F i)

The Euler characteristic may be summed through any bound at least as large as the sheaf-dependent vanishing bound.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.dimension_iso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) {F G : Coh X} (e : F ≅ G) (i : ℕ) : D.dimension F i = D.dimension G i

Isomorphic coherent sheaves have equal cohomology dimensions in every degree.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.eulerCharacteristic_iso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) {F G : Coh X} (e : F ≅ G) : D.eulerCharacteristic F = D.eulerCharacteristic G

The geometric Euler characteristic is invariant under isomorphism of coherent sheaves.