Discriminants of a realized numerical surface

CentralCharge/Divisorial/Discriminant.lean owns the Macrì--Schmidt quadratic forms (arXiv:1607.01262v3, Definition 6.12) on an abstract real divisor space, and the DivisorSpace.HodgeIndex certificate. This file is their geometric adapter: it reads those forms off a NumericalRealization of a rational numerical intersection ring and connects them to the numerical data of BogomolovGieseker.lean.

The two Hodge certificates are related in one direction only. A DivisorSpace.HodgeIndex on the realized divisor space yields the numerical HodgeIndexStatement, because the latter is the former restricted to first Chern classes of numerical classes. The converse is false as stated: HodgeIndexStatement quantifies over classes E : N, not over arbitrary real divisors, so it yields only index_le_chOne_of_hodgeIndexStatement. That asymmetry is deliberate and is the honest content of this file.

Bogomolov--Gieseker enters only as the supplied BogomolovGiesekerData of BogomolovGieseker.lean; nothing here proves an inequality about sheaves.

Through a numerical realization

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.pair_chOne_self {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (E : N) : R.divisorSpace.pair (R.chernCharacter.chOne E) (R.chernCharacter.chOne E) = ↑(V.ring.degree (V.chComp E 1 * V.chComp E 1))

The realized first Chern class has the rational self-intersection.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.discriminant_chernCharacter {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (E : N) : R.chernCharacter.discriminant R.divisorSpace E = ↑(V.ring.degree (V.discriminant E))

The intrinsic discriminant of the realized character is the integrated numerical discriminant ∫Δ(E).

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.hodgeIndexStatement_of_hodgeIndex {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (h : R.divisorSpace.HodgeIndex (R.realizePolarization P)) : HodgeIndexStatement V P

A Hodge index inequality on the realized divisor space yields the numerical HodgeIndexStatement: the latter is the former restricted to first Chern classes of numerical classes.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.index_le_chOne_of_hodgeIndexStatement {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (hI : HodgeIndexStatement V P) (E : N) : R.divisorSpace.pair (R.realizePolarization P) (R.realizePolarization P) * R.divisorSpace.pair (R.chernCharacter.chOne E) (R.chernCharacter.chOne E) ≤ R.divisorSpace.pair (R.realizePolarization P) (R.chernCharacter.chOne E) ^ 2

The numerical HodgeIndexStatement yields the index inequality on realized first Chern classes. It does not yield DivisorSpace.HodgeIndex, which quantifies over every real class.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.discriminant_nonneg_of_semistable {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) {E : N} (B : BogomolovGiesekerData V P) (hE : B.Semistable E) : 0 ≤ R.chernCharacter.discriminant R.divisorSpace E

Bogomolov--Gieseker, transported: the intrinsic discriminant of a semistable class is nonnegative. BogomolovGiesekerData is the supplied datum; nothing is proved about sheaves.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.barDiscriminant_nonneg_of_semistable {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) {E : N} (B : BogomolovGiesekerData V P) (hE : B.Semistable E) (Q : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters D) (h : R.divisorSpace.HodgeIndex Q.omega) : 0 ≤ R.chernCharacter.barDiscriminant R.divisorSpace Q E

The bar discriminant of a semistable class is nonnegative at every (B, ω) with a Hodge index at ω. This is the Bogomolov half of Macrì--Schmidt Theorem 6.13 for slope-semistable classes; the Bridgeland semistable half is not stated here.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.barDiscriminant_rankOneParameters {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (p : ℝ × ℝ) (E : N) : R.chernCharacter.barDiscriminant R.divisorSpace (R.rankOneParameters P p) E = p.2 ^ 2 * ↑(discrH V P E)

On the rank-one slice B = sH, ω = tH of a realized polarisation the bar discriminant is t² · discrH.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.barDiscriminant_rankOneParameters_eq_discr_toNumClass {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (p : ℝ × ℝ) (E : N) : R.chernCharacter.barDiscriminant R.divisorSpace (R.rankOneParameters P p) E = p.2 ^ 2 * (toNumClass V P E).discr

The same, against the wall-plane discriminant of the transported class: the bar discriminant on the (s,t) slice is t² times Wall.NumClass.discr (toNumClass V P E).

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.barDiscriminant_rankOneParameters_nonneg {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [AddCommGroup D] [Module ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) {E : N} (B : BogomolovGiesekerData V P) (hI : HodgeIndexStatement V P) (hE : B.Semistable E) (p : ℝ × ℝ) : 0 ≤ R.chernCharacter.barDiscriminant R.divisorSpace (R.rankOneParameters P p) E

On the rank-one slice the bar discriminant of a semistable class is nonnegative from the numerical data alone: BogomolovGiesekerData and the numerical HodgeIndexStatement, with no real Hodge index at ω required.