Enriques surfaces

An Enriques surface is a smooth projective surface whose canonical class is 2-torsion but not trivial, with no first cohomology. This file says exactly that, against the objects this repository already has:

• the surface is X : Scheme with [IsSmoothProperVariety k X] carrying a CanonicalSheafData k X 2, exactly as for IsK3Surface — the dimension is the 2 in that package's SmoothOfRelativeDimension;
• "2-torsion canonical class" is the pair of group equations C.canonicalClass ^ 2 = 1 and C.canonicalClass ≠ 1 in Pic X, which need no torsion-Picard API: Pic is a group of units and the conditions are ordinary equations in it;
• "no first cohomology" is vanishing of H¹(X, O_X), using the constructed functor Cohomology.coherentH, verbatim the IsK3Surface clause.

The characteristic is not a field of the structure

Over a field of characteristic 2 the surfaces classically called Enriques split into classical, singular, and supersingular types, and for some of them ω_X is trivial, contradicting canonicalClass_ne_one. The definition here is the characteristic ≠ 2 one, but the exclusion is not recorded as a field: the source papers (Li--Nuer--Stellari--Zhao, arXiv:1912.04332, and Li--Stellari--Zhao, arXiv:2104.13610) assume an algebraically closed field of characteristic different from 2 theorem by theorem, and that is where the hypothesis belongs. A characteristic field here would make every downstream statement carry it even when unused.

What this file does not do

• It exhibits no Enriques surface. Nothing here constructs an X, a CanonicalSheafData k X 2, or an IsEnriquesSurface; every statement is conditional on data nobody has yet produced, exactly as for IsK3Surface.
• It states no geometric numerical consequence. Both H²(X, O_X) = 0 and χ(O_X) = 1 reduce to one missing input: Serre duality against the non-triviality of ω_X. It gives H²(X, O_X) ≅ H⁰(X, ω_X)^∨ = 0, because a non-trivial torsion line bundle has no sections, and then χ(O_X) = h⁰ - h¹ + h² = 1 needs nothing further. Duality/Serre/ carries that duality as DerivedStatement realization data rather than as a theorem, so neither geometric consequence is available at the pin. A separate numerical shadow now exists in Numerical/Models/Surface/Enriques.lean, including a degree-one witness of td₁ = 0 and ∫td₂ = 1; no bridge from that numerical model to a geometric Scheme or to IsEnriquesSurface is claimed.
• It does not construct the K3 double cover. The 2-torsion class classically determines an étale double cover with trivial canonical class; no covering machinery exists at the pin and none is stated.

Main definitions

• IsEnriquesSurface — the Prop-valued definition, over a supplied canonical-sheaf package.

Main results

• IsEnriquesSurface.canonicalSheaf_tensor_self_iso_unit — the sheaf-level trivialization ω_X ⊗ ω_X ≅ O_X extracted from the class equation.
• IsEnriquesSurface.canonicalSheaf_not_iso_unit — non-triviality at the sheaf level, through canonicalClass_eq_one_iff.
• IsEnriquesSurface.antiCanonicalClass_eq_canonicalClass — a 2-torsion class is its own inverse.
• IsEnriquesSurface.not_isK3Surface — the same canonical-sheaf package cannot witness both definitions.

References

• Li, Nuer, Stellari, Zhao, A refined Derived Torelli Theorem for Enriques surfaces, arXiv:1912.04332.
• Li, Stellari, Zhao, A refined Derived Torelli Theorem for Enriques surfaces, II: the non-generic case, arXiv:2104.13610.

Tags

Enriques surface, canonical class, torsion, Picard group

The definition

class AlgebraicGeometry.SmoothProperVariety.IsEnriquesSurface (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] (C : CanonicalSheafData k X 2) : Prop

An Enriques surface: a smooth projective surface whose canonical class is 2-torsion but not trivial, with vanishing first cohomology.

Prop-valued over a chosen CanonicalSheafData k X 2, for the same reason as IsK3Surface: the canonical-sheaf package is genuine data, so bundling it into the predicate would make "being an Enriques surface" depend on a choice. The torsion conditions are ordinary group equations in Pic X; no torsion-subgroup API is involved. The characteristic ≠ 2 hypothesis of the classical theory is deliberately absent — see the module docstring.

• projective : Variety.IsProjective k X

  The surface is projective. Stronger than the properness already carried by SmoothProperVariety, and the standard hypothesis of the source papers.

• canonicalClass_sq_eq_one : C.canonicalClass ^ 2 = 1

  ω_X is 2-torsion in Pic X. Equivalently, by canonicalSheaf_tensor_self_iso_unit, there is an isomorphism ω_X ⊗ ω_X ≅ O_X.

• canonicalClass_ne_one : C.canonicalClass ≠ 1

  ω_X is not trivial in Pic X. This is what separates an Enriques surface from a K3 surface; see not_isK3Surface.

• h1_vanishing : CategoryTheory.Limits.IsZero ((Cohomology.coherentH X 1).obj X.structureSheafCoh)

  H¹(X, O_X) = 0.

theorem AlgebraicGeometry.SmoothProperVariety.IsEnriquesSurface.canonicalSheaf_tensor_self_iso_unit {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {C : CanonicalSheafData k X 2} (h : IsEnriquesSurface k X C) : Nonempty (C.canonicalSheaf.tensorObj C.canonicalSheaf ≅ X.structureSheafCoh.obj)

The square of the canonical sheaf of an Enriques surface is trivial, at the sheaf level.

The class equation κ² = 1 is unpacked through Scheme.Modules.LineBundleData.toPic_tensor and Scheme.Modules.LineBundleData.toPic_eq_iff; the recorded tensor inverses play no part, which is why a bare Nonempty of isomorphisms comes out.

theorem AlgebraicGeometry.SmoothProperVariety.IsEnriquesSurface.canonicalSheaf_not_iso_unit {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {C : CanonicalSheafData k X 2} (h : IsEnriquesSurface k X C) : ¬Nonempty (C.canonicalSheaf ≅ X.structureSheafCoh.obj)

The canonical sheaf of an Enriques surface is not trivial, at the sheaf level. The contrapositive of canonicalClass_eq_one_iff applied to canonicalClass_ne_one.

theorem AlgebraicGeometry.SmoothProperVariety.IsEnriquesSurface.antiCanonicalClass_eq_canonicalClass {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {C : CanonicalSheafData k X 2} (h : IsEnriquesSurface k X C) : C.antiCanonicalLineBundle.toPic = C.canonicalClass

A 2-torsion canonical class is its own inverse: κ⁻¹ = κ, since κ * κ = 1.

Stated for Serre duality, whose surface-level statements twist by κ * L⁻¹ (Duality.Serre.SurfacePicardSymmetry): on an Enriques surface the ω_X and ω_X⁻¹ twists coincide, so the two directions of the duality agree without a case split. Nothing consumes it yet — those statements take the canonical class as a bare Pic parameter and never see a CanonicalSheafData.

theorem AlgebraicGeometry.SmoothProperVariety.IsEnriquesSurface.not_isK3Surface {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {C : CanonicalSheafData k X 2} (h : IsEnriquesSurface k X C) : ¬IsK3Surface k X C

No canonical-sheaf package witnesses both definitions: an Enriques surface is not a K3 surface. The two definitions disagree exactly at triviality of the canonical class, and this pins them against each other on the shared carrier.

Scheme-facing convenience namespace

As for K3 surfaces, "let Y be an Enriques surface" means (Y : Scheme) [Y.Over (Spec k)] [IsSmoothProperVariety k Y] (C : CanonicalSheafData k Y 2) [IsEnriquesSurface k Y C]. There is no bundled surface carrier. The namespace below only gives Scheme-facing convenience theorems.

theorem AlgebraicGeometry.EnriquesSurface.isProjective {k : Type u} [Field k] {Y : Scheme} [Y.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y] {C : SmoothProperVariety.CanonicalSheafData k Y 2} [h : SmoothProperVariety.IsEnriquesSurface k Y C] : Variety.IsProjective k Y

An Enriques surface is projective. Not an instance, for the reason given at K3Surface.isProjective.