The Euler pairing

χ(E,F) = ∫_X ch(E)^∨ · ch(F) · td(X), the bilinear form Bridgeland stability conditions are defined against: the central charge factors through N(X) modulo the radical of this pairing.

What chi₂ is and is not

chi₂ is a definition, not a theorem. At this layer there is no Ext, so there is nothing to prove chi₂ E F = Σᵢ (-1)ⁱ dim Extⁱ(E,F) against; that identity is the bilinear Hirzebruch–Riemann–Roch and it is Layer B's job, exactly as hirzebruch_riemannRoch is for the one-variable chi. What is proved here is that chi₂ is consistent with the chi already in NumericalVarietyData: chi₂_eq_chi_of_isStructureSheafLike says that pairing against a rank-one class with vanishing higher Chern components returns chi.

Main results

• chi₂_eq_sum — the expansion in any dimension, one term per (i, j) with i + j ≤ n.
• Surface.chi₂_eq — the n = 2 specialisation.
• Surface.chi₂_sub_chi₂_swap — the failure of symmetry, measured exactly.
• K3.chi₂_eq_neg_mukaiPairing — χ(E,F) = −⟨v(E), v(F)⟩ on a K3.

The symmetry claim in issue #6 is false

Issue #6 asks for chi₂ E F = chi₂ F E in even dimension. That does not hold, and it is not a convention problem. chi₂_sub_chi₂_swap computes the obstruction on a surface:

χ(E,F) − χ(F,E) = 2·(r_E·∫c₁(F)·td₁ − r_F·∫c₁(E)·td₁),

which is nonzero as soon as td₁ ≠ 0 — on ℙ², for instance, where td₁ = (3/2)H. What is true formally is chi₂_symm_of_toddComp_one_eq_zero: symmetry holds once td₁ = 0, hence on every K3 and every Calabi–Yau. What Serre duality gives in general is χ(E,F) = (-1)ⁿ χ(F, E ⊗ ω_X) — a Layer B theorem about Ext, not an identity between these integrals — so it is not asserted here. The ω_X is not decoration: dropping it would read, at n = 2, as exactly the symmetry disproved above, and it disappears only when ω_X ≅ O_X, which is the same Calabi–Yau hypothesis as td₁ = 0.

Continued in the lattice module

This file proves that chi₂ is additive in each argument (chi₂_add_left, chi₂_add_right). DerivedAlgGeo.AlgebraicGeometry.Numerical.GrothendieckGroup.Lattice packages that biadditivity, constructs the radical quotient and descends the pairing. Keeping the construction there separates the ℚ-valued Euler form from the explicit finite-generation and torsion-freeness hypotheses needed for its underlying ℤ-lattice.

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

The Euler pairing χ(E,F) = ∫_X ch(E)^∨ · ch(F) · td(X).

Note what this does not require: no NumericalRingDualData value. chDual is the explicit alternating sum Σᵢ (-1)ⁱ chᵢ(E), which the grading alone supplies. The involution is what justifies calling it a dual — chi₂_eq_degree_dual_ch below — but the pairing and every consequence of it are available on any NumericalVarietyData.

Equations

• V.chi₂ E F = V.ring.degree (V.chDual E * V.ch F * V.todd)

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

A mixed term q·chᵢ(E)·chⱼ(F)·td_k(X) integrates to zero unless i + j + k = n. This is the only computational input to the expansion, exactly as degree_chComp_mul_toddComp_eq_zero is for the one-variable case.

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

A mixed term chᵢ(E)·chⱼ(F)·td_k(X) integrates to zero unless i + j + k = n.

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) (E F : N) : V.chi₂ E F = ∑ i ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (n + 1 - i), (-1) ^ i * V.ring.degree (V.chComp E i * V.chComp F j * V.toddComp (n - i - j))

The bilinear Riemann–Roch expansion. Integrating ch(E)^∨ · ch(F) · td(X) leaves one term per pair (i, j) with i + j ≤ n, the Todd index being forced to n - i - j:

χ(E,F) = Σᵢ Σ_{j ≤ n-i} (-1)ⁱ ∫_X chᵢ(E)·chⱼ(F)·td_{n-i-j}(X).

The inner range is n + 1 - i rather than n + 1 with a side condition. Both say the same thing, but the truncated range leaves no if in the term, and every dimension-specific specialisation below is then a matter of Finset.sum_range_succ and nothing else.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.degree_algebraMap_mul_mul {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (q : ℚ) (x y : A) : V.ring.degree ((algebraMap ℚ A) q * x * y) = q * V.ring.degree (x * y)

Pulling a scalar out of the left of a triple product.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.degree_mul_algebraMap_mul {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (q : ℚ) (x y : A) : V.ring.degree (x * (algebraMap ℚ A) q * y) = q * V.ring.degree (x * y)

Pulling a scalar out of the middle of a triple product.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.degree_mul_algebraMap {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (q : ℚ) (x : A) : V.ring.degree (x * (algebraMap ℚ A) q) = q * V.ring.degree x

Pulling a scalar out of the right of a product.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.chi₂_add_right {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E F G : N) : V.chi₂ E (F + G) = V.chi₂ E F + V.chi₂ E G

chi₂ is additive in its second argument.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.chi₂_add_left {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E F G : N) : V.chi₂ (E + F) G = V.chi₂ E G + V.chi₂ F G

chi₂ is additive in its first argument.

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.chi₂_eq_degree_dual_ch {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (D : NumericalRingDualData V.ring) (E F : N) : V.chi₂ E F = V.ring.degree (D.dual (V.ch E) * V.ch F * V.todd)

chi₂ written with the involution rather than with chDual, which is how Hirzebruch–Riemann–Roch states it. This is the only place the involution is needed, and it is what earns chDual its name.

theorem AlgebraicGeometry.Numerical.Surface.chi₂_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (E F : N) : V.chi₂ E F = ↑(V.rank E) * ↑(V.rank F) * V.ring.degree (V.toddComp 2) + ↑(V.rank E) * V.ring.degree (V.chComp F 1 * V.toddComp 1) - ↑(V.rank F) * V.ring.degree (V.chComp E 1 * V.toddComp 1) + ↑(V.rank E) * V.ring.degree (V.chComp F 2) + ↑(V.rank F) * V.ring.degree (V.chComp E 2) - V.ring.degree (V.chComp E 1 * V.chComp F 1)

The Euler pairing on a surface.

χ(E,F) = r_E·r_F·∫td₂ + r_E·∫c₁(F)·td₁ − r_F·∫c₁(E)·td₁ + r_E·∫ch₂(F) + r_F·∫ch₂(E) − ∫c₁(E)·c₁(F).

The two td₁ terms carry opposite signs; that asymmetry is the whole content of the dual involution, and it is what chi₂_sub_chi₂_swap measures.

theorem AlgebraicGeometry.Numerical.Surface.chi₂_eq_chi_of_isStructureSheafLike {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (hV : V.SatisfiesHRR) (E F : N) (hr : V.rank E = 1) (h₁ : V.chComp E 1 = 0) (h₂ : V.chComp E 2 = 0) : V.chi₂ E F = ↑(V.chi F)

Pairing against a rank-one class with vanishing higher Chern components returns the one-variable chi. This is the consistency check between chi₂ and the chi that NumericalVarietyData already carries: chi₂ is a new definition, and this is the statement that it is the right one.

theorem AlgebraicGeometry.Numerical.Surface.chi₂_sub_chi₂_swap {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (E F : N) : V.chi₂ E F - V.chi₂ F E = 2 * (↑(V.rank E) * V.ring.degree (V.chComp F 1 * V.toddComp 1) - ↑(V.rank F) * V.ring.degree (V.chComp E 1 * V.toddComp 1))

The Euler pairing is not symmetric, and this is by how much:

χ(E,F) − χ(F,E) = 2·(r_E·∫c₁(F)·td₁ − r_F·∫c₁(E)·td₁).

Issue #6 asked for symmetry in even dimension. It is false: on ℙ², td₁ = (3/2)H ≠ 0, so the right-hand side is nonzero for suitable E, F. Symmetry needs td₁ = 0.

theorem AlgebraicGeometry.Numerical.Surface.chi₂_symm_of_toddComp_one_eq_zero {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (htd : V.toddComp 1 = 0) (E F : N) : V.chi₂ E F = V.chi₂ F E

The Euler pairing is symmetric once td₁(X) = 0 — in particular on every K3 and every Calabi–Yau surface. This is the correct form of the claim issue #6 made for all even dimensions.

noncomputable def AlgebraicGeometry.Numerical.K3.mukaiPairing {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (E F : N) : ℚ

The Mukai pairing ⟨v(E), v(F)⟩ = ∫c₁(E)·c₁(F) − r_E·s_F − r_F·s_E, the bilinear form whose diagonal is mukaiSelfPairing.

Equations

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

theorem AlgebraicGeometry.Numerical.K3.mukaiPairing_self {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (E : N) : mukaiPairing V E E = mukaiSelfPairing V E

The Mukai pairing restricts to mukaiSelfPairing on the diagonal, so nothing in Numerical/RiemannRoch/K3.lean is being redefined.

theorem AlgebraicGeometry.Numerical.K3.mukaiPairing_comm {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (E F : N) : mukaiPairing V E F = mukaiPairing V F E

The Mukai pairing is symmetric.

theorem AlgebraicGeometry.Numerical.K3.chi₂_eq_neg_mukaiPairing {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (hK3 : IsK3 V) (E F : N) : V.chi₂ E F = -mukaiPairing V E F

The Euler pairing is minus the Mukai pairing on a K3: χ(E,F) = −⟨v(E), v(F)⟩.

This is the identity issue #6 named as the check that matters, and it is what fixes the sign convention of the dual involution: with chᵢ(E^∨) = (-1)ⁱchᵢ(E) the sign comes out, and with the opposite convention it does not. The self-pairing case recovers K3.mukaiSelfPairing_eq.

theorem AlgebraicGeometry.Numerical.K3.chi₂_comm {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (hK3 : IsK3 V) (E F : N) : V.chi₂ E F = V.chi₂ F E

Consequently the Euler pairing is symmetric on a K3.

theorem AlgebraicGeometry.Numerical.K3.chi₂_self {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (hK3 : IsK3 V) (E : N) : V.chi₂ E E = 2 * ↑(V.rank E) ^ 2 - V.ring.degree (V.discriminant E)

χ(E,E) = −⟨v(E), v(E)⟩ = 2r² − ∫Δ(E), tying the Euler pairing to the Bogomolov–Gieseker discriminant through K3.mukaiSelfPairing_eq.