General numerical Riemann--Roch expansion

hirzebruch_riemannRoch states χ(E) = ∫_X ch(E) · td(X) with both factors written as sums over all codimensions. Every dimension-specific Riemann–Roch formula is obtained by expanding that product and discarding the terms whose total codimension is not n.

degree_ch_mul_todd does that once, in arbitrary dimension. Any finite-dimensional display formula is an optional evaluation of this identity, not part of the foundational interface.

noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.structureSheafEulerCharacteristic {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) : ℚ

The Euler characteristic of the structure sheaf, represented numerically by the degree of the top Todd component. This definition is dimension-general; surface, threefold, and fourfold names are only compatibility aliases in the specialization modules.

Equations

• V.structureSheafEulerCharacteristic = V.ring.degree (V.toddComp n)

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.degree_ch_mul_todd {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) : V.ring.degree (V.ch E * V.todd) = ∑ i ∈ Finset.range (n + 1), V.ring.degree (V.chComp E i * V.toddComp (n - i))

The Riemann–Roch expansion. Integrating ch(E) · td(X) leaves exactly the n + 1 terms of total codimension n:

∫_X ch(E) · td(X) = Σ_{i=0}^{n} ∫_X chᵢ(E) · td_{n-i}(X).

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.chi_eq_sum {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (hV : V.SatisfiesHRR) (E : N) : ↑(V.chi E) = ∑ i ∈ Finset.range (n + 1), V.ring.degree (V.chComp E i * V.toddComp (n - i))

Riemann–Roch with the product already expanded: χ(E) = Σ_{i=0}^{n} ∫_X chᵢ(E) · td_{n-i}(X).