The Euler characteristic of a sheaf of modules on a scheme #
For a scheme X over a field k, the cohomology Hⁱ(X, M) of a sheaf of modules is a
k-vector space, so the alternating sum of its dimensions can be formed. This file introduces
that alternating sum, truncated at a degree n, and proves that it is additive on short exact
sequences as soon as the truncation degree is one past the last nonvanishing degree.
Main declarations #
Scheme.Modules.eulerCharBelow k X M n, the alternating sum∑_{i < n} (-1)ⁱ dim_k Hⁱ(X, M). For a sheaf whose cohomology is finite-dimensional in degrees< nand vanishes in degrees≥ nthis is the Euler characteristicχ(X, M);Scheme.Modules.eulerCharBelow_sub_sub, the exact defect of additivity: the failure ofeulerCharBelowto be additive on a short exact sequence0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0is, up to sign, the dimension of the image of the last connecting map that the truncation cuts off;Scheme.Modules.eulerCharBelow_eq_add_of_cohomologyδ_eq_zero, the additivity itself, under the vanishing of the connecting map the truncation cuts off, andScheme.Modules.eulerCharBelow_eq_add, the form in which that vanishing comes from the vanishing ofHⁿ(X, M₁);Scheme.Modules.finrank_cohomology_zero_sub_one_eq_add, the shape of the additivity on a curve, where cohomology vanishes above degree one so thatχ(X, M) = dim H⁰(X, M) - dim H¹(X, M);Scheme.Modules.eulerCharBelow_congr, the invariance of the truncated Euler characteristic under isomorphism, andScheme.Modules.finrank_cohomology_zero_eq_finrank_globalSections, the identification ofdim H⁰(X, M)with the dimension of the space of global sections.
Junk values #
No finiteness assumption is built into eulerCharBelow, exactly as none is built into
Mathlib's HomologicalComplex.eulerChar: Module.finrank is 0 on an infinite-dimensional
space, so a degree i < n in which Hⁱ(X, M) is infinite-dimensional contributes 0 to the
sum instead of making it meaningless. The alternating sum is therefore read as an Euler
characteristic when the cohomology is finite-dimensional in the degrees < n it sums over:
accordingly the statements that read it that way, eulerCharBelow_sub_sub,
eulerCharBelow_eq_add_of_cohomologyδ_eq_zero, eulerCharBelow_eq_add and
finrank_cohomology_zero_sub_one_eq_add, assume that finite-dimensionality — but only where
the dimension count really needs it. For the middle term of the sequence that is the degrees
below the truncation; for the first term only the positive ones among them, since the
degree-zero contribution of M₁ is computed by an injectivity; and for the third term nothing
at all, since exactness makes Hⁱ(X, M₃) finite-dimensional as soon as Hⁱ(X, M₂) and
Hⁱ⁺¹(X, M₁) are — only eulerCharBelow_sub_sub, whose defect term lives in the top degree
the truncation reads, still assumes it there. So the curve statement
finrank_cohomology_zero_sub_one_eq_add assumes finite-dimensionality of Hⁱ(X, M₂) in
degrees 0 and 1 and of H¹(X, M₁), and of nothing else — while
eulerCharBelow_zero, eulerCharBelow_succ, eulerCharBelow_two and eulerCharBelow_congr
are identities of the alternating sum as it stands and need no such hypothesis.
The proof is the usual dimension count in the long exact cohomology sequence: the rank-nullity
theorem turns each of the three cohomology dimensions in degree i into a sum of two ranks of
maps of the sequence, and the alternating sum telescopes down to the single rank left over at
the truncation degree.
Additivity of the Euler characteristic is what makes the degree of a line bundle on a curve,
deg L := χ(L) - χ(𝒪_X), behave additively, and it is the step from which Riemann-Roch is
proved by induction on a divisor. It is therefore Layer B infrastructure for
TauCetiRoadmap/JacobianChallenge/README.md, "genus, Riemann-Roch, Serre duality".
No formalization is vendored. The alternating-sum bookkeeping reuses Mathlib's
LinearMap.finrank_range_add_finrank_ker, LinearMap.finrank_range_of_inj and
Function.Exact.linearMap_ker_eq, and the finite-dimensionality that exactness supplies is
Mathlib's Module.Finite.of_exact; the long exact sequence and the linearity of its maps are
TauCeti/AlgebraicGeometry/Cohomology/LongExactSequence.lean.
The alternating sum ∑_{i < n} (-1)ⁱ dim_k Hⁱ(X, M) of the dimensions of the cohomology of
a sheaf of modules on a scheme over a field, truncated at degree n.
No finiteness assumption is imposed, just as none is imposed on Mathlib's
HomologicalComplex.eulerChar: a degree i < n in which Hⁱ(X, M) is infinite-dimensional
contributes the junk value finrank k Hⁱ(X, M) = 0. For this sum to be the Euler
characteristic χ(X, M) it is enough that the cohomology be finite-dimensional in degrees
< n and vanish in degrees ≥ n; that is a sufficient condition and not a necessary one,
since a truncation that cuts off finite-dimensional cohomology whose own alternating sum
vanishes computes χ(X, M) just as well. On a curve, the relevant truncation is n = 2.
Equations
- AlgebraicGeometry.Scheme.Modules.eulerCharBelow k X M n = ∑ i ∈ Finset.range n, (-1) ^ i * ↑(Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i))
Instances For
An isomorphism of sheaves of modules induces a k-linear equivalence on cohomology.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The truncated Euler characteristic only depends on the isomorphism class of the sheaf. This
is what makes an invariant such as the degree χ(L) - χ(𝒪_X) of a line bundle well defined on
the Picard group.
The defect of additivity of the truncated Euler characteristic on a short exact sequence
0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 is, up to sign, the dimension of the image of the connecting map
Hⁿ(X, M₃) → Hⁿ⁺¹(X, M₁) that the truncation cuts off.
Finite-dimensionality is only assumed in the degrees the truncation reads, that is in the
degrees < n + 1 summed over — and for the first term of the sequence only in the positive
ones, since the degree-zero contribution of M₁ is computed by the injectivity of
H⁰(X, M₁) → H⁰(X, M₂) rather than by rank-nullity, and for the third term only in the top
degree n, since exactness supplies it in the lower ones.
Additivity of the Euler characteristic. If 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 is a short exact
sequence of sheaves of modules whose first two terms have finite-dimensional cohomology in the
degrees < n + 1 that the truncation reads, and the connecting map Hⁿ(X, M₃) → Hⁿ⁺¹(X, M₁)
that the truncation cuts off vanishes, then the Euler characteristics truncated at n + 1 add
up. The third term needs no hypothesis: exactness makes its cohomology finite-dimensional in
those degrees too.
This is the exact hypothesis the defect formula eulerCharBelow_sub_sub asks for; the usual
sufficient condition, the vanishing of the whole target Hⁿ⁺¹(X, M₁), is
eulerCharBelow_eq_add.
Additivity of the Euler characteristic under a vanishing target. If
0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 is a short exact sequence of sheaves of modules whose first two terms
have finite-dimensional cohomology in the degrees < n that the truncation reads, and
Hⁿ(X, M₁) vanishes, then the Euler characteristics truncated at n add up.
Additivity of the Euler characteristic on a curve. For a short exact sequence of sheaves
of modules whose first two terms have finite-dimensional cohomology in degrees 0 and 1 and
with H²(X, M₁) vanishing, as it does on a curve, the Euler characteristics
χ(X, M) = dim H⁰(X, M) - dim H¹(X, M) add up.