Display formulas for numerical surfaces

The n = 2 specialisation of AlgebraicGeometry.Numerical.NumericalVarietyData.chi_eq_sum.

This is an optional display specialization of the dimension-general API. It contains no foundational surface object: NumericalVarietyData 2 A N is the general variety interface at dimension two, and the discriminant itself now lives in Numerical/GrothendieckGroup/Discriminant.lean for arbitrary dimension.

Main results

• chi_eq — χ(E) = r·∫td₂(X) + ∫c₁(E)·td₁(X) + ∫ch₂(E).
• compatibility aliases for the dimension-general numerical discriminant.

Writing td₁(X) = −K_X/2 and ch₂(E) = (c₁² − 2c₂)/2 turns chi_eq into the classical χ(E) = r·χ(O_X) + ½c₁(c₁ − K_X) − c₂. Those substitutions need K_X and c₂, which are Layer B objects, so they are not asserted here.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Numerical.Surface.chiStructureSheaf {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) : ℚ

χ(O_X) for a surface, read off the top Todd component: taking E of rank one with vanishing higher Chern components in chi_eq leaves exactly ∫_X td₂(X).

Equations

• AlgebraicGeometry.Numerical.Surface.chiStructureSheaf V = V.structureSheafEulerCharacteristic

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

Riemann–Roch for surfaces.

χ(E) = rank(E) · ∫_X td₂(X) + ∫_X c₁(E)·td₁(X) + ∫_X ch₂(E).

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Numerical.Surface.discriminant {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (E : N) : A

The Bogomolov–Gieseker discriminant Δ(E) = c₁(E)² − 2·rank(E)·ch₂(E), a class in codimension two.

Equivalently Δ(E) = 2·r·c₂(E) − (r − 1)·c₁(E)² once c₂ is available; the ch-form is used here because c₂ is a Layer B object. Bogomolov's inequality — ∫_X Δ(E) ≥ 0 for E slope-semistable with respect to a polarisation — is not stated at this layer: there is no stability notion in NumericalVarietyData, and asserting it here would hide a real theorem behind a class field.

Equations

• AlgebraicGeometry.Numerical.Surface.discriminant V E = V.discriminant E

theorem AlgebraicGeometry.Numerical.Surface.discriminant_mem_piece_two {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (E : N) : V.discriminant E ∈ V.ring.piece 2

The discriminant lives in codimension two.

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

∫_X Δ(E) = ∫_X c₁(E)² − 2·rank(E)·∫_X ch₂(E): the scalar the Bogomolov–Gieseker inequality is about.