Enriques surfaces, numerically

The numerical signature of a classical Enriques surface is

• td₁(Y) = 0, because the canonical class is torsion and disappears in the numerical quotient;
• ∫_Y td₂(Y) = χ(O_Y) = 1.

IsEnriques records exactly this numerical shadow. It does not assert that a geometric Enriques scheme exists, nor does it recover the non-trivial 2-torsion canonical line bundle: numerical equivalence cannot see that data.

structure AlgebraicGeometry.Numerical.Enriques.IsEnriques {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) : Prop

The numerical signature of an Enriques surface: numerically trivial canonical class and χ(O_Y) = 1.

This is deliberately weaker than AlgebraicGeometry.SmoothProperVariety.IsEnriquesSurface: the latter is geometric and remembers non-trivial 2-torsion in Pic, while this predicate lives after passage to numerical data.

• toddComp_one : V.toddComp 1 = 0

  td₁(Y) = −K_Y/2 = 0 in the numerical quotient.

• degree_toddComp_two : V.ring.degree (V.toddComp 2) = 1

  ∫_Y td₂(Y) = χ(O_Y) = 1.

theorem AlgebraicGeometry.Numerical.Enriques.chi_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 2 A N) (hHRR : V.SatisfiesHRR) (hEnriques : IsEnriques V) (E : N) : ↑(V.chi E) = ↑(V.rank E) + V.ring.degree (V.chComp E 2)

Riemann--Roch on a numerical Enriques surface: χ(E) = rank(E) + ∫_Y ch₂(E).

The c₁ term vanishes numerically, while the rank term has coefficient one, in contrast with the K3 coefficient two.