Core numerical data of a smooth projective variety over a field

This is Layer A of DerivedAlgGeo: the numerical interface that Bridgeland-stability arguments actually consume from a smooth projective variety, stated for a variety of arbitrary dimension n so that the surface case (n = 2), the threefold case (n = 3) and the fourfold case (n = 4) are specialisations rather than rewrites.

Design

Two explicit data bundles:

• NumericalRingData n A — A is the numerical intersection ring A^•(X)_ℚ: a commutative ℚ-algebra graded by codimension, concentrated in degrees 0, …, n, with a ℚ-linear degree map ∫_X : A → ℚ supported in top codimension.
• NumericalVarietyData n A N — adds the numerical Grothendieck group N, the Chern character, the Todd class of X and the Euler characteristic.

These bundles are passed explicitly: a carrier may support more than one numerical presentation. Hirzebruch--Riemann--Roch is the separate proposition-valued property NumericalVarietyData.SatisfiesHRR.

Trust boundary

NumericalVarietyData records a selected presentation and its structural compatibility laws; it does not assert that the presentation comes from geometry. In particular HRR is not a field. Proving SatisfiesHRR is the job of Layer B (DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent), which builds Coh X, sheaf cohomology, χ, and intersection numbers from Mathlib's scheme theory. Any downstream result that uses HRR must receive that witness explicitly.

Graded components of ch and td are carried as data (chComp, toddComp) rather than extracted by a projection operator. That is deliberate: it keeps this file free of graded-decomposition machinery, and every consumer needs the components anyway.

References

• Hirzebruch, Topological Methods in Algebraic Geometry, §21
• Fulton, Intersection Theory, ch. 15 and 18
• Huybrechts–Lehn, The Geometry of Moduli Spaces of Sheaves, §1.1 and §2.1

structure AlgebraicGeometry.Numerical.NumericalRingData (n : ℕ) (A : Type u) [CommRing A] [Algebra ℚ A] : Type u

A numerical intersection ring of dimension n: a commutative ℚ-algebra A graded by codimension and concentrated in degrees 0, …, n, together with a ℚ-linear degree map degree (written ∫_X in the literature) supported in top codimension.

The bundle is explicit because the same carrier can support several numerical presentations (for example, different degree normalizations).

• piece : ℕ → Submodule ℚ A

  The codimension-i graded piece Aⁱ.

• isInternal : DirectSum.IsInternal self.piece

  The pieces decompose A, i.e. A = ⨁ᵢ Aⁱ.

• piece_eq_bot_of_lt ⦃i : ℕ⦄ : n < i → self.piece i = ⊥

  Nothing lives above the dimension: Aⁱ = 0 for i > n.

• one_mem_piece_zero : 1 ∈ self.piece 0

  1 ∈ A⁰.

• mul_mem_piece {i j : ℕ} {x y : A} : x ∈ self.piece i → y ∈ self.piece j → x * y ∈ self.piece (i + j)

  The grading is multiplicative: Aⁱ · Aʲ ⊆ Aⁱ⁺ʲ.

• degree : A →ₗ[ℚ] ℚ

  The degree map ∫_X : A → ℚ.

• degree_eq_zero_of_mem {i : ℕ} {x : A} : i ≠ n → x ∈ self.piece i → self.degree x = 0

  ∫_X kills every graded piece other than the top one.

theorem AlgebraicGeometry.Numerical.NumericalRingData.algebraMap_mem_piece_zero {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] (R : NumericalRingData n A) (q : ℚ) : (algebraMap ℚ A) q ∈ R.piece 0

Scalars sit in codimension zero.

theorem AlgebraicGeometry.Numerical.NumericalRingData.degree_algebraMap_mul {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] (R : NumericalRingData n A) (q : ℚ) (x : A) : R.degree ((algebraMap ℚ A) q * x) = q * R.degree x

∫_X is ℚ-homogeneous in the sense we actually use it: pulling a scalar out of a product with algebraMap.

theorem AlgebraicGeometry.Numerical.NumericalRingData.eq_zero_of_mem_piece_of_lt {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] (R : NumericalRingData n A) {i : ℕ} (hi : n < i) {x : A} (hx : x ∈ R.piece i) : x = 0

Anything in a piece above the dimension is zero.

structure AlgebraicGeometry.Numerical.NumericalVarietyData (n : ℕ) (A : Type u) (N : Type v) [CommRing A] [Algebra ℚ A] [AddCommGroup N] : Type (max u v)

Numerical data of a smooth projective variety of dimension n over a field.

A is the numerical intersection ring A^•(X)_ℚ and N is the numerical Grothendieck group N(X) = K(X)/≡. The Chern character is carried by its graded components chComp E i = chᵢ(E), the Todd class of X by toddComp i = tdᵢ(X).

Hirzebruch--Riemann--Roch is deliberately kept outside this data bundle as NumericalVarietyData.SatisfiesHRR.

• ring : NumericalRingData n A

  The selected numerical intersection-ring presentation.

• rank : N →+ ℤ

  The rank homomorphism N(X) → ℤ.

• chComp : N → ℕ → A

  The codimension-i component of the Chern character, chᵢ(E).

• chComp_mem (E : N) (i : ℕ) : self.chComp E i ∈ self.ring.piece i

  chᵢ(E) lives in codimension i.

• chComp_zero (E : N) : self.chComp E 0 = (algebraMap ℚ A) ↑(self.rank E)

  ch₀(E) = rank E.

• chComp_add (E F : N) (i : ℕ) : self.chComp (E + F) i = self.chComp E i + self.chComp F i

  The Chern character is additive on N(X).

• toddComp : ℕ → A

  The codimension-i component of the Todd class of X.

• toddComp_mem (i : ℕ) : self.toddComp i ∈ self.ring.piece i

  tdᵢ(X) lives in codimension i.

• toddComp_zero : self.toddComp 0 = 1

  td₀(X) = 1.

• chi : N →+ ℤ

  The Euler characteristic χ(E) = Σᵢ (-1)ⁱ dim Hⁱ(X, E).

structure AlgebraicGeometry.Numerical.NumericalVarietyData.SatisfiesHRR {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) : Prop

Hirzebruch--Riemann--Roch as a proposition-valued property of one explicit numerical presentation. It is not selected by typeclass inference.

• eq (E : N) : ↑(V.chi E) = V.ring.degree ((∑ i ∈ Finset.range (n + 1), V.chComp E i) * ∑ j ∈ Finset.range (n + 1), V.toddComp j)

  χ(E) = ∫_X ch(E) · td(X).

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

The Chern character ch(E) = Σᵢ chᵢ(E).

Equations

• V.ch E = ∑ i ∈ Finset.range (n + 1), V.chComp E i

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

The Todd class td(X) = Σᵢ tdᵢ(X).

Equations

• V.todd = ∑ j ∈ Finset.range (n + 1), V.toddComp j

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.hrr {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) = V.ring.degree (V.ch E * V.todd)

Hirzebruch–Riemann–Roch, restated in terms of ch and todd.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.chComp_eq_zero_of_lt {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) {i : ℕ} (hi : n < i) : V.chComp E i = 0

Components of the Chern character above the dimension vanish.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.toddComp_eq_zero_of_lt {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) {i : ℕ} (hi : n < i) : V.toddComp i = 0

Components of the Todd class above the dimension vanish.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.degree_chComp_mul_toddComp_eq_zero {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) {i j : ℕ} (hij : i + j ≠ n) : V.ring.degree (V.chComp E i * V.toddComp j) = 0

The degree of a mixed term chᵢ(E) · tdⱼ(X) vanishes unless i + j = n.

This is the single computational fact behind every dimension-specific Riemann–Roch formula: expanding ch(E) · td(X) leaves only the terms of total codimension n.