The Euler pairing is the integral of Mukai classes, on a K3

χ(E,F) = ∫_X v(E)^∨·v(F), with v(E) = ch(E)·√td(X) the actual class from Mukai/VectorClass.lean. This is the identity that makes √td(X) earn its place, and it is the form Mukai's paper uses and a Fourier–Mukai comparison needs.

EulerPairing.lean already proves χ(E,F) = −⟨v(E),v(F)⟩ against the explicit formula for the Mukai pairing. That is a different statement: it compares against a formula, this compares against the class.

The sign, stated out loud rather than left to the reader

The headline identity carries no minus sign, and this is the one thing here that is easy to get wrong — a draft of this lane wrote one and propagated it into three further statements.

The two objects differ by a sign, and conflating them is where a spurious minus comes from:

• the Mukai pairing ⟨v,w⟩, which EulerPairing.lean defines by the explicit formula ∫c₁(E)c₁(F) − r_E·s_F − r_F·s_E;
• the integral of the dual product ∫ v^∨·w, which is this file's mukaiIntegral.

They are related by ⟨v,w⟩ = −∫ v^∨·w. So the literature identity χ(E,F) = −⟨v(E),v(F)⟩ and this file's χ(E,F) = +∫ v(E)^∨·v(F) are the same statement, and both are true.

The diagonal is the cross-check: chi₂_self gives χ(E,E) = 2r² − ∫Δ while mukaiSelfPairing_eq gives ⟨v,v⟩ = ∫Δ − 2r², so mukaiIntegral E E = −mukaiSelfPairing E. If a statement here came out with the opposite sign, the error would be in its proof and not in this note.

The dual, and why it is the literature's involution on a K3

mukaiDual uses chDual's convention, chᵢ(E^∨) = (−1)ⁱchᵢ(E), applied to the Mukai components. The literature's Mukai involution is (r,c,s)^∨ = (r,−c,s). On a K3 the two agree, because the odd component of √td(X) vanishes and so √td(X) is its own dual.

Two dimensions only, and why

mukaiDual is defined for every n, but nothing relates it to χ outside IsK3. On a general surface χ(E,F) ≠ ∫ v(E)^∨·v(F), because td₁ ≠ 0 makes (√td)^∨ ≠ √td; Surface.chi₂_sub_chi₂_swap already measures the resulting asymmetry. That is the whole story and this file stops there.

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

The dual Mukai class v(E)^∨, alternating in codimension, exactly as chDual is.

Equations

• V.mukaiDual E = ∑ i ∈ Finset.range (n + 1), (-1) ^ i • V.mukaiComp E i

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

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

The integral of the dual product, ∫_X v(E)^∨·v(F).

Note the name: this is not the Mukai pairing. The two differ by a sign; see the module docstring.

Equations

• AlgebraicGeometry.Numerical.K3.mukaiIntegral V E F = V.ring.degree (V.mukaiDual E * V.mukaiClass F)

theorem AlgebraicGeometry.Numerical.K3.mukaiDual_eq {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} (E : N) : V.mukaiDual E = V.mukaiComp E 0 - V.mukaiComp E 1 + V.mukaiComp E 2

The dual class on a surface, written out.

theorem AlgebraicGeometry.Numerical.K3.mukaiClass_eq {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} (E : N) : V.mukaiClass E = V.mukaiComp E 0 + V.mukaiComp E 1 + V.mukaiComp E 2

The Mukai class on a surface, written out.

theorem AlgebraicGeometry.Numerical.K3.mukaiIntegral_eq {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} (hK3 : IsK3 V) (E F : N) : mukaiIntegral V E F = ↑(V.rank E) * mukaiS V F - V.ring.degree (V.chComp E 1 * V.chComp F 1) + ↑(V.rank F) * mukaiS V E

The expansion. Only the three pairs with i + j = 2 survive the integral, and the middle one carries the sign of the dual.

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

The headline. χ(E,F) = ∫_X v(E)^∨·v(F), with no minus sign; see the module docstring on why, and on why chi₂_eq_neg_mukaiPairing carries one.

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

The integral is symmetric, because √td(X) is its own dual on a K3.

theorem AlgebraicGeometry.Numerical.K3.mukaiIntegral_self {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} (hK3 : IsK3 V) (E : N) : mukaiIntegral V E E = -mukaiSelfPairing V E

On the diagonal the integral is minus the Mukai self-pairing. This is the cross-check the module docstring names.

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

Consequently the integral is 2·rank² − ∫Δ, through the existing discriminant comparison.

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

The sign, as a theorem. The integral of the dual product is minus the Mukai pairing.

The three-way closure

The abstract lattice pairing, the explicit formula and the integral of classes are one number.

theorem AlgebraicGeometry.Numerical.K3.pairing_eq_neg_mukaiIntegral {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} {Λ : Type u_1} [AddCommGroup Λ] (D : IntegralMukaiData V Λ) (hHRR : V.SatisfiesHRR) (hK3 : IsK3 V) (E F : N) : ↑(Mukai.pairing D.b (D.mukaiVector E) (D.mukaiVector F)) = -mukaiIntegral V E F

The abstract Mukai pairing on the lattice is minus the integral of classes.

Composing pairing_mukaiVector, which lands on the explicit formula, with mukaiIntegral_eq_neg_mukaiPairing. This is the one place the sign is visible from both sides at once.