Numerical Todd data for smooth proper surfaces

This file constructs the three Todd components needed by surface Riemann--Roch. The codimension-zero and codimension-one terms are the expected explicit classes

td₀ = 1, td₁ = -K_X / 2.

The top component is not postulated. It is the representative reconstructed from the structure-sheaf twist polynomial, and its degree is proved to be the geometric Euler characteristic χ(O_X). Representability of the twist functional remains explicit through PairingContext.ReconstructionData; no global Chow group or hidden existence instance is used.

The resulting component family carries the grading and normalization statements expected by NumericalVarietyData. A final comparison theorem turns geometric K3 hypotheses into a Layer A K3.IsK3 witness for any proposed NumericalVarietyData using these components.

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.homogeneousPicardCoefficient_nil {X : Scheme} (d : ℕ) (f : Scheme.Modules.Pic X → ℤ) : IntersectionTheory.ChernCharacter.homogeneousPicardCoefficient d [] f = ↑(f 1)

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.homogeneousPicardCoefficient_singleton {X : Scheme} (f : Scheme.Modules.Pic X → ℤ) (L : Scheme.Modules.Pic X) : IntersectionTheory.ChernCharacter.homogeneousPicardCoefficient 2 [L] f = 2 * ↑(f L - f 1) - ↑(f (L ^ 2) - f 1) / 2

The degree-one homogeneous coefficient of a quadratic Picard Euler function in one direction, written using its values at the first three powers.

structure AlgebraicGeometry.RiemannRoch.Surface.ToddData.Data {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) : Type (u + 1)

The explicit geometric data used to construct the surface Todd components.

The structure-sheaf representative is required to realize the same Picard Euler function as the intersection context. Serre symmetry is included because it is what identifies the linear Todd term with -K_X/2.

• structureData : P.ReconstructionData (IntersectionTheory.Number.structureSheafObject ⋯)
• structure_rank : self.structureData.rank = 1
• structure_twists : self.structureData.twists.eulerPic = P.intersection.eulerPic
• serre : Duality.Serre.Data.SurfacePicardSymmetry P.intersection K.canonicalClass

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.ToddData.numericalCanonicalClass {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} : A

The canonical divisor class inside the chosen numerical intersection ring.

Equations

• AlgebraicGeometry.RiemannRoch.Surface.ToddData.numericalCanonicalClass = P.divisorClass K.canonicalClassAdd

def AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddZero {A : Type v} [CommRing A] : A

The codimension-zero Todd component.

Equations

• AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddZero = 1

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddOne {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} : A

The codimension-one Todd component -K_X/2.

Equations

• AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddOne = -((algebraMap ℚ A) (1 / 2) * AlgebraicGeometry.RiemannRoch.Surface.ToddData.numericalCanonicalClass)

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddTwo {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 : Data P K) : A

The top Todd component reconstructed from the structure-sheaf twist polynomial.

Equations

• AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddTwo T = T.structureData.tauComponent 2

noncomputable def AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent {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 : Data P K) : ℕ → A

The surface Todd components, extended by zero above the dimension.

Equations

• AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent T 0 = AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddZero
• AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent T 1 = AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddOne
• AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent T 2 = AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddTwo T
• AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent T x✝ = 0

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.numericalCanonicalClass_mem {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} : numericalCanonicalClass ∈ P.ring.piece 1

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddZero_mem {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} : toddZero ∈ P.ring.piece 0

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddOne_mem {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} : toddOne ∈ P.ring.piece 1

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddTwo_mem {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 : Data P K) : toddTwo T ∈ P.ring.piece 2

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent_mem {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 : Data P K) (i : ℕ) : toddComponent T i ∈ P.ring.piece i

@[simp]

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent_zero {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 : Data P K) : toddComponent T 0 = 1

@[simp]

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent_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} {K : SmoothProperVariety.CanonicalSheafData k X 2} (T : Data P K) : toddComponent T 1 = toddOne

@[simp]

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent_two {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 : Data P K) : toddComponent T 2 = toddTwo T

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddComponent_eq_zero_of_two_lt {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 : Data P K) {i : ℕ} (hi : 2 < i) : toddComponent T i = 0

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.degree_toddTwo_eq_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} {K : SmoothProperVariety.CanonicalSheafData k X 2} (T : Data P K) : P.ring.degree (toddTwo T) = ↑(P.intersection.eulerPic 1)

The reconstructed top Todd component has degree χ(O_X), derived from the structure-sheaf twist polynomial rather than supplied as a Todd axiom.

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.degree_toddTwo_eq_structureSheafEulerCharacteristic {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 : Data P K) : P.ring.degree (toddTwo T) = ↑(D.eulerCharacteristic (IntersectionTheory.Number.structureSheafObject ⋯))

Geometric form of the top normalization: ∫td₂ = χ(O_X).

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.degree_numericalCanonicalClass_mul_divisorClass {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} (L : Additive (Scheme.Modules.Pic X)) : P.ring.degree (numericalCanonicalClass * P.divisorClass L) = ↑((P.intersection.surfaceIntersectionPairing K.canonicalClassAdd) L)

Realization of the intersection of the numerical canonical class with a divisor class.

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddOnePairing_eq_neg_half_canonical {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 : Data P K) (L : Additive (Scheme.Modules.Pic X)) : (IntersectionTheory.ChernCharacterSurface.toddOnePairing P.intersection) L = -↑((P.intersection.surfaceIntersectionPairing K.canonicalClassAdd) L) / 2

Serre symmetry identifies the degree-one Todd functional with -K_X/2.

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.degree_toddOne_mul_divisorClass {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 : Data P K) (L : Additive (Scheme.Modules.Pic X)) : P.ring.degree (toddOne * P.divisorClass L) = (IntersectionTheory.ChernCharacterSurface.toddOnePairing P.intersection) L

Ring-valued form of td₁ = -K_X/2, tested against every divisor class.

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.structureToddOne_eq_toddOne {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 : Data P K) : IntersectionTheory.ChernCharacter.toddComponent T.structureData 1 = toddOne

The explicit class -K_X/2 is the degree-one representative reconstructed from the structure-sheaf twist polynomial. Thus the Todd family used by surface assembly is exactly the one used to extract reconstructed Chern characters, rather than an independently postulated comparison.

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.toddOne_eq_zero {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} (hK : K.canonicalClass = 1) : toddOne = 0

Trivial canonical class forces the geometric first Todd component to vanish.

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.degree_toddTwo_eq_two {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 : Data P K) (hchi : P.intersection.eulerPic 1 = 2) : P.ring.degree (toddTwo T) = 2

K3 top normalization: χ(O_X)=2 gives ∫td₂=2.

structure AlgebraicGeometry.RiemannRoch.Surface.ToddData.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} (T : Data PB KB) : Prop

A proposed Layer A numerical variety uses the geometrically constructed Todd components.

• ring_eq : V.ring = PB.ring
• toddComp_eq (i : ℕ) : V.toddComp i = toddComponent T i

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.NumericalVarietyComparison.toddComp_zero_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} {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} (T : Data PB KB) (Q : NumericalVarietyComparison V T) : V.toddComp 0 = 1

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.NumericalVarietyComparison.toddComp_one_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} {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} (T : Data PB KB) (Q : NumericalVarietyComparison V T) : V.toddComp 1 = toddOne

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.NumericalVarietyComparison.degree_toddComp_two_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} {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} (T : Data PB KB) (Q : NumericalVarietyComparison V T) : V.ring.degree (V.toddComp 2) = ↑(PB.intersection.eulerPic 1)

theorem AlgebraicGeometry.RiemannRoch.Surface.ToddData.NumericalVarietyComparison.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} {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} (T : Data PB KB) (Q : NumericalVarietyComparison V T) (hK : KB.canonicalClass = 1) (hchi : PB.intersection.eulerPic 1 = 2) : Numerical.K3.IsK3 V

The geometric Todd construction supplies the existing Layer A K3 hypotheses whenever the Layer A variety is explicitly compared with it.