Documentation

DerivedAlgGeo.AlgebraicGeometry.Numerical.GrothendieckGroup.Discriminant

The numerical discriminant in arbitrary dimension #

The Bogomolov discriminant is built from the first two components of the Chern character, so its definition does not depend on the dimension of the ambient variety. Surface geometry is where its degree enters the Bogomolov--Gieseker inequality, but the class itself belongs to the dimension-general numerical API.

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

The numerical discriminant Δ(E) = ch₁(E)² - 2 rank(E) ch₂(E).

It is defined for a numerical variety of any dimension. When n < 2, its membership in the second graded piece forces it to vanish; when n = 2, its degree is the quantity appearing in the Bogomolov--Gieseker inequality.

Equations
Instances For
    source
    theorem AlgebraicGeometry.Numerical.NumericalVarietyData.discriminant_eq_selfPairing {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) :
    V.discriminant E = Mukai.selfPairing (LinearMap.mul A A) ((algebraMap ℚ A) ↑(V.rank E), V.chComp E 1, V.chComp E 2)

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

    This is one of the three leaves that forced the root to move: it is A-valued, not ℝ-valued, and a ℤ-only or ℝ-only pairing could not parent it. Nothing else about the root changes — the arity is still three and the triple is (rank, ch₁, ch₂) with the rank pushed into A along ℚ → A.

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

    The discriminant lives in codimension two, independently of the ambient dimension.

    source
    theorem AlgebraicGeometry.Numerical.NumericalVarietyData.degree_discriminant {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n 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)

    Integrating the discriminant pulls its scalar coefficient outside the degree map.