The dual involution on a numerical intersection ring #

(-)^∨ acts on the codimension-i part of A^•(X)_ℚ by (-1)^i. It is what turns Hirzebruch–Riemann–Roch into its bilinear form χ(E,F) = ∫_X ch(E)^∨ · ch(F) · td(X), and so it is the last piece of Layer A that Bridgeland stability needs: the central charge factors through N(X) modulo the radical of that pairing.

Why a separate data bundle #

NumericalRingDualData R is an explicit extension of one selected presentation R : NumericalRingData n A, not a field of every numerical ring and not an independent bundle with another path back to R. A ring that has no chosen dual needs no placeholder, while two choices can coexist without instance search selecting between them.

Main definitions #

NumericalRingDualData R — the involution, as data plus the axiom that it acts by (-1)^i on piece i.
chDual E — ch(E)^∨, written directly as Σᵢ (-1)ⁱ chᵢ(E) rather than as dual (ch E).

Main results #

dual_ch — the two descriptions of ch(E)^∨ agree.
dual_involutive_of_mem_piece — (-)^∨ is an involution on each graded piece.

Deliberately not stated #

dual (dual x) = x for arbitrary x, and degree (dual x) = (-1)^n · degree x. Both are true, and both need the graded decomposition of x — NumericalRingData.isInternal — rather than just membership in a single piece. Nothing downstream needs them: every consumer here reaches dual through chComp and toddComp, which are graded by construction, so the component-wise lemmas suffice. Adding the general versions means importing DirectSum.IsInternal machinery for no current gain.

source

structure AlgebraicGeometry.Numerical.NumericalRingDualData {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] (R : NumericalRingData n A) :

Type u

The dual involution on a numerical intersection ring: a ℚ-algebra endomorphism acting on codimension i by (-1)^i.

Geometrically this is E ↦ E^∨ read through the Chern character: chᵢ(E^∨) = (-1)ⁱchᵢ(E). It is carried as data because NumericalRingData does not expose the graded projections, so there is nothing to define it from at this layer.

dual : A →ₐ[ℚ ] A
The involution, as a ℚ-algebra map.
dual_of_mem_piece {i : ℕ} {x : A} : x ∈ R.piece i → self.dual x = (-1) ^ i • x
It acts on codimension i by (-1)^i.

Instances For

source

theorem AlgebraicGeometry.Numerical.NumericalRingDualData.dual_mem_piece {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] {R : NumericalRingData n A} (D : NumericalRingDualData R) {i : ℕ} {x : A} (hx : x ∈ R.piece i) :

D.dual x ∈ R.piece i

(-)^∨ preserves each graded piece: it only rescales it.

source

theorem AlgebraicGeometry.Numerical.NumericalRingDualData.dual_involutive_of_mem_piece {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] {R : NumericalRingData n A} (D : NumericalRingDualData R) {i : ℕ} {x : A} (hx : x ∈ R.piece i) :

D.dual (D.dual x) = x

(-)^∨ is an involution on each graded piece.

source

theorem AlgebraicGeometry.Numerical.NumericalRingDualData.dual_algebraMap {n : ℕ} {A : Type u} [CommRing A] [Algebra ℚ A] {R : NumericalRingData n A} (D : NumericalRingDualData R) (q : ℚ) :

D.dual ((algebraMap ℚ A) q) = (algebraMap ℚ A) q

Scalars are fixed by (-)^∨, since they sit in codimension zero.

source

theorem AlgebraicGeometry.Numerical.NumericalVarietyData.ch_add {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E F : N) :

V.ch (E + F) = V.ch E + V.ch F

The Chern character is additive, componentwise additivity summed up.

Stated before the dual is in scope because it has nothing to do with it.

source

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

The dual Chern character ch(E)^∨ = Σᵢ (-1)ⁱ chᵢ(E).

Defined from the grading alone, with no NumericalRingDualData argument in sight: the alternating sum is available on any NumericalVarietyData, and dual_ch below is what says it deserves the name. Everything the Euler pairing needs lives at this level of generality.

Equations