Riemann--Roch for Cartier divisors on smooth proper surfaces #
This file proves the geometric surface formula
χ(O_X(D)) = χ(O_X) + (D · (D - K_X)) / 2
from the degree-two Snapper intersection pairing and the Picard Euler symmetry supplied by Serre duality. It does not import or invoke the Layer A Hirzebruch--Riemann--Roch property.
The proof is first carried out intrinsically on Pic X. The numerator is shown to be even over
ℤ, before division by two in ℚ. It is then specialized to Cartier divisors, where
principal-equivalence invariance is formal. Finally, EffectiveSequenceRealization connects the
formula to #25's genuine coherent short exact sequence
0 → O_X(E-D) → O_X(E) → O_X(E) ⊗ i_*O_D → 0.
Coherence and the comparison between chosen Picard representatives and the displayed associated sheaves remain explicit because those closure/comparison constructors are not yet automatic in the current geometric layer.
The integral numerator in the surface divisor formula.
Equations
Instances For
Serre symmetry and bilinearity give the denominator-free surface formula.
The factor 1/2 is integral: the intersection numerator is even.
Intrinsic Picard-group surface Riemann--Roch.
The Euler characteristic of the Cartier line bundle O_X(E), through its Picard class.
Equations
Instances For
The intersection numerator E · (E-K) for a Cartier divisor.
Equations
Instances For
Surface Riemann--Roch for an arbitrary Cartier divisor.
The Cartier numerator is even before passing to rational coefficients.
Principal-equivalent Cartier divisors have the same geometric Euler characteristic.
The full Riemann--Roch expression is invariant under Cartier divisor-class equivalence.
Effective divisors and the fundamental exact sequence #
Realization data connecting #25's twisted fundamental sequence to the intrinsic Picard Euler function. The quotient term needs no additional comparison: it is the actual coherent third object of that sequence.
- sourceCoherent : X.coherent (Scheme.CartierDivisor.associatedSheaf (E - A.divisor))
- middleCoherent : X.coherent (Scheme.CartierDivisor.associatedSheaf E)
- sourceEuler : D.eulerCharacteristic (A.cohTwistSequence E ⋯ ⋯).X₁ = I.eulerPic (Scheme.CartierDivisor.toPic (E - A.divisor))
- middleEuler : D.eulerCharacteristic (A.cohTwistSequence E ⋯ ⋯).X₂ = I.eulerPic (Scheme.CartierDivisor.toPic E)
Instances For
The coherent quotient term O_X(E) ⊗ i_*O_A.
Equations
- R.quotient = (A.cohTwistSequence E ⋯ ⋯).X₃
Instances For
Euler additivity for the genuine twisted fundamental sequence.
For the effective divisor itself, the exact sequence reads
χ(O_X(A)) = χ(O_X) + χ(O_X(A)|_A).
The geometric curve/intersection comparison needed to compute the quotient term in the effective-divisor sequence. Keeping this comparison explicit isolates the remaining adjunction input from the already-constructed coherent short exact sequence.
- quotientEuler : ↑(D.eulerCharacteristic R.quotient) = ↑(cartierCorrectionNumerator I K A.divisor) / 2
Instances For
Surface Riemann--Roch for an effective divisor, obtained directly from #25's coherent fundamental sequence and the geometric intersection computation on its quotient.
The effective-divisor specialization of surface Riemann--Roch.
Combining the effective exact sequence with Riemann--Roch computes the quotient Euler characteristic as half the intersection numerator.
Normalizations and K3 specialization #
D = 0: the correction term vanishes.
D = K_X: Serre duality gives χ(O_X(K_X)) = χ(O_X).
K3 specialization: for trivial canonical class,
χ(L) = χ(O_X) + L²/2.
K3 normalization with χ(O_X)=2, matching the audited Layer A numerical formula.