The Mukai vector as a class in the intersection ring

v(E) = ch(E)·√td(X), component by component, for a numerical variety of any dimension.

Until now the Mukai vector existed in this repository only as a formula: IntegralMukaiData asserts a triple (rank, c₁, s) by fiat, and RiemannRoch/K3.lean explains in a docstring that this triple is what ch(E)·√td(X) comes to on a K3. This file makes that a theorem. After it, mukaiS is a statement about ch(E)·√td(X) rather than a definition that happens to look right.

Why it is defined in every dimension

mukaiComp takes an arbitrary n. The K3 facts are a section at n = 2, not the definition. Fourier–Mukai and the higher-dimensional Bridgeland lanes want v(E) on a threefold, and defining it only where it is currently used would force a rewrite later.

What is deliberately not touched

mukaiS is not redefined as the degree of the top component. The existing definition stays and K3.degree_mukaiComp_two is the comparison theorem. Redefining it would ripple through the Euler pairing, the Mukai vector, the transfer and the realization files, which is a restructuring this lane must not do. Nothing under Numerical/Core/** or Numerical/GrothendieckGroup/** is edited.

The one place the convolution bites

mukaiComp_mem needs the summand chᵢ(E)·√td_{i-j} to land in codimension i, and the grading gives it codimension j + (i - j). Those agree only because j ≤ i inside the sum, so the index arithmetic is Nat.add_sub_cancel' and not rfl.

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

The codimension-i component of the Mukai vector, (ch(E)·√td(X))ᵢ.

Equations

• V.mukaiComp E i = ∑ j ∈ Finset.range (i + 1), V.chComp E j * V.sqrtToddComp (i - j)

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

The Mukai vector v(E) = ch(E)·√td(X), as a single class.

Equations

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

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.mukaiComp_mem {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) (i : ℕ) : V.mukaiComp E i ∈ V.ring.piece i

The i-th component lives in codimension i.

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

The Mukai vector is additive, because the Chern character is and √td(X) is a constant.

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

@[simp]

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.mukaiComp_zero {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) : V.mukaiComp E 0 = (algebraMap ℚ A) ↑(V.rank E)

v₀(E) = rank E, because √td₀ = 1 and ch₀ = rank.

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

A product of Mukai components integrates to zero unless the codimensions add to the dimension. This is the shape degree_chComp_mul_chComp_mul_toddComp_eq_zero already has for the Chern character, and it is what makes the Euler pairing collapse to a single term.