The divisorial discriminant is a support form #
The charge constructors are upstream under CentralCharge/Divisorial/; this
module adds the support interpretation. Every full quadratic-support theorem
below supplies both nonnegativity on the selected locus and strict negativity
on the kernel of the same charge.
Discriminant.lean defines Δ, \bar Δ^B_ω and Δ^C_{ω,B} as functions of a
class E : N, because N is only an additive group and a QuadraticForm ℝ N
is not available there. The support property of
Weak/Support/Predicate/Quadratic.lean needs a bundled QuadraticForm ℝ V
against an ℝ-linear charge V →ₗ[ℝ] ℂ. This file supplies both on the real
Mukai extension ℝ × D × ℝ, which is the smallest real vector space the
divisorial charge factors through, and proves the two halves of
Support.IsCompatible.
The two forms #
DivisorSpace.realDiscriminantisΔ(r, c, s) = c² - 2rs, the bundled form ofChernCharacter.discriminant;DivisorSpace.realDiscriminantCaddsC · (ω · c^B)², the bundledChernCharacter.discriminantCof Macrì--Schmidt Definition 6.12, withω · c^Bsupplied by the linear functionalDivisorSpace.omegaTwistedDegree.
realDiscriminantC_toRealExtension and its siblings say these agree with the
unbundled functions along the class map, so nothing is a second definition of
the same quantity.
Why negative definiteness needs HodgeDefinite, not HodgeIndex #
On ker Z the computation is exact. Writing c^B = c - r B, vanishing of the
imaginary part says ω · c^B = 0 and vanishing of the real part pins s, and
substituting both gives
Δ^C(v) = (c^B)² - r² ω² for every C.
The C term drops because it is C (ω · c^B)², so no sign condition on C
is needed here; C ≥ 0 is what discriminant_le_discriminantC needs, which
is a different step.
The remaining input is that (c^B)² < 0 for a nonzero c^B orthogonal to ω.
DivisorSpace.HodgeIndex gives only ≤ 0 — an isotropic class in ω^⊥ would
make Δ^C vanish on a nonzero kernel vector and destroy the support property —
so the hypothesis here is the strictly stronger DivisorSpace.HodgeDefinite,
which is exactly the signature (1, ρ - 1) statement of the Hodge index
theorem rather than the inequality it implies.
What is supplied and what is proved #
Nonnegativity on the locus is supplied: it is Bogomolov--Gieseker, which
this repository does not prove. hasQuadraticSupportProperty takes it as a
hypothesis, and the numerical corollary in
AlgebraicGeometry/Numerical/Stability/DivisorialSupport.lean discharges it
from BogomolovGiesekerData. Negative definiteness on the kernel is proved.
The route deliberately avoids PeriodDomain.HasSignatureTwo (realForm b), which
Mukai/RealForm.lean records as unavailable at the pinned Mathlib; the argument
below needs only definiteness on ω^⊥, which HodgeDefinite states directly.
The bundled forms and the linear charge #
The discriminant as a genuine quadratic form on the real extension:
Δ(r, c, s) = c² - 2rs.
This is Mukai.realDiscriminant at b = S.intersection, and nothing more.
The form itself lives in Lattice/Mukai/RealForm.lean beside the pairing it is
built from: this file imports two of the discriminant leaves the form parents,
so the parent could not live here. realDiscriminant_toRealExtension below is
what pins the unhalved convention against ChernCharacter.discriminant.
Equations
Instances For
The twisted ω-degree v ↦ ω · (c - r B), as a linear functional on the
real extension. It is the linear form whose square Δ^C adds to Δ.
Equations
- S.omegaTwistedDegree P = { toFun := fun (v : Mukai.RealExtension D) => (S.intersection P.omega) (v.2.1 - v.1 • P.B), map_add' := ⋯, map_smul' := ⋯ }
Instances For
The C-discriminant as a genuine quadratic form:
Δ^C_{ω,B} = Δ + C (ω · c^B)².
Equations
- S.realDiscriminantC P C = S.realDiscriminant + C • QuadraticMap.sq.comp (S.omegaTwistedDegree P)
Instances For
The divisorial central charge as an ℝ-linear map on the real
extension. It is Mukai.expCharge, which Charge.lean already proved the
divisorial charge to be.
Equations
- S.realCentralCharge P = Mukai.expChargeLinearMap S.intersection P.B P.omega
Instances For
Agreement with the unbundled discriminants #
Not a simp lemma: toRealExtension_apply is already simp, so it rewrites
the left-hand side first and the normal-form linter rejects the attribute. The
statement is the identification that keeps the bundled and unbundled forms from
being two definitions of one quantity.
Not a simp lemma: toRealExtension_apply is already simp, so it rewrites
the left-hand side first and the normal-form linter rejects the attribute. The
statement is the identification that keeps the bundled and unbundled forms from
being two definitions of one quantity.
Not a simp lemma: toRealExtension_apply is already simp, so it rewrites
the left-hand side first and the normal-form linter rejects the attribute. The
statement is the identification that keeps the bundled and unbundled forms from
being two definitions of one quantity.
Negative definiteness on the kernel of the charge #
The imaginary part of a vanishing charge says the twisted ω-degree
vanishes.
The kernel computation. On a class of vanishing charge the
C-discriminant is (c^B)² - r² ω², independently of C.
Both halves of Z v = 0 are used: the imaginary part kills the C term and the
real part eliminates s.
Δ^C is negative on every nonzero class of vanishing charge, given the
Hodge index theorem in its definite form at ω.
No sign condition is imposed on C; the C term vanishes on the kernel.
The support property #
The divisorial charge has the quadratic support property on any locus
where the C-discriminant is nonnegative, given the Hodge index theorem in its
definite form at ω.
Nonnegativity on the locus is the supplied Bogomolov--Gieseker input; negative definiteness on the kernel is proved.
The norm-bound formulation, for consumers stated against
Support.HasSupportProperty.
The support property on the image of a locus of classes.
This is the shape a numerical consumer wants: the hypothesis is
0 ≤ Δ^C_{ω,B}(E) for classes E in the locus, which
discriminant_le_discriminantC supplies from Δ(E) ≥ 0 once C ≥ 0.