The Euler-characteristic degree of a line bundle

On a proper curve over a field, the degree of a line bundle L can be recovered from Euler characteristics by

deg L = χ(L) - χ(𝒪_X).

This file constructs the right-hand side using the degree-2 truncation of sheaf cohomology and shows that it depends only on the isomorphism class of L. Thus it descends to a function LineBundleClass.eulerDegree k : LineBundleClass X → ℤ. The normalization by the trivial line bundle makes its degree zero by construction.

The definition makes sense for any scheme over a field. As with Scheme.Modules.eulerCharBelow, it is the difference of the usual Euler characteristics when the relevant cohomology groups are finite-dimensional and cohomology above degree one vanishes. On a proper curve with H¹(X, 𝒪_X) finite-dimensional, TauCeti.AlgebraicGeometry.WeilDivisor.Scheme.EulerCharacteristic identifies this invariant with the residue-degree-weighted degree of a divisor of L and proves that it is additive.

Main declarations

• InvertibleSheaf.eulerDegree is χ(L) - χ(𝒪_X) for an invertible sheaf;
• InvertibleSheaf.eulerDegree_def is its defining formula;
• InvertibleSheaf.eulerDegree_eq_sub_unit states it with the structure sheaf 𝒪_X in place of the trivial line bundle;
• InvertibleSheaf.eulerDegree_eq_finrank_sub expands it as the difference of the dimensions of H⁰ and H¹;
• LineBundleClass.eulerDegree descends the invariant to isomorphism classes of line bundles;
• LineBundleClass.eulerDegree_mk and LineBundleClass.eulerDegree_one are its representative and normalization formulas.

The formula is the rearrangement of Riemann--Roch for curves; see Hartshorne, Algebraic Geometry, Chapter IV, Section 1.

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] (L : InvertibleSheaf X) : ℤ

The Euler-characteristic degree χ(L) - χ(𝒪_X) of an invertible sheaf L, using the degree-2 truncation χ(M) = dim H⁰(X, M) - dim H¹(X, M).

For a proper curve, finite-dimensionality and vanishing above degree one make this the usual Euler characteristic degree. No such hypotheses are needed to form the invariant itself; in their absence it has the same possible junk values as Scheme.Modules.eulerCharBelow.

Equations

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

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree_def (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] (L : InvertibleSheaf X) : eulerDegree k L = AlgebraicGeometry.Scheme.Modules.eulerCharBelow k X L.obj 2 - AlgebraicGeometry.Scheme.Modules.eulerCharBelow k X (trivial X).obj 2

The defining formula of the Euler-characteristic degree as a difference of truncated Euler characteristics.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree_eq_sub_unit (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] (L : InvertibleSheaf X) : eulerDegree k L = AlgebraicGeometry.Scheme.Modules.eulerCharBelow k X L.obj 2 - AlgebraicGeometry.Scheme.Modules.eulerCharBelow k X (SheafOfModules.unit X.ringCatSheaf) 2

The Euler-characteristic degree is χ(L) - χ(𝒪_X) with 𝒪_X the structure sheaf.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree_eq_finrank_sub (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] (L : InvertibleSheaf X) : eulerDegree k L = ↑(Module.finrank k (Scheme.Modules.Cohomology L.obj 0)) - ↑(Module.finrank k (Scheme.Modules.Cohomology L.obj 1)) - (↑(Module.finrank k (Scheme.Modules.Cohomology (trivial X).obj 0)) - ↑(Module.finrank k (Scheme.Modules.Cohomology (trivial X).obj 1)))

The Euler-characteristic degree is the difference of dim H⁰ - dim H¹ for the line bundle and the trivial line bundle.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree_congr (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] {L M : InvertibleSheaf X} (e : L.obj ≅ M.obj) : eulerDegree k L = eulerDegree k M

Isomorphic invertible sheaves have the same Euler-characteristic degree.

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree_trivial (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] : eulerDegree k (trivial X) = 0

The trivial line bundle has Euler-characteristic degree zero.

noncomputable def TauCeti.AlgebraicGeometry.LineBundleClass.eulerDegree (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] (a : LineBundleClass X) : ℤ

The Euler-characteristic degree of an isomorphism class of line bundles.

This is well defined because sheaf cohomology, and hence its truncated Euler characteristic, is invariant under isomorphism of coefficient sheaves.

Equations

• TauCeti.AlgebraicGeometry.LineBundleClass.eulerDegree k a = TauCeti.AlgebraicGeometry.LineBundleClass.lift (TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree k) ⋯ a

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.eulerDegree_mk (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] (L : InvertibleSheaf X) : eulerDegree k (mk L) = InvertibleSheaf.eulerDegree k L

The Euler-characteristic degree of the class represented by L is the degree of L.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.eulerDegree_one (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] : eulerDegree k 1 = 0

The tensor-unit class has Euler-characteristic degree zero.