Surface Riemann--Roch by finite locally free dévissage #
This file extends the line-bundle surface formula to the strongest honest coherent scope currently supported by the repository.
- A determinant-equipped finite locally free coherent sheaf gets degree-level
ch₂andc₂coordinates, with the classical rank/c₁/c₂Riemann--Roch formula. - Those coordinates satisfy the expected short-exact additivity and Whitney formula when the determinant and rank comparisons are supplied.
- A coherent sheaf is treated only when it carries
TwoTermPerfectDeterminantData. Itsch₂is proved to be the difference of the two finite locally free terms in that resolution.
No global resolution property or splitting principle is inferred from coherence. The current The Mathlib/DerivedAlgGeo API has no theorem producing a finite locally free resolution for every coherent sheaf on a smooth projective surface, so the perfectness certificate remains visible in every coherent theorem. Compatibility with issue #32 is recorded through the explicit geometric Grothendieck group and its Euler homomorphism.
Finite locally free coherent sheaves #
noncomputable def
AlgebraicGeometry.RiemannRoch.Surface.Devissage.locallyFreeCh2Degree
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(_T : ToddData.Data P K)
(E : F.DeterminantData)
:
The degree of ch₂ of a determinant-equipped finite locally free coherent sheaf, recovered
from its Euler characteristic and the geometric Todd terms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
AlgebraicGeometry.RiemannRoch.Surface.Devissage.locallyFreeC2Degree
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(T : ToddData.Data P K)
(E : F.DeterminantData)
:
The degree of c₂, using ch₂ = (c₁² - 2c₂)/2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.locallyFree_eulerCharacteristic_eq_ch2
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(T : ToddData.Data P K)
(E : F.DeterminantData)
:
Riemann--Roch for a finite locally free sheaf in Todd-coordinate form.
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.locallyFree_eulerCharacteristic_eq
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(T : ToddData.Data P K)
(E : F.DeterminantData)
:
↑(D.eulerCharacteristic F) = ↑E.rank * ↑(P.intersection.eulerPic 1) + (↑((P.intersection.surfaceIntersectionPairing (Scheme.Modules.DeterminantData.firstChernClassAdd E))
(Scheme.Modules.DeterminantData.firstChernClassAdd E)) - ↑((P.intersection.surfaceIntersectionPairing (Scheme.Modules.DeterminantData.firstChernClassAdd E))
K.canonicalClassAdd)) / 2 - locallyFreeC2Degree T E
Classical finite locally free surface formula
χ(E) = rχ(O_X) + (c₁²-c₁K_X)/2 - c₂.
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.locallyFreeCh2Degree_shortExact
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{S : CategoryTheory.ShortComplex (Coh X)}
(T : ToddData.Data P K)
(E : Coh.ShortExactDeterminantData S)
(hrank : E.middle.rank = E.left.rank + E.right.rank)
:
Degree-level ch₂ is additive in a determinant-compatible short exact sequence of finite
locally free coherent sheaves, once the chosen fixed ranks are explicitly compatible.
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.locallyFreeC2Degree_shortExact
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{S : CategoryTheory.ShortComplex (Coh X)}
(T : ToddData.Data P K)
(E : Coh.ShortExactDeterminantData S)
(hrank : E.middle.rank = E.left.rank + E.right.rank)
:
The degree-level Whitney formula
c₂(E₂)=c₂(E₁)+c₂(E₃)+c₁(E₁)c₁(E₃).
Explicit two-term perfect resolutions #
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.picardFirstChernClass_eq_middle_sub_left
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{F : Coh X}
(Q : F.TwoTermPerfectDeterminantData)
:
The virtual first Chern class is the difference of the two finite locally free terms.
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.eulerCharacteristic_eq_middle_sub_left
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{F : Coh X}
(C : D.LinearConnectingSystem)
(Q : F.TwoTermPerfectDeterminantData)
:
Euler dévissage along the recorded finite locally free resolution.
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.chernCharacterTwoDegree_eq_middle_sub_left
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(T : ToddData.Data P K)
(Q : F.TwoTermPerfectDeterminantData)
:
The reconstructed ch₂ of a perfect coherent sheaf is the difference of the ch₂ values
of the two finite locally free terms in its recorded resolution.
noncomputable def
AlgebraicGeometry.RiemannRoch.Surface.Devissage.perfectC2Degree
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(_T : ToddData.Data P K)
(Q : F.TwoTermPerfectDeterminantData)
:
The degree of the second Chern class of a perfect coherent sheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.perfect_eulerCharacteristic_eq_ch2
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(T : ToddData.Data P K)
(Q : F.TwoTermPerfectDeterminantData)
:
↑(D.eulerCharacteristic F) = ↑(IntersectionTheory.ChernCharacterSurface.virtualRank Q) * ↑(P.intersection.eulerPic 1) - ↑((P.intersection.surfaceIntersectionPairing (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q))
K.canonicalClassAdd) / 2 + IntersectionTheory.ChernCharacterSurface.chernCharacterTwoDegree P.intersection Q
Surface Riemann--Roch for a coherent sheaf with an explicit two-term finite locally free
resolution, in rank/c₁/ch₂ form.
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.perfect_eulerCharacteristic_eq
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(T : ToddData.Data P K)
(Q : F.TwoTermPerfectDeterminantData)
:
↑(D.eulerCharacteristic F) = ↑(IntersectionTheory.ChernCharacterSurface.virtualRank Q) * ↑(P.intersection.eulerPic 1) + (↑((P.intersection.surfaceIntersectionPairing (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q))
(IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q)) - ↑((P.intersection.surfaceIntersectionPairing
(IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q))
K.canonicalClassAdd)) / 2 - perfectC2Degree T Q
Classical rank/c₁/c₂ surface formula for explicitly perfect coherent sheaves.
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.discriminantDegree_eq_c2
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(T : ToddData.Data P K)
(Q : F.TwoTermPerfectDeterminantData)
:
IntersectionTheory.ChernCharacterSurface.discriminantDegree P.intersection Q = 2 * ↑(IntersectionTheory.ChernCharacterSurface.virtualRank Q) * perfectC2Degree T Q - (↑(IntersectionTheory.ChernCharacterSurface.virtualRank Q) - 1) * ↑((P.intersection.surfaceIntersectionPairing (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q))
(IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q))
The discriminant in c₂ form:
Δ = 2r c₂ - (r-1)c₁².
Grothendieck-group compatibility #
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.grothendieckEulerHom_class_eq_perfect_formula
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A}
{K : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(T : ToddData.Data P K)
(Q : F.TwoTermPerfectDeterminantData)
:
↑((D.grothendieckEulerHom C) (CategoryTheory.K₀Ab.of F)) = ↑(IntersectionTheory.ChernCharacterSurface.virtualRank Q) * ↑(P.intersection.eulerPic 1) + (↑((P.intersection.surfaceIntersectionPairing (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q))
(IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q)) - ↑((P.intersection.surfaceIntersectionPairing
(IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q))
K.canonicalClassAdd)) / 2 - perfectC2Degree T Q
The perfect surface formula computes exactly the value of the Grothendieck Euler homomorphism on the coherent-sheaf class.
Term-by-term Layer A comparison #
structure
AlgebraicGeometry.RiemannRoch.Surface.Devissage.NumericalVarietyComparison
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{B : Type v}
[CommRing B]
[Algebra ℚ B]
{N : Type w}
[AddCommGroup N]
(V : Numerical.NumericalVarietyData 2 B N)
{PB : IntersectionTheory.ChernCharacter.PairingContext D C 2 B}
{KB : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
(Q : F.TwoTermPerfectDeterminantData)
(E : N)
:
Explicit comparison between one Layer A numerical class and the geometric data of an
explicitly perfect coherent sheaf. Each term of Numerical.Surface.chi_eq is compared
separately; no equality of characteristic classes is inferred from equality of Euler numbers.
- toddOne_degree : V.ring.degree (V.chComp E 1 * V.toddComp 1) = (IntersectionTheory.ChernCharacterSurface.toddOnePairing PB.intersection) (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q)
- chTwo_degree : V.ring.degree (V.chComp E 2) = IntersectionTheory.ChernCharacterSurface.chernCharacterTwoDegree PB.intersection Q
Instances For
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.NumericalVarietyComparison.chi_eq_geometric_terms
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{B : Type v}
[CommRing B]
[Algebra ℚ B]
{N : Type w}
[AddCommGroup N]
(V : Numerical.NumericalVarietyData 2 B N)
{PB : IntersectionTheory.ChernCharacter.PairingContext D C 2 B}
{KB : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
{Q : F.TwoTermPerfectDeterminantData}
{E : N}
(hV : V.SatisfiesHRR)
(R : NumericalVarietyComparison V Q E)
:
↑(V.chi E) = ↑(IntersectionTheory.ChernCharacterSurface.virtualRank Q) * ↑(PB.intersection.eulerPic 1) + (IntersectionTheory.ChernCharacterSurface.toddOnePairing PB.intersection)
(IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q) + IntersectionTheory.ChernCharacterSurface.chernCharacterTwoDegree PB.intersection Q
The Layer A surface expansion becomes exactly the geometric rank/Todd/ch₂ expansion.
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.NumericalVarietyComparison.chi_eq_geometric
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{B : Type v}
[CommRing B]
[Algebra ℚ B]
{N : Type w}
[AddCommGroup N]
(V : Numerical.NumericalVarietyData 2 B N)
{PB : IntersectionTheory.ChernCharacter.PairingContext D C 2 B}
{KB : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
{Q : F.TwoTermPerfectDeterminantData}
{E : N}
(R : NumericalVarietyComparison V Q E)
:
The compared Layer A Euler homomorphism agrees with the geometric one on this class.
theorem
AlgebraicGeometry.RiemannRoch.Surface.Devissage.NumericalVarietyComparison.chi_eq_classical
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{B : Type v}
[CommRing B]
[Algebra ℚ B]
{N : Type w}
[AddCommGroup N]
(V : Numerical.NumericalVarietyData 2 B N)
{PB : IntersectionTheory.ChernCharacter.PairingContext D C 2 B}
{KB : SmoothProperVariety.CanonicalSheafData k X 2}
{F : Coh X}
{Q : F.TwoTermPerfectDeterminantData}
{E : N}
(T : ToddData.Data PB KB)
(R : NumericalVarietyComparison V Q E)
:
↑(V.chi E) = ↑(IntersectionTheory.ChernCharacterSurface.virtualRank Q) * ↑(PB.intersection.eulerPic 1) + (↑((PB.intersection.surfaceIntersectionPairing (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q))
(IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q)) - ↑((PB.intersection.surfaceIntersectionPairing
(IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q))
KB.canonicalClassAdd)) / 2 - perfectC2Degree T Q
After the explicit term comparisons, Layer A and geometric surface Riemann--Roch give the
same classical rank/c₁/c₂ formula.