A geometric numerical variety for surfaces

This file is the assembly point from the geometric surface theory to Layer A. It does two things which should not be hidden behind instances:

• an invariant of coherent sheaves which respects isomorphisms and short exact sequences is descended through the explicit Grothendieck group K₀(Coh X);
• reconstructed surface Chern characters, geometric Todd components, and geometric Hirzebruch--Riemann--Roch are packaged as a genuine NumericalVarietyData.

The construction uses K₀(Coh X) as its input group. The numerical Grothendieck group is then the Euler-radical quotient from Numerical/GrothendieckGroup/Lattice.lean; in particular the quotient and sign conventions are shared with Layer A rather than reconstructed here.

GeometricData.sheaf_hirzebruch_riemannRoch is a theorem about every coherent sheaf, not a Layer A axiom about arbitrary Grothendieck classes. The latter is proved below by descending both sides as additive invariants. Thus toNumericalVariety selects the data, while toNumericalVariety_satisfiesHRR supplies its separate HRR witness.

Reconstructed Chern characters on K₀

Surface assembly and Hirzebruch--Riemann--Roch

structure AlgebraicGeometry.RiemannRoch.Surface.GeometricData {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) (R : ReconstructionSystem) : Type v

Geometric input which assembles the coherent Grothendieck group into a Layer A numerical surface.

The sheaf-level HRR property is deliberately kept separate from this selected data. Its proof for every virtual Grothendieck class is GeometricData.hirzebruch_riemannRoch below.

• toddComponent : ℕ → A

  The geometrically constructed Todd components.

• toddComponent_mem (i : ℕ) : self.toddComponent i ∈ P.ring.piece i

  Todd components carry their geometric grading.

• toddComponent_zero : self.toddComponent 0 = 1

  The degree-zero Todd component is normalized to one.

structure AlgebraicGeometry.RiemannRoch.Surface.GeometricData.SatisfiesSheafHRR {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) : Prop

Geometric surface HRR for coherent sheaves, as a proposition-valued property of the selected geometric data.

• eq (F : Coh X) : ↑(D.eulerCharacteristic F) = P.ring.degree ((∑ i ∈ Finset.range 3, IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) i) * ∑ j ∈ Finset.range 3, G.toddComponent j)

  Geometric surface HRR for coherent sheaves.

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.GeometricData.totalChernCharacterHom {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (_G : GeometricData RO R) : CategoryTheory.K₀Ab (Coh X) →+ A

The total reconstructed Chern character as an additive homomorphism on K₀.

Equations

• AlgebraicGeometry.RiemannRoch.Surface.GeometricData.totalChernCharacterHom RO _G = ∑ i ∈ Finset.range 3, R.chernCharacterHom RO i

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.GeometricData.totalTodd {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) : A

The total geometric Todd class of the surface.

Equations

• AlgebraicGeometry.RiemannRoch.Surface.GeometricData.totalTodd RO G = ∑ j ∈ Finset.range 3, G.toddComponent j

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.GeometricData.riemannRochHom {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) : CategoryTheory.K₀Ab (Coh X) →+ ℚ

The right side of HRR, as an additive homomorphism on K₀.

Equations

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

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.GeometricData.rationalEulerHom {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (_G : GeometricData RO R) : CategoryTheory.K₀Ab (Coh X) →+ ℚ

Cast the cohomological Euler homomorphism from ℤ to ℚ.

Equations

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

@[simp]

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.totalChernCharacterHom_class {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (F : Coh X) : (totalChernCharacterHom RO G) (CategoryTheory.K₀Ab.of F) = ∑ i ∈ Finset.range 3, IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) i

@[simp]

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.riemannRochHom_class {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (F : Coh X) : (riemannRochHom RO G) (CategoryTheory.K₀Ab.of F) = P.ring.degree ((∑ i ∈ Finset.range 3, IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) i) * ∑ j ∈ Finset.range 3, G.toddComponent j)

@[simp]

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.rationalEulerHom_class {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (F : Coh X) : (rationalEulerHom RO G) (CategoryTheory.K₀Ab.of F) = ↑(D.eulerCharacteristic F)

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.hirzebruch_riemannRoch {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (hG : SatisfiesSheafHRR RO G) (E : CategoryTheory.K₀Ab (Coh X)) : ↑((D.grothendieckEulerHom C) E) = P.ring.degree ((∑ i ∈ Finset.range 3, (R.chernCharacterHom RO i) E) * ∑ j ∈ Finset.range 3, G.toddComponent j)

Geometric HRR descends from coherent sheaves to every virtual Grothendieck class.

@[reducible]

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.GeometricData.toNumericalVariety {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) : Numerical.NumericalVarietyData 2 A (CategoryTheory.K₀Ab (Coh X))

The selected scheme-derived numerical surface. Its separate HRR witness is toNumericalVariety_satisfiesHRR, proved by Grothendieck descent.

Equations

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

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.toNumericalVariety_satisfiesHRR {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (hG : SatisfiesSheafHRR RO G) : (toNumericalVariety RO G).SatisfiesHRR

The descended coherent-sheaf HRR proof supplies numerical HRR.

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.toNumericalVariety_rank_class {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (F : Coh X) : (toNumericalVariety RO G).rank (CategoryTheory.K₀Ab.of F) = (R.reconstruction F).rank

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.toNumericalVariety_chComp_class {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (F : Coh X) (i : ℕ) : (toNumericalVariety RO G).chComp (CategoryTheory.K₀Ab.of F) i = IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) i

@[simp]

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.toNumericalVariety_toddComp {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (i : ℕ) : (toNumericalVariety RO G).toddComp i = G.toddComponent i

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.toNumericalVariety_chi_class {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (F : Coh X) : (toNumericalVariety RO G).chi (CategoryTheory.K₀Ab.of F) = D.eulerCharacteristic F

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.surface_chi_class_eq {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (hG : SatisfiesSheafHRR RO G) (F : Coh X) : ↑(D.eulerCharacteristic F) = ↑(R.reconstruction F).rank * P.ring.degree (G.toddComponent 2) + P.ring.degree (IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 1 * G.toddComponent 1) + P.ring.degree (IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 2)

On a coherent-sheaf class, the Layer A surface expansion is exactly the geometric rank/ch₁/ch₂ expansion used to construct the presentation.

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.toIsK3 {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (htoddOne : G.toddComponent 1 = 0) (htoddTwo : P.ring.degree (G.toddComponent 2) = 2) : Numerical.K3.IsK3 (toNumericalVariety RO G)

The geometric K3 hypotheses give the existing Layer A K3 structure on the assembled surface.

theorem AlgebraicGeometry.RiemannRoch.Surface.GeometricData.k3_eulerCharacteristic_eq {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (hG : SatisfiesSheafHRR RO G) (htoddOne : G.toddComponent 1 = 0) (htoddTwo : P.ring.degree (G.toddComponent 2) = 2) (F : Coh X) : ↑(D.eulerCharacteristic F) = 2 * ↑(R.reconstruction F).rank + P.ring.degree (IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 2)

Under the geometric K3 hypotheses, the existing Layer A K3 Riemann--Roch theorem becomes the corresponding statement for every coherent sheaf.

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.GeometricData.numericalClass {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety 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} {O : Coh X} (RO : P.ReconstructionData O) {R : ReconstructionSystem} (G : GeometricData RO R) (F : Coh X) : (toNumericalVariety RO G).NumericalQuotient

The numerical class of a coherent sheaf: first its coherent-Grothendieck class, then the Euler-radical quotient fixed by Layer A.

Equations

• AlgebraicGeometry.RiemannRoch.Surface.GeometricData.numericalClass RO G F = Submodule.Quotient.mk (CategoryTheory.K₀Ab.of F)