Geometric assembly of the surface numerical variety

This file closes the surface bridge from the geometric Todd and reconstruction data to the Layer A NumericalVarietyData interface.

The crucial all-coherent HRR theorem comes from reconstruction, not from an unproved global resolution theorem. For every coherent sheaf, the degree of its reconstructed top Todd-weighted component is its Euler characteristic, while triangular extraction identifies that component with the degree-two part of ch(F) td(X). The explicit-perfect dévissage API then supplies the classical rank/c₁/c₂ interpretation whenever a two-term finite locally free resolution is actually present.

Reconstruction computes the geometric Euler characteristic

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.reconstruction_eulerPic_one {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} {F : Coh X} (Q : P.ReconstructionData F) : Q.twists.eulerPic 1 = D.eulerCharacteristic F

The Picard Euler function in any reconstruction package takes the trivial class to the actual Euler characteristic of its coherent sheaf.

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.degree_tauComponent_two_eq_eulerCharacteristic {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} {F : Coh X} (Q : P.ReconstructionData F) : P.ring.degree (Q.tauComponent 2) = ↑(D.eulerCharacteristic F)

The degree of the top reconstructed Todd-weighted component is the coherent Euler characteristic.

The concrete geometric HRR datum

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.sheaf_hirzebruch_riemannRoch {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} (T : ToddData.Data P K) (R : ReconstructionSystem) (F : Coh X) : ↑(D.eulerCharacteristic F) = P.ring.degree ((∑ i ∈ Finset.range 3, IntersectionTheory.ChernCharacter.chernCharacterComponent T.structureData (R.reconstruction F) i) * ∑ j ∈ Finset.range 3, ToddData.toddComponent T j)

Surface HRR for a coherent sheaf, proved from its reconstruction data and the geometrically constructed Todd components.

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.Assembly.toGeometricData {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} (T : ToddData.Data P K) (R : ReconstructionSystem) : GeometricData T.structureData R

The concrete geometric input to the surface numerical-variety assembly. The theorem above supplies its separate HRR witness rather than adding proof data here.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.toGeometricData_satisfiesSheafHRR {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} (T : ToddData.Data P K) (R : ReconstructionSystem) : GeometricData.SatisfiesSheafHRR T.structureData (toGeometricData T R)

The constructed geometric data satisfies sheaf-level HRR.

@[reducible]

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.Assembly.toNumericalVariety {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} (T : ToddData.Data P K) (R : ReconstructionSystem) : Numerical.NumericalVarietyData 2 A (CategoryTheory.K₀Ab (Coh X))

The scheme-derived numerical surface obtained from the concrete Todd and reconstruction data.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.toNumericalVariety_satisfiesHRR {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} (T : ToddData.Data P K) (R : ReconstructionSystem) : (toNumericalVariety T R).SatisfiesHRR

The assembled numerical presentation satisfies HRR.

Explicit-perfect comparison with dévissage

structure AlgebraicGeometry.RiemannRoch.Surface.Assembly.PerfectReconstructionComparison {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} (T : ToddData.Data P K) (R : ReconstructionSystem) (F : Coh X) : Type (u + 1)

Compatibility data between the twist-polynomial reconstruction of one coherent sheaf and an actually supplied two-term finite locally free resolution. No resolution is inferred from coherence.

• resolution : F.TwoTermPerfectDeterminantData
• rank_eq : (R.reconstruction F).rank = IntersectionTheory.ChernCharacterSurface.virtualRank self.resolution
• firstChern_eq : IntersectionTheory.ChernCharacter.chernCharacterComponent T.structureData (R.reconstruction F) 1 = P.divisorClass (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass self.resolution)

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.perfect_rank_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} (T : ToddData.Data P K) (R : ReconstructionSystem) (F : Coh X) (Q : PerfectReconstructionComparison T R F) : (R.reconstruction F).rank = IntersectionTheory.ChernCharacterSurface.virtualRank Q.resolution

The reconstructed rank of an explicitly perfect coherent sheaf is its virtual rank.

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.perfect_toddTwo_degree {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} (T : ToddData.Data P K) : P.ring.degree (ToddData.toddComponent T 2) = ↑(P.intersection.eulerPic 1)

The top Todd term in the assembled numerical surface is χ(O_X).

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.perfect_toddOne_degree {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} (T : ToddData.Data P K) (R : ReconstructionSystem) (F : Coh X) (Q : PerfectReconstructionComparison T R F) : P.ring.degree (IntersectionTheory.ChernCharacter.chernCharacterComponent T.structureData (R.reconstruction F) 1 * ToddData.toddComponent T 1) = (IntersectionTheory.ChernCharacterSurface.toddOnePairing P.intersection) (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q.resolution)

The mixed ch₁ td₁ term of an explicitly perfect coherent sheaf is its classical Todd-one pairing.

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.perfect_chTwo_degree {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} (T : ToddData.Data P K) (R : ReconstructionSystem) (F : Coh X) (Q : PerfectReconstructionComparison T R F) : P.ring.degree (IntersectionTheory.ChernCharacter.chernCharacterComponent T.structureData (R.reconstruction F) 2) = IntersectionTheory.ChernCharacterSurface.chernCharacterTwoDegree P.intersection Q.resolution

The reconstructed ch₂ term of an explicitly perfect coherent sheaf has the classical degree computed by its supplied two-term resolution.

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.perfect_surface_expansion {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} (T : ToddData.Data P K) (R : ReconstructionSystem) (F : Coh X) (Q : PerfectReconstructionComparison T R F) : ↑(D.eulerCharacteristic F) = ↑(IntersectionTheory.ChernCharacterSurface.virtualRank Q.resolution) * ↑(P.intersection.eulerPic 1) + (IntersectionTheory.ChernCharacterSurface.toddOnePairing P.intersection) (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q.resolution) + IntersectionTheory.ChernCharacterSurface.chernCharacterTwoDegree P.intersection Q.resolution

On an explicitly perfect coherent sheaf, the assembled surface expansion is exactly the rank/Todd/ch₂ expansion supplied by geometric dévissage.

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.perfect_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} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C 2 A} {K : SmoothProperVariety.CanonicalSheafData k X 2} (T : ToddData.Data P K) (R : ReconstructionSystem) (F : Coh X) (Q : PerfectReconstructionComparison T R F) : ↑(D.eulerCharacteristic F) = ↑(IntersectionTheory.ChernCharacterSurface.virtualRank Q.resolution) * ↑(P.intersection.eulerPic 1) + (↑((P.intersection.surfaceIntersectionPairing (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q.resolution)) (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q.resolution)) - ↑((P.intersection.surfaceIntersectionPairing (IntersectionTheory.ChernCharacterSurface.picardFirstChernClass Q.resolution)) K.canonicalClassAdd)) / 2 - Devissage.perfectC2Degree T Q.resolution

The termwise comparison specializes the assembled Layer A theorem to the classical rank/c₁/c₂ formula for every explicitly perfect coherent sheaf.

Geometric K3 specialization

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.toIsK3 {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} (T : ToddData.Data P K) (R : ReconstructionSystem) (hK : K.canonicalClass = 1) (hchi : P.intersection.eulerPic 1 = 2) : Numerical.K3.IsK3 (toNumericalVariety T R)

Trivial canonical class and χ(O_X)=2 prove the Layer A K3 property for the scheme-derived numerical surface.

theorem AlgebraicGeometry.RiemannRoch.Surface.Assembly.k3_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} (T : ToddData.Data P K) (R : ReconstructionSystem) (hK : K.canonicalClass = 1) (hchi : P.intersection.eulerPic 1 = 2) (F : Coh X) : ↑(D.eulerCharacteristic F) = 2 * ↑(R.reconstruction F).rank + P.ring.degree (IntersectionTheory.ChernCharacter.chernCharacterComponent T.structureData (R.reconstruction F) 2)

The geometric K3 hypotheses turn the assembled Layer A formula into the K3 Euler formula for every coherent sheaf.