Discriminants and the Hodge index on a real divisor space

Macrì--Schmidt (arXiv:1607.01262v3, Definition 6.12) attach three quadratic quantities to a class on a polarised surface:

• the discriminant Δ = (ch₁)² - 2 ch₀ ch₂, which is invariant under every B-twist;
• Δ^C_{ω,B} = Δ + C (ω · ch₁^B)², the support form of Theorem 6.13;
• \bar Δ^B_ω = (ω · ch₁^B)² - 2 ω² ch₀^B ch₂^B, the form that gives the support property on the (α,β)-plane.

Before this file the only discriminant available was the compressed one of the (s,t) branch of the wall hierarchy. Here the three forms are defined on the intrinsic ChernCharacter over an arbitrary real divisor space, and the relations between them are proved:

• discriminant_twist: Δ does not see B;
• omega_square_mul_discriminant_le_barDiscriminant: ω² Δ ≤ \bar Δ^B_ω whenever the Hodge index inequality holds at ω;
• barDiscriminant_rankOne: on B = βH, ω = αH the bar form is α² times the compressed discriminant, independently of β, and through a NumericalRealization this is α² · discrH, hence α² times the wall-plane discriminant of the transported class.

The Hodge index input

LinearAlgebra/BilinearForm/HodgeIndex.lean owns the proposition-valued Hodge index and definiteness certificates. This module consumes that neutral input for discriminants and orthogonal charge slices. Nothing here proves the certificate for a geometric surface.

• a Hodge index on a realized divisor space yields the numerical HodgeIndexStatement of BogomolovGieseker.lean, which is the same inequality restricted to first Chern classes of numerical classes;
• the numerical statement yields the inequality on realized first Chern classes only. It does not yield DivisorSpace.HodgeIndex, because it quantifies over classes E : N and not over arbitrary real divisors. The two certificates are therefore related in one direction only, and that asymmetry is the honest content of this file, not an omission.

For orthogonal slices, OrthogonalSlice.isHodge_of_hodgeIndex derives the IsHodge certificate from the Hodge index inequality plus nondegeneracy of the transverse pairing; the inequality alone gives only ≤ 0 on H^⊥, which is OrthogonalSlice.transverse_square_nonpos_of_hodgeIndex. Conversely IsHodge.index_le_B recovers the inequality on the B-fields a slice can reach. The rank-one slice is Hodge as soon as H² > 0.

What is not here

No Bogomolov inequality is proved. discriminant_nonneg_of_semistable and its consequences take BogomolovGiesekerData, the supplied datum of BogomolovGieseker.lean, and transport it; the statement 0 ≤ \bar Δ^B_ω(E) for a semistable E and arbitrary (B, ω) is obtained only under a supplied Hodge index at ω.

Orthogonal slices

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.transverse_square_nonpos_of_hodgeIndex {D : Type w} [AddCommGroup D] [Module ℝ D] {U : Type x} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (h : S.HodgeIndex T.H) (u : U) : S.pair (T.transverse u) (T.transverse u) ≤ 0

The Hodge index inequality gives nonpositive square on every transverse direction.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.isHodge_of_hodgeIndex {D : Type w} [AddCommGroup D] [Module ℝ D] {U : Type x} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (h : S.HodgeIndex T.H) (hnd : ∀ (u : U), u ≠ 0 → S.pair (T.transverse u) (T.transverse u) ≠ 0) : T.IsHodge

Hodge index plus nondegeneracy of the transverse pairing gives the IsHodge certificate. Nondegeneracy is stated as: a nonzero transverse parameter has nonzero square; it implies injectivity of transverse.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.H_pair_B {D : Type w} [AddCommGroup D] [Module ℝ D] {U : Type x} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (p : Point U) : S.pair T.H (T.parameters p).B = p.s * S.pair T.H T.H

The pairing of H with the B-field of a slice point sees only the longitudinal coefficient.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.IsHodge.index_le_B {D : Type w} [AddCommGroup D] [Module ℝ D] {U : Type x} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (hT : T.IsHodge) (p : Point U) : S.pair T.H T.H * S.pair (T.parameters p).B (T.parameters p).B ≤ S.pair T.H (T.parameters p).B ^ 2

On the B-fields of a Hodge slice the index inequality holds outright: this is the direction from IsHodge back to the inequality, on the classes the slice can reach.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.rankOne_isHodge {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (H : D) (hH : 0 < S.pair H H) : (rankOne S H).IsHodge

The rank-one slice is Hodge as soon as H² > 0: there are no transverse directions.

The three discriminants

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.discriminant {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (E : N) : ℝ

The discriminant Δ(E) = (ch₁)² - 2 ch₀ ch₂, with (ch₁)² computed by the intersection form of the divisor space.

Equations

• ch.discriminant S E = S.pair (ch.chOne E) (ch.chOne E) - 2 * ch.rank E * ch.chTwo E

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.discriminant_eq_selfPairing {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (E : N) : ch.discriminant S E = Mukai.selfPairing S.intersection (ch.rank E, ch.chOne E, ch.chTwo E)

The divisorial discriminant is the Mukai self-pairing of the Chern-character triple, at coefficient ring ℝ and the divisor space's own intersection form.

This is the leaf that fixes the arity: the middle summand here is D, an arbitrary real divisor space, not a copy of ℝ. The root generalises over the coefficient ring for the sake of the ℚ- and A-valued leaves, never over the number of slots.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.discriminant_twist {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (B : D) (E : N) : (ch.twist S B).discriminant S E = ch.discriminant S E

The discriminant is invariant under every B-twist: Δ(ch^B) = Δ(ch).

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.barDiscriminant {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : ℝ

The ω-bar discriminant \bar Δ^B_ω(E) = (ω · ch₁^B)² - 2 ω² ch₀^B ch₂^B of Macrì--Schmidt Definition 6.12.

Equations

• ch.barDiscriminant S P E = S.pair P.omega ((ch.twist S P.B).chOne E) ^ 2 - 2 * S.pair P.omega P.omega * ch.rank E * (ch.twist S P.B).chTwo E

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.discriminantC {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (C : ℝ) (E : N) : ℝ

The C-discriminant Δ^C_{ω,B}(E) = Δ(E) + C (ω · ch₁^B)² of Macrì--Schmidt Definition 6.12; the constant C is the one of their Exercise 6.11 and is supplied by the caller.

Equations

• ch.discriminantC S P C E = ch.discriminant S E + C * S.pair P.omega ((ch.twist S P.B).chOne E) ^ 2

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.discriminant_le_discriminantC {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) {C : ℝ} (hC : 0 ≤ C) (E : N) : ch.discriminant S E ≤ ch.discriminantC S P C E

For C ≥ 0 the C-discriminant dominates the discriminant.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.omega_square_mul_discriminant_le_barDiscriminant {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (h : S.HodgeIndex P.omega) (E : N) : S.pair P.omega P.omega * ch.discriminant S E ≤ ch.barDiscriminant S P E

ω² Δ ≤ \bar Δ^B_ω under the Hodge index inequality at ω. This is the step by which Macrì--Schmidt pass from Bogomolov's Δ ≥ 0 to the support form on the (α,β)-plane.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.barDiscriminant_nonneg_of_discriminant_nonneg {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (h : S.HodgeIndex P.omega) (E : N) (hΔ : 0 ≤ ch.discriminant S E) : 0 ≤ ch.barDiscriminant S P E

A nonnegative discriminant gives a nonnegative bar discriminant at every (B, ω) with the Hodge index inequality at ω.

The compressed discriminant and the rank-one slice

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.discr {N : Type v} [AddCommGroup N] (Dc : ChargeCoordinates N) (E : N) : ℝ

The compressed discriminant (∫H·ch₁)² - 2 (∫H²) ch₀ ∫ch₂ on charge coordinates: the shape consumed by the wall-plane Wall.NumClass.discr, with the rank slot weighted by ∫H².

Equations

• Dc.discr E = Dc.degree E ^ 2 - 2 * Dc.hyperplaneSquare * Dc.rank E * Dc.chTwo E

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.discr_eq_selfPairing {N : Type v} [AddCommGroup N] (Dc : ChargeCoordinates N) (E : N) : Dc.discr E = Mukai.selfPairing (LinearMap.mul ℝ ℝ) (Dc.hyperplaneSquare * Dc.rank E, Dc.degree E, Dc.chTwo E)

The compressed discriminant is the Mukai self-pairing with the rank slot carrying the polarisation square.

The triple is (∫H²·rk, ∫H·ch₁, ∫ch₂), not (rk, ∫H·ch₁, ∫ch₂). The ∫H² weight is what makes this the same quantity as the uncompressed ChernCharacter.discriminant on the rank-one slice, and dropping it is the error the surface transport's docstring already warns about.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.coordinatesAt_discr_eq {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) {x : ℝ} (E : N) (hc : ch.chOne E = x • H) : (ch.coordinatesAt S H).discr E = S.pair H H * ch.discriminant S E

The integral bridge: on the rank-one slice the compressed discriminant is ∫H² times the uncompressed one.

Δ_H(E) = (∫H²) · Δ(E) whenever c₁(E) is a multiple of H, which is exactly the hypothesis hc. Both sides are Mukai.selfPairing of the same root — the left at the compressed triple, the right at the divisorial one — so the whole content is where the weight goes.

The weight cannot be normalised away. The two agree on the nose only when ∫H² = 1; at any other polarisation degree they differ by that factor, and reading the compressed discriminant as the uncompressed one is the error Numerical/Stability/WallTransport.lean records having made once. The statement is confined to the rank-one slice by necessity: off it, c₁ has components orthogonal to H that the compression discards, so no factor relates the two.

The companion statement on the pairings rather than the discriminants belongs to the bridge epic beside Mukai.realPairing; this is the discriminant-level form, and that one should be stated against it rather than re-derived.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.barDiscriminant_rankOne {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) (alpha beta : ℝ) (E : N) : ch.barDiscriminant S (StabilityParameters.rankOne H alpha beta) E = alpha ^ 2 * (ch.coordinatesAt S H).discr E

On the rank-one slice B = βH, ω = αH the bar discriminant is α² times the compressed discriminant at H, and does not depend on β.