The square-root Todd class on a K3 surface

This downstream specialization combines the generic square-root construction with the numerical K3 axioms. The generic construction therefore remains importable without K3 Riemann--Roch.

theorem AlgebraicGeometry.Numerical.K3.sqrtToddComp_one {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} (hK3 : IsK3 V) : V.sqrtToddComp 1 = 0

On a K3 the linear term of √td vanishes, because td₁ = 0.

theorem AlgebraicGeometry.Numerical.K3.degree_sqrtToddComp_two {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} (hK3 : IsK3 V) : V.ring.degree (V.sqrtToddComp 2) = 1

∫_X √td₂ = 1: with td₁ = 0 the quadratic term is td₂/2, and ∫td₂ = χ(O_X) = 2.