Reconstructed Hirzebruch--Riemann--Roch through dimension four #
This file implements the higher-dimensional route selected in issue #45. The route is numerical rather than cycle-valued:
- Snapper polynomiality supplies the Picard Euler polynomial of every coherent sheaf;
PairingContext.ReconstructionDatarepresents its homogeneous coefficients as the Todd-weighted componentstau_i(F)in a chosen numerical ring;- the structure sheaf supplies the positive-degree Todd components;
- the triangular identities from
Intersection/ChernCharacter/Basicrecoverch_i(F); and - the top identity
degree (tau_d(F)) = chi(F)proves HRR.
The construction is valid in every positive dimension at most four. In particular it gives
scheme-derived NumericalVarietyData bridges in dimensions three and four and makes the existing
Layer A display formulas unconditional once the explicit reconstruction packages below are
supplied.
Trust and scope boundary #
PairingContext keeps representability and separation by divisor products explicit. This is
necessary: products of divisors need not separate all middle-codimension classes on an arbitrary
higher-dimensional variety. The Todd components constructed here are therefore
divisor-numerical representatives reconstructed from chi, not cycle-valued Chow classes.
No splitting principle, deformation to the normal cone, or Grothendieck--Riemann--Roch theorem is required for this numerical HRR statement. Such input would still be required to identify these representatives with Chern-polynomial expressions in a geometrically constructed tangent bundle. The upper bound four is exactly the current bound of the triangular Chern-character implementation; arbitrary dimension requires extending that universal recursion, not adding a new HRR axiom.
The top reconstructed component #
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.reconstruction_eulerPic_one
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{F : Coh X}
(Q : P.ReconstructionData 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.HigherDimension.degree_tauComponent_top_eq_eulerCharacteristic
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{F : Coh X}
(Q : P.ReconstructionData F)
:
In every dimension, the degree of the top reconstructed Todd-weighted component is the coherent Euler characteristic.
Reconstructed Todd components and the top convolution #
noncomputable def
AlgebraicGeometry.RiemannRoch.HigherDimension.reconstructedToddComponent
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
:
ℕ → A
The reconstructed Todd component, normalized to td₀ = 1. Positive components are the
Todd-weighted representatives reconstructed from the structure sheaf.
Equations
Instances For
@[simp]
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.reconstructedToddComponent_zero
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
:
@[simp]
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.reconstructedToddComponent_succ
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(i : ℕ)
:
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.reconstructedToddComponent_mem
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(i : ℕ)
:
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.sheaf_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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(hdpos : 1 ≤ d)
(hd4 : d ≤ 4)
(F : Coh X)
:
↑(D.eulerCharacteristic F) = P.ring.degree
((∑ i ∈ Finset.range (d + 1), IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) i) * ∑ j ∈ Finset.range (d + 1), reconstructedToddComponent RO j)
Reconstructed HRR for every coherent sheaf in every positive dimension at most four.
The numerical variety and its low-dimensional bridges #
noncomputable def
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
:
The total reconstructed Chern character as an additive homomorphism on K₀(Coh X).
Equations
- AlgebraicGeometry.RiemannRoch.HigherDimension.totalChernCharacterHom RO R = ∑ i ∈ Finset.range (d + 1), R.chernCharacterHom RO i
Instances For
noncomputable def
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
:
A
The total reconstructed Todd representative through the geometric dimension.
Equations
Instances For
noncomputable def
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
:
The reconstructed right side of HRR as an additive homomorphism on K₀(Coh X).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
:
The cohomological Euler homomorphism cast from ℤ to ℚ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(F : Coh X)
:
(totalChernCharacterHom RO R) (CategoryTheory.K₀Ab.of F) = ∑ i ∈ Finset.range (d + 1), IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) i
@[simp]
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(F : Coh X)
:
(riemannRochHom RO R) (CategoryTheory.K₀Ab.of F) = P.ring.degree
((∑ i ∈ Finset.range (d + 1), IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) i) * ∑ j ∈ Finset.range (d + 1), reconstructedToddComponent RO j)
@[simp]
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
(F : Coh X)
:
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(hdpos : 1 ≤ d)
(hd4 : d ≤ 4)
(E : CategoryTheory.K₀Ab (Coh X))
:
↑((D.grothendieckEulerHom C) E) = P.ring.degree
((∑ i ∈ Finset.range (d + 1), (R.chernCharacterHom RO i) E) * ∑ j ∈ Finset.range (d + 1), reconstructedToddComponent RO j)
Reconstructed HRR descends from coherent sheaves to every virtual Grothendieck class.
@[reducible]
noncomputable def
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
:
The scheme-derived numerical variety reconstructed from Picard Euler polynomials.
This constructor only selects data. The positive-dimension and codimension-four implementation
bounds occur on toNumericalVariety_satisfiesHRR, where they are actually needed.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(hdpos : 1 ≤ d)
(hd4 : d ≤ 4)
:
(toNumericalVariety RO R).SatisfiesHRR
The reconstructed numerical presentation satisfies HRR.
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(F : Coh X)
:
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(F : Coh X)
(i : ℕ)
:
@[simp]
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(i : ℕ)
:
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(F : Coh X)
:
noncomputable def
AlgebraicGeometry.RiemannRoch.HigherDimension.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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : IntersectionTheory.ChernCharacter.PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
(F : Coh X)
:
The numerical class of a coherent sheaf in the Euler-radical quotient fixed by Layer A.
Equations
Instances For
Explicit threefold and fourfold constructors #
@[reducible]
noncomputable def
AlgebraicGeometry.RiemannRoch.HigherDimension.toThreefoldNumericalVariety
{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 3 A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
:
The scheme-derived dimension-three bridge requested by issue #45.
Equations
Instances For
@[reducible]
noncomputable def
AlgebraicGeometry.RiemannRoch.HigherDimension.toFourfoldNumericalVariety
{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 4 A}
{O : Coh X}
(RO : P.ReconstructionData O)
(R : ReconstructionSystem)
:
The scheme-derived dimension-four bridge requested by issue #45.
Equations
Instances For
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.threefold_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}
{B : Type v}
[CommRing B]
[Algebra ℚ B]
{P3 : IntersectionTheory.ChernCharacter.PairingContext D C 3 B}
{O3 : Coh X}
(RO : P3.ReconstructionData O3)
(R : ReconstructionSystem)
(F : Coh X)
:
↑(D.eulerCharacteristic F) = ↑(R.reconstruction F).rank * P3.ring.degree (reconstructedToddComponent RO 3) + P3.ring.degree
(IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 1 * reconstructedToddComponent RO 2) + P3.ring.degree
(IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 2 * reconstructedToddComponent RO 1) + P3.ring.degree (IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 3)
The existing Layer A threefold display, evaluated on a genuine coherent sheaf through the scheme-derived bridge.
theorem
AlgebraicGeometry.RiemannRoch.HigherDimension.fourfold_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}
{B : Type v}
[CommRing B]
[Algebra ℚ B]
{P4 : IntersectionTheory.ChernCharacter.PairingContext D C 4 B}
{O4 : Coh X}
(RO : P4.ReconstructionData O4)
(R : ReconstructionSystem)
(F : Coh X)
:
↑(D.eulerCharacteristic F) = ↑(R.reconstruction F).rank * P4.ring.degree (reconstructedToddComponent RO 4) + P4.ring.degree
(IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 1 * reconstructedToddComponent RO 3) + P4.ring.degree
(IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 2 * reconstructedToddComponent RO 2) + P4.ring.degree
(IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 3 * reconstructedToddComponent RO 1) + P4.ring.degree (IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) 4)
The existing Layer A fourfold display, evaluated on a genuine coherent sheaf through the scheme-derived bridge.