A polarisation, the Mumford slope, and the two H-discriminants

The numerical layer has an intersection ring, a Chern character and a rank, but no polarisation: nothing yet picks a class H in codimension one against which degrees are taken. This file adds one, and the three quantities that need it.

Definitions only

Every statement here is a definition, a grading lemma, or an evaluation. No inequality is proved and none is assumed — not Bogomolov–Gieseker, not Hodge index, not 0 ≤ discrH. Those are the next slice's, and discrH's docstring says so where a reader will look.

The two discriminants must not be conflated

There are two different things called "the H-discriminant" and they are not equal:

discDegH E = ∫ Δ(E) · H^(n-2)          -- what Bogomolov–Gieseker is about in dimension n
discrH   E = (∫ch₁(E)·H)² - 2(∫H²)·rk(E)·∫ch₂(E)   -- the surface tilt discriminant

discrH weights the rank slot by ∫H², because that is what the charge formula of Walls/Numerical/Basic.lean requires of a class transported to the (s, t) plane. The two agree only when ∫H² = 1. Conflating them is the mistake this section exists to prevent, and it is why discrH is defined only at n = 2, under Surface, rather than in general.

ℕ-subtraction in the exponents

degH twists by H^(n-1) and discDegH by H^(n-2), both written with ℕ-subtraction. At n = 0 and n < 2 respectively the exponent truncates to 0 and the definition is junk. That is harmless and is the convention the rest of the layer already lives with; the grading lemmas that need the exponent to mean what it says carry 2 ≤ n as an explicit hypothesis.

At n = 2 the discDegH twist is H^0 = 1, which is why the surface statements downstream carry no polarisation in their conclusions — Surface.discDegH_eq records exactly that.

Explicit data, never an instance

Polarization hangs off NumericalRingData, not off NumericalVarietyData: a polarisation is a fact about the intersection ring and says nothing about the Grothendieck group, and keeping it there lets one H serve several presentations on the same carrier. It is a structure, it is passed explicitly, and it is never selected by instance search — the idiom NumericalRingData and NumericalVarietyData already follow.

degree_pow_pos is the only positivity assumed anywhere in this file. It is a field, supplied by whoever builds the polarisation.

Main results

• Polarization and Polarization.pow_mem.
• degH, degH_add, degHHom — the H-degree, additive in the class.
• slopeH — the Mumford slope, junk at rank zero.
• discDegH, discDegH_mul_mem and Surface.discDegH_eq.
• Surface.discrH — the tilt discriminant, and not ∫Δ(E).

The polarisation

structure AlgebraicGeometry.Numerical.Polarization {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] (R : NumericalRingData n A) : Type u

A polarisation of a numerical intersection ring: a codimension-one class whose top self-intersection is positive.

degree_pow_pos is supplied, not proved. It stands for ∫_X Hⁿ > 0, which for an actual ample class follows from Nakai–Moishezon; nothing here relates this structure to Mathlib's IsAmple, and nothing here needs to.

• cls : A

  The polarising class H.

• cls_mem : self.cls ∈ R.piece 1

  H lives in codimension one.

• degree_pow_pos : 0 < R.degree (self.cls ^ n)

  ∫_X Hⁿ > 0. Supplied by the caller.

theorem AlgebraicGeometry.Numerical.Polarization.pow_mem {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] {R : NumericalRingData n A} (P : Polarization R) (i : ℕ) : P.cls ^ i ∈ R.piece i

Hⁱ lives in codimension i.

The H-degree and the Mumford slope

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

The H-degree deg_H(E) = ∫_X ch₁(E) · H^(n-1).

The exponent is ℕ-subtraction, so at n = 0 it truncates to 0 and the definition is junk — the same convention the rest of the numerical layer uses.

Equations

• AlgebraicGeometry.Numerical.degH V P E = V.ring.degree (V.chComp E 1 * P.cls ^ (n - 1))

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

The H-degree is additive, because ch₁ is.

noncomputable def AlgebraicGeometry.Numerical.degHHom {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) : N →+ ℚ

The H-degree, bundled as an additive homomorphism.

Equations

• AlgebraicGeometry.Numerical.degHHom V P = AddMonoidHom.mk' (AlgebraicGeometry.Numerical.degH V P) ⋯

@[simp]

theorem AlgebraicGeometry.Numerical.degHHom_apply {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (E : N) : (degHHom V P) E = degH V P E

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

The Mumford slope μ_H(E) = deg_H(E) / rk(E).

Junk at rank zero, exactly as SlopeData.slope in CategoryTheory/Abelian/Stability/Slope.lean is, so the two agree where they meet.

Equations

• AlgebraicGeometry.Numerical.slopeH V P E = AlgebraicGeometry.Numerical.degH V P E / ↑(V.rank E)

theorem AlgebraicGeometry.Numerical.slopeH_eq {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (E : N) : slopeH V P E = degH V P E / ↑(V.rank E)

The two discriminants

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

The H-twisted discriminant degree ∫_X Δ(E) · H^(n-2).

This is the quantity the Bogomolov–Gieseker inequality is about in dimension n. It is not Surface.discrH; see the module docstring.

Equations

• AlgebraicGeometry.Numerical.discDegH V P E = V.ring.degree (V.discriminant E * P.cls ^ (n - 2))

theorem AlgebraicGeometry.Numerical.discDegH_mul_mem {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (hn : 2 ≤ n) (E : N) : V.discriminant E * P.cls ^ (n - 2) ∈ V.ring.piece n

The integrand of discDegH sits in the top piece, which is what makes discDegH the integral of a top-dimensional class rather than a truncation. 2 ≤ n is where the ℕ-subtraction in the exponent stops being junk.

theorem AlgebraicGeometry.Numerical.Surface.discDegH_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (P : Polarization V.ring) (E : N) : discDegH V P E = V.ring.degree (V.discriminant E)

At n = 2 the twist is H⁰ = 1, so the polarisation drops out of discDegH entirely. This is why the surface statements downstream carry no polarisation in their conclusions.

noncomputable def AlgebraicGeometry.Numerical.Surface.discrH {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (P : Polarization V.ring) (E : N) : ℚ

The surface tilt discriminant discrH(E) = (∫ch₁(E)·H)² − 2·(∫H²)·rk(E)·∫ch₂(E).

This is not discDegH, and it is not ∫Δ(E). It weights the rank slot by ∫H², because that is what the twisted-charge formula of Walls/Numerical/Basic.lean requires of a class transported to the (s, t) plane. The two agree only when ∫H² = 1.

0 ≤ discrH is not proved here. It needs Bogomolov–Gieseker and the Hodge index inequality, both of which are supplied data in the next slice.

Equations

• AlgebraicGeometry.Numerical.Surface.discrH V P E = AlgebraicGeometry.Numerical.degH V P E ^ 2 - 2 * V.ring.degree (P.cls ^ 2) * ↑(V.rank E) * V.ring.degree (V.chComp E 2)

theorem AlgebraicGeometry.Numerical.Surface.discrH_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (P : Polarization V.ring) (E : N) : discrH V P E = degH V P E ^ 2 - 2 * V.ring.degree (P.cls ^ 2) * ↑(V.rank E) * V.ring.degree (V.chComp E 2)

theorem AlgebraicGeometry.Numerical.Surface.discrH_eq_selfPairing {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (P : Polarization V.ring) (E : N) : discrH V P E = Mukai.selfPairing (LinearMap.mul ℚ ℚ) (V.ring.degree (P.cls ^ 2) * ↑(V.rank E), degH V P E, V.ring.degree (V.chComp E 2))

The tilt discriminant is the Mukai self-pairing, at coefficient ring ℚ with the multiplication of ℚ as the bilinear form.

The rank slot carries ∫H², exactly as it does in the (s,t) wall plane. That weighting is why discrH is the quantity Wall.NumClass.discr computes on a transported class and ∫Δ(E) is not; see WallTransport.lean, which records the mistake of reading it the other way.