Realizing a triangulated Grothendieck group numerically

CategoryTheory.Triangulated.K₀ is the Grothendieck group of a triangulated category; AlgebraicGeometry.Numerical's N is the numerical Grothendieck group of a variety, supplied axiomatically by NumericalVarietyData. Nothing in this repository connected them, so no statement about a Fourier--Mukai transform could reach the Mukai lattice. This file supplies the connection as data and proves what follows from it.

The chain it completes is

K₀ 𝒳  --K₀.map Φ-->  K₀ 𝒴
  | cl                  | cl'
  v                     v
  N   ----- φ ------>   N'
  | mukaiVector         | mukaiVector
  v                     v
 ℤ×Λ×ℤ  ---------->  ℤ×Λ'×ℤ

and the theorem is that the Mukai pairing of two Mukai vectors is unchanged when φ preserves the Euler form: pairing_mukaiVector_eq_of_preservesEuler. Specialised to Φ = C.transform K it says the pairing is unchanged on Mukai vectors of realized classes, pairing_mukaiVector_eq_on_realized.

With IntegralMukaiData this is not an isometry, and is deliberately not named as one. At that data level mukaiVector is a bare function, so there is no bilinear form for a map to be an isometry of; the statements are equalities of pairings between vectors that happen to be indexed by the same classes.

With AdditiveMukaiData it is one, and is named as one. That structure adds additivity of c₁, which makes mukaiVectorHom an AddMonoidHom and mukaiForm a LinearMap.BilinForm ℤ N, and isometryOfPreservesEuler packages the same equality as a LinearMap.BilinForm.Isometry — Mathlib's structure, so the word carries its standard meaning.

Two things that remain absent in both layers. No map MukaiLattice Λ → MukaiLattice Λ' is constructed anywhere: the isometry is of the forms on N and N', not of the extensions, and one should not expect the split map (r, c, s) ↦ (r, f c, s) to be it, because a Fourier--Mukai transform does not preserve rank. And no injectivity or surjectivity of φ is assumed or proved, so isometryOfPreservesEuler is an isometric map; isometryEquivOfPreservesEuler is the bijective version and takes the bijection as an input.

The realization is a hypothesis, and a large one

The generic K₀.Realization root names the supplied class map without wrapping its additive homomorphism in another carrier. Nothing here constructs its geometric specialization. For an actual smooth projective X the realization would be K₀(D^b(Coh X)) → N(X). The ingredients of that are missing or unconnected:

• D^b(Coh X) itself now exists in DerivedCategory/Coherent.lean as SchemeBoundedCoherentDerivedCategory, with Perf(X) inside it — but nothing connects it to this file: no class map out of its K₀ is constructed, and this file does not import it;
• the Chern character of an object of a derived category does not exist -- NumericalVarietyData.chComp is a field of the selected presentation, defined on the abstract N, not computed from a complex;
• the quotient of K₀ by the radical of the Euler form is built in GrothendieckGroup.Lattice for the numerical side only.

So this file does not shorten the distance to a geometric theorem. What it does is make the distance explicit and let the categorical side be stated.

What this file does not assert

• Nothing constructs a geometric K₀.Realization, and nothing constructs a K₀.Realization.Descends witness. Both are supplied. An AdditiveMukaiData is no longer uninhabited — Numerical/Models/Surface/K3Mukai.lean builds one on the rank-one model — but none comes from a scheme, so the isometry statements still rest on a lattice-valued additive Chern class that no file produces geometrically.
• Nothing proves a Fourier--Mukai transform preserves the Euler pairing. That it does when the transform is an equivalence is a real theorem, and the hypothesis that carries it is full faithfulness together with k-linearity and shift-compatibility -- not adjunction, and not Serre duality, which is unnecessary once full faithfulness is known. See EulerTransfer's docstring. PreservesEuler is a hypothesis here, not a conclusion, and no transform is shown to satisfy it.
• No Hodge structure appears anywhere in this repository, so the classical statement that a Fourier--Mukai equivalence induces a Hodge isometry is not what is proved. What is proved concerns the lattice form alone. This is the claim AdditiveMukaiData does not license: an isometry of bilinear forms is not a Hodge isometry, and nothing here has a Hodge structure to be compatible with.
• No claim that a realization is injective, surjective, or unique, and none that two functors with the same descent are isomorphic.
• No map of Mukai extensions ℤ × Λ × ℤ → ℤ × Λ' × ℤ is constructed. The isometry that does exist is of the forms pulled back to N and N'.

def AlgebraicGeometry.Numerical.PreservesEuler {n : ℕ} {A : Type y₁} {A' : Type y₂} {N : Type x₁} {N' : Type x₂} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [CommRing A'] [Algebra ℚ A'] [AddCommGroup N'] (V : NumericalVarietyData n A N) (V' : NumericalVarietyData n A' N') (φ : N →+ N') : Prop

φ preserves the Euler form: χ(φE, φF) = χ(E, F).

For a fully faithful k-linear shift-compatible functor this is a theorem; adjunction alone does not give it, and Serre duality is not needed for it. Here it is a hypothesis; nothing in this repository discharges it for any functor.

Equations

• AlgebraicGeometry.Numerical.PreservesEuler V V' φ = ∀ (E F : N), V'.chi₂ (φ E) (φ F) = V.chi₂ E F

theorem AlgebraicGeometry.Numerical.pairing_mukaiVector_eq_of_preservesEuler {A : Type y₁} {A' : Type y₂} {N : Type x₁} {N' : Type x₂} {Λ : Type w₁} {Λ' : Type w₂} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [CommRing A'] [Algebra ℚ A'] [AddCommGroup N'] [AddCommGroup Λ] [AddCommGroup Λ'] {V : NumericalVarietyData 2 A N} {V' : NumericalVarietyData 2 A' N'} (D : K3.IntegralMukaiData V Λ) (D' : K3.IntegralMukaiData V' Λ') (hHRR : V.SatisfiesHRR) (hHRR' : V'.SatisfiesHRR) (hK3 : K3.IsK3 V) (hK3' : K3.IsK3 V') (φ : N →+ N') (hφ : PreservesEuler V V' φ) (E F : N) : Mukai.pairing D'.b (D'.mukaiVector (φ E)) (D'.mukaiVector (φ F)) = Mukai.pairing D.b (D.mukaiVector E) (D.mukaiVector F)

An Euler-preserving map leaves the Mukai pairing unchanged.

Not an isometry statement: this equates two pairings, and constructs no map of lattices. It is the arithmetic heart of the bridge, and where the sign convention pays off: both sides equal −χ of their arguments by IntegralMukaiData.chi₂_eq_neg_pairing, so preserving χ is exactly preserving the Mukai pairing. The ℤ-valued conclusion comes from the ℚ-valued one by injectivity of the cast.

theorem AlgebraicGeometry.Numerical.selfPairing_mukaiVector_eq_of_preservesEuler {A : Type y₁} {A' : Type y₂} {N : Type x₁} {N' : Type x₂} {Λ : Type w₁} {Λ' : Type w₂} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [CommRing A'] [Algebra ℚ A'] [AddCommGroup N'] [AddCommGroup Λ] [AddCommGroup Λ'] {V : NumericalVarietyData 2 A N} {V' : NumericalVarietyData 2 A' N'} (D : K3.IntegralMukaiData V Λ) (D' : K3.IntegralMukaiData V' Λ') (hHRR : V.SatisfiesHRR) (hHRR' : V'.SatisfiesHRR) (hK3 : K3.IsK3 V) (hK3' : K3.IsK3 V') (φ : N →+ N') (hφ : PreservesEuler V V' φ) (E : N) : Mukai.selfPairing D'.b (D'.mukaiVector (φ E)) = Mukai.selfPairing D.b (D.mukaiVector E)

Self-pairings are preserved, hence so is sphericity of a Mukai vector.

theorem AlgebraicGeometry.Numerical.isSpherical_mukaiVector_iff_of_preservesEuler {A : Type y₁} {A' : Type y₂} {N : Type x₁} {N' : Type x₂} {Λ : Type w₁} {Λ' : Type w₂} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [CommRing A'] [Algebra ℚ A'] [AddCommGroup N'] [AddCommGroup Λ] [AddCommGroup Λ'] {V : NumericalVarietyData 2 A N} {V' : NumericalVarietyData 2 A' N'} (D : K3.IntegralMukaiData V Λ) (D' : K3.IntegralMukaiData V' Λ') (hHRR : V.SatisfiesHRR) (hHRR' : V'.SatisfiesHRR) (hK3 : K3.IsK3 V) (hK3' : K3.IsK3 V') (φ : N →+ N') (hφ : PreservesEuler V V' φ) (E : N) : Mukai.IsSpherical D'.b (D'.mukaiVector (φ E)) ↔ Mukai.IsSpherical D.b (D.mukaiVector E)

An Euler-preserving map carries spherical Mukai vectors to spherical ones, in both directions.

The isometry

Everything above equates pairings. With AdditiveMukaiData the Mukai form is a LinearMap.BilinForm ℤ N and φ is a linear map of the underlying groups, so the same equalities assemble into a LinearMap.BilinForm.Isometry — the word now carrying Mathlib's meaning rather than an informal one.

Nothing new is proved: map_app' below is literally pairing_mukaiVector_eq_of_preservesEuler. What changes is that there is now an object for it to be a property of.

noncomputable def AlgebraicGeometry.Numerical.isometryOfPreservesEuler {A : Type y₁} {A' : Type y₂} {N : Type x₁} {N' : Type x₂} {Λ : Type w₁} {Λ' : Type w₂} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [CommRing A'] [Algebra ℚ A'] [AddCommGroup N'] [AddCommGroup Λ] [AddCommGroup Λ'] {V : NumericalVarietyData 2 A N} {V' : NumericalVarietyData 2 A' N'} (D : K3.AdditiveMukaiData V Λ) (D' : K3.AdditiveMukaiData V' Λ') (hHRR : V.SatisfiesHRR) (hHRR' : V'.SatisfiesHRR) (hK3 : K3.IsK3 V) (hK3' : K3.IsK3 V') (φ : N →+ N') (hφ : PreservesEuler V V' φ) : D.mukaiForm →bᵢ D'.mukaiForm

An Euler-preserving map is an isometry of Mukai forms.

The proof field is pairing_mukaiVector_eq_of_preservesEuler unchanged; the content is in the types. Isometry is LinearMap.BilinForm.Isometry, so this asserts exactly: a ℤ-linear map under which the two Mukai forms agree.

Read what is still absent. This is an isometry of the forms on N and N' — the numerical Grothendieck groups — not of the Mukai extensions ℤ × Λ × ℤ and ℤ × Λ' × ℤ, and no map between those is built here. Nor is φ claimed injective or surjective, so this is an isometric map rather than an isometric equivalence; isometryEquivOfPreservesEuler is the bijective version, and it takes the bijection as input.

There is a reason not to expect the split map (r, c, s) ↦ (r, f c, s) on extensions: a Fourier--Mukai transform does not preserve rank in general, so a Λ →+ Λ' compatible with mukaiVector in that shape would be demanding something the intended examples do not satisfy.

Equations

• AlgebraicGeometry.Numerical.isometryOfPreservesEuler D D' hHRR hHRR' hK3 hK3' φ hφ = { toLinearMap := φ.toIntLinearMap, map_app' := ⋯ }

@[simp]

theorem AlgebraicGeometry.Numerical.isometryOfPreservesEuler_apply {A : Type y₁} {A' : Type y₂} {N : Type x₁} {N' : Type x₂} {Λ : Type w₁} {Λ' : Type w₂} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [CommRing A'] [Algebra ℚ A'] [AddCommGroup N'] [AddCommGroup Λ] [AddCommGroup Λ'] {V : NumericalVarietyData 2 A N} {V' : NumericalVarietyData 2 A' N'} (D : K3.AdditiveMukaiData V Λ) (D' : K3.AdditiveMukaiData V' Λ') (hHRR : V.SatisfiesHRR) (hHRR' : V'.SatisfiesHRR) (hK3 : K3.IsK3 V) (hK3' : K3.IsK3 V') (φ : N →+ N') (hφ : PreservesEuler V V' φ) (E : N) : (isometryOfPreservesEuler D D' hHRR hHRR' hK3 hK3' φ hφ) E = φ E

The isometry changes the bilinear form but retains the supplied additive map on vectors.

noncomputable def AlgebraicGeometry.Numerical.isometryEquivOfPreservesEuler {A : Type y₁} {A' : Type y₂} {N : Type x₁} {N' : Type x₂} {Λ : Type w₁} {Λ' : Type w₂} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [CommRing A'] [Algebra ℚ A'] [AddCommGroup N'] [AddCommGroup Λ] [AddCommGroup Λ'] {V : NumericalVarietyData 2 A N} {V' : NumericalVarietyData 2 A' N'} (D : K3.AdditiveMukaiData V Λ) (D' : K3.AdditiveMukaiData V' Λ') (hHRR : V.SatisfiesHRR) (hHRR' : V'.SatisfiesHRR) (hK3 : K3.IsK3 V) (hK3' : K3.IsK3 V') (φ : N ≃+ N') (hφ : PreservesEuler V V' ↑φ) : D.mukaiForm.IsometryEquiv D'.mukaiForm

An Euler-preserving isomorphism is an isometric equivalence.

The bijection is supplied, not derived: PreservesEuler says nothing about injectivity or surjectivity, and no result in this repository produces an isomorphism of numerical Grothendieck groups. Classically the class map of a Fourier--Mukai equivalence is one, and the categorical shadow of that is DualKernel in the stability track — but that lives on K₀, and getting from there to N would need the realizations to be compatible with both directions, which nothing states.

Equations

• AlgebraicGeometry.Numerical.isometryEquivOfPreservesEuler D D' hHRR hHRR' hK3 hK3' φ hφ = { toLinearEquiv := φ.toIntLinearEquiv, map_app' := ⋯ }

theorem AlgebraicGeometry.Numerical.pairing_mukaiVector_eq_on_realized {𝒳 : Type u₁} {𝒴 : Type u₂} {𝒲 : Type u₃} [CategoryTheory.Category.{v₁, u₁} 𝒳] [CategoryTheory.Category.{v₂, u₂} 𝒴] [CategoryTheory.Category.{v₃, u₃} 𝒲] [CategoryTheory.Limits.HasZeroObject 𝒳] [CategoryTheory.HasShift 𝒳 ℤ] [CategoryTheory.Preadditive 𝒳] [∀ (n : ℤ), (CategoryTheory.shiftFunctor 𝒳 n).Additive] [CategoryTheory.Pretriangulated 𝒳] [CategoryTheory.Limits.HasZeroObject 𝒴] [CategoryTheory.HasShift 𝒴 ℤ] [CategoryTheory.Preadditive 𝒴] [∀ (n : ℤ), (CategoryTheory.shiftFunctor 𝒴 n).Additive] [CategoryTheory.Pretriangulated 𝒴] [CategoryTheory.Limits.HasZeroObject 𝒲] [CategoryTheory.HasShift 𝒲 ℤ] [CategoryTheory.Preadditive 𝒲] [∀ (n : ℤ), (CategoryTheory.shiftFunctor 𝒲 n).Additive] [CategoryTheory.Pretriangulated 𝒲] {A : Type y₁} {A' : Type y₂} {N : Type x₁} {N' : Type x₂} {Λ : Type w₁} {Λ' : Type w₂} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [CommRing A'] [Algebra ℚ A'] [AddCommGroup N'] [AddCommGroup Λ] [AddCommGroup Λ'] {V : NumericalVarietyData 2 A N} {V' : NumericalVarietyData 2 A' N'} (C : CategoryTheory.Triangulated.FourierMukai.Correspondence 𝒳 𝒴 𝒲) (K : 𝒲) [C.pull.CommShift ℤ] [(C.tensor.obj K).CommShift ℤ] [C.push.CommShift ℤ] [C.pull.IsTriangulated] [(C.tensor.obj K).IsTriangulated] [C.push.IsTriangulated] (R : CategoryTheory.Triangulated.K₀.Realization 𝒳 N) (R' : CategoryTheory.Triangulated.K₀.Realization 𝒴 N') (φ : N →+ N') (hd : R.Descends R' (C.transform K) φ) (D : K3.IntegralMukaiData V Λ) (D' : K3.IntegralMukaiData V' Λ') (hHRR : V.SatisfiesHRR) (hHRR' : V'.SatisfiesHRR) (hK3 : K3.IsK3 V) (hK3' : K3.IsK3 V') (hφ : PreservesEuler V V' φ) (x y : CategoryTheory.Triangulated.K₀ 𝒳) : Mukai.pairing D'.b (D'.mukaiVector (R' ((C.transformK₀ K) x))) (D'.mukaiVector (R' ((C.transformK₀ K) y))) = Mukai.pairing D.b (D.mukaiVector (R x)) (D.mukaiVector (R y))

A kernel functor leaves the Mukai pairing unchanged on realized classes, given a descent of its class map that preserves the Euler form.

Read the quantifiers carefully. The conclusion is an equality of pairings for the Mukai vectors of R x and R y, for classes x y : K₀ 𝒳. It is NOT an isometry of Mukai lattices: no map between the two lattices is built, the statement says nothing at vectors outside the image of mukaiVector ∘ R, and at this data level mukaiVector is not additive. mukaiForm_eq_on_realized is the AdditiveMukaiData restatement, where the two sides are values of a genuine bilinear form; even there the map whose isometry property it is, is φ, not a map of extensions.

Every geometric input is named: the two realizations, the descent, and Euler-preservation. None is constructed anywhere, and the classical theorem -- that a Fourier--Mukai equivalence supplies all of them and a Hodge isometry besides -- is not proved here.

theorem AlgebraicGeometry.Numerical.mukaiForm_eq_on_realized {𝒳 : Type u₁} {𝒴 : Type u₂} {𝒲 : Type u₃} [CategoryTheory.Category.{v₁, u₁} 𝒳] [CategoryTheory.Category.{v₂, u₂} 𝒴] [CategoryTheory.Category.{v₃, u₃} 𝒲] [CategoryTheory.Limits.HasZeroObject 𝒳] [CategoryTheory.HasShift 𝒳 ℤ] [CategoryTheory.Preadditive 𝒳] [∀ (n : ℤ), (CategoryTheory.shiftFunctor 𝒳 n).Additive] [CategoryTheory.Pretriangulated 𝒳] [CategoryTheory.Limits.HasZeroObject 𝒴] [CategoryTheory.HasShift 𝒴 ℤ] [CategoryTheory.Preadditive 𝒴] [∀ (n : ℤ), (CategoryTheory.shiftFunctor 𝒴 n).Additive] [CategoryTheory.Pretriangulated 𝒴] [CategoryTheory.Limits.HasZeroObject 𝒲] [CategoryTheory.HasShift 𝒲 ℤ] [CategoryTheory.Preadditive 𝒲] [∀ (n : ℤ), (CategoryTheory.shiftFunctor 𝒲 n).Additive] [CategoryTheory.Pretriangulated 𝒲] {A : Type y₁} {A' : Type y₂} {N : Type x₁} {N' : Type x₂} {Λ : Type w₁} {Λ' : Type w₂} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [CommRing A'] [Algebra ℚ A'] [AddCommGroup N'] [AddCommGroup Λ] [AddCommGroup Λ'] {V : NumericalVarietyData 2 A N} {V' : NumericalVarietyData 2 A' N'} (C : CategoryTheory.Triangulated.FourierMukai.Correspondence 𝒳 𝒴 𝒲) (K : 𝒲) [C.pull.CommShift ℤ] [(C.tensor.obj K).CommShift ℤ] [C.push.CommShift ℤ] [C.pull.IsTriangulated] [(C.tensor.obj K).IsTriangulated] [C.push.IsTriangulated] (R : CategoryTheory.Triangulated.K₀.Realization 𝒳 N) (R' : CategoryTheory.Triangulated.K₀.Realization 𝒴 N') (φ : N →+ N') (hd : R.Descends R' (C.transform K) φ) (D : K3.AdditiveMukaiData V Λ) (D' : K3.AdditiveMukaiData V' Λ') (hHRR : V.SatisfiesHRR) (hHRR' : V'.SatisfiesHRR) (hK3 : K3.IsK3 V) (hK3' : K3.IsK3 V') (hφ : PreservesEuler V V' φ) (x y : CategoryTheory.Triangulated.K₀ 𝒳) : (D'.mukaiForm (R' ((C.transformK₀ K) x))) (R' ((C.transformK₀ K) y)) = (D.mukaiForm (R x)) (R y)

The Mukai form is unchanged along a kernel functor's realized classes.

pairing_mukaiVector_eq_on_realized stated against AdditiveMukaiData, where the two sides are values of an actual bilinear form. The hypotheses are the same ones, with no addition beyond the additivity AdditiveMukaiData carries.

Still not an isometry of the two Mukai extensions: the map whose isometry property this is, is φ on numerical Grothendieck groups (isometryOfPreservesEuler), and this theorem is that isometry evaluated at realized classes.