Bogomolov--Gieseker gives the support property on a realized surface

Support/Divisorial.lean proves that the C-discriminant, bundled as a QuadraticForm ℝ on the real Mukai extension, is negative on every nonzero class of vanishing charge, provided the intersection form is negative definite on ω^⊥. What it leaves open is the other half of Support.IsCompatible: nonnegativity of that form on the locus of classes one actually wants a support property for.

This file closes it for slope-semistable classes of a realized numerical surface, and the closing input is exactly the one the repository already isolates as unproved. BogomolovGiesekerData supplies ∫Δ(E) ≥ 0 for a semistable E; discriminant_le_discriminantC upgrades that to Δ^C ≥ 0 for C ≥ 0; and hasQuadraticSupportProperty_image transports it along the class map.

What the two hypotheses are

• BogomolovGiesekerData is supplied, not proved. Nothing below asserts an inequality about sheaves, and the trust boundary is unchanged.
• DivisorSpace.HodgeDefinite is supplied, not proved. It is the Hodge index theorem in the form the support property needs — negative definiteness on ω^⊥, not merely the inequality H²x² ≤ (H·x)². On a smooth projective surface with ω ample it is true; this repository does not prove it, and hodgeIndexStatement_of_hodgeDefinite records that it is the stronger of the two certificates already in the library.

What is not claimed

Nothing here says the resulting Z is a Bridgeland stability condition, or that the semistable locus is the set of semistable objects of a heart. The support property is a statement about a linear charge and a set of classes, and that is all that is proved.

The stronger Hodge certificate

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.hodgeIndexStatement_of_hodgeDefinite {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.HodgeDefinite (R.realizePolarization P)) : HodgeIndexStatement V P

Negative definiteness on ω^⊥ yields the numerical HodgeIndexStatement, through the weaker inequality certificate. This is what places HodgeDefinite above HodgeIndex in the same one-directional ladder DivisorialDiscriminant.lean describes.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.discriminantC_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) {C : ℝ} (hC : 0 ≤ C) : 0 ≤ R.chernCharacter.discriminantC R.divisorSpace Q C E

Δ^C is nonnegative on the slope-semistable locus for every C ≥ 0.

This is Bogomolov--Gieseker plus discriminant_le_discriminantC; the first is supplied and the second is proved.

The support property

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.hasQuadraticSupportProperty_semistable {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [NormedAddCommGroup D] [NormedSpace ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) (B : BogomolovGiesekerData V P) (Q : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters D) (hω : R.divisorSpace.HodgeDefinite Q.omega) {C : ℝ} (hC : 0 ≤ C) : CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasQuadraticSupportProperty (R.divisorSpace.realCentralCharge Q) (⇑R.chernCharacter.toRealExtension '' {E : N | B.Semistable E})

The divisorial charge has the support property on the slope-semistable locus.

The quadratic form is the C-discriminant of Macrì--Schmidt Definition 6.12, bundled on the real Mukai extension. Its nonnegativity on the locus is Bogomolov--Gieseker, supplied by BogomolovGiesekerData; its negativity on the kernel of the charge is proved from HodgeDefinite in Support/Divisorial.lean.

This is the Kontsevich--Soibelman support property in the form Weak/Support/Predicate/Quadratic.lean states it, for the charge of an arbitrary (B, ω) with ω in the positive cone.

theorem AlgebraicGeometry.Numerical.Surface.NumericalRealization.hasSupportProperty_semistable {A : Type u} {N : Type v} {D : Type w} [CommRing A] [Algebra ℚ A] [AddCommGroup N] [NormedAddCommGroup D] [NormedSpace ℝ D] {V : NumericalVarietyData 2 A N} (R : NumericalRealization V.ring) (P : Polarization V.ring) [FiniteDimensional ℝ D] (B : BogomolovGiesekerData V P) (Q : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters D) (hω : R.divisorSpace.HodgeDefinite Q.omega) {C : ℝ} (hC : 0 ≤ C) : CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasSupportProperty (R.divisorSpace.realCentralCharge Q) (⇑R.chernCharacter.toRealExtension '' {E : N | B.Semistable E})

The same conclusion in the norm-bound formulation of Support.HasSupportProperty, which is the shape the stability-condition interfaces consume.