Exceptional line bundles on an Enriques surface

Li--Nuer--Stellari--Zhao, arXiv:1912.04332v2, Proposition 3.5, use Extⁿ(L,L) ≅ Hⁿ(Y,O_Y) and the vanishing of H¹(Y,O_Y) and H²(Y,O_Y) to show that every line bundle on an Enriques surface is exceptional.

This file formalizes that reduction against the APIs available at the current pin. IsEnriquesSurface already contains the degree-one vanishing. The degree-two vanishing, the self-Ext/cohomology comparisons, the endomorphism comparison, and the out-of-range Ext vanishing are supplied as explicit Prop-valued data: Serre duality and the required derived Ext comparison are not theorems in the repository yet. From those inputs, exceptionality is proved rather than stored.

No Enriques surface, line bundle, comparison, or exceptional collection is constructed here.

Main definitions

• DerivedCat -- Dᵇ(Coh Y) in the Enriques namespace.
• ExtComparison -- the precise self-Ext comparison boundary for one line bundle.
• IsotropicCollection.ExceptionalityData -- the common degree-two vanishing and the ten comparison witnesses.

Main results

• isExceptional_of_extComparison -- the exceptionality reduction.
• IsotropicCollection.ExceptionalityData.bundle_isExceptional -- every member of a supplied isotropic collection is exceptional.

@[reducible, inline]

abbrev AlgebraicGeometry.EnriquesSurface.DerivedCat (Y : Scheme) [IsLocallyNoetherian Y] : Type (u + 1)

The bounded derived category of coherent sheaves on an Enriques surface. This is an abbreviation only; it introduces no new category.

Equations

• AlgebraicGeometry.EnriquesSurface.DerivedCat Y = AlgebraicGeometry.DerivedCategory.SchemeBoundedCoherentDerivedCategory Y

structure AlgebraicGeometry.EnriquesSurface.ExtComparison {k : Type u} [Field k] {Y : Scheme} [Y.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y] (L : Scheme.Modules.LineBundleData Y) : Prop

Supplied comparison data reducing exceptionality of a line bundle to coherent cohomology of the structure sheaf.

The first field is the degree-zero comparison together with H⁰(Y,O_Y) = k. The next two fields are the degree-one and degree-two self-Ext comparisons. The last field packages negative Ext vanishing and cohomological-dimension vanishing above degree two. These are fields because the requisite Ext/cohomology and cohomological-dimension theorems are not available at the current pin.

• endomorphisms : Function.Bijective ⇑(algebraMap k (CategoryTheory.End L.boundedDerivedObject))

  Scalar multiplication identifies k with the endomorphism ring of the bounded derived line bundle.

• ext_one : Nonempty ((L.boundedDerivedObject ⟶ (CategoryTheory.shiftFunctor (DerivedCategory.SchemeBoundedCoherentDerivedCategory Y) 1).obj L.boundedDerivedObject) ≃+ ↑((Cohomology.coherentH Y 1).obj Y.structureSheafCoh))

  The degree-one self-Ext group is the first coherent cohomology of the structure sheaf.

• ext_two : Nonempty ((L.boundedDerivedObject ⟶ (CategoryTheory.shiftFunctor (DerivedCategory.SchemeBoundedCoherentDerivedCategory Y) 2).obj L.boundedDerivedObject) ≃+ ↑((Cohomology.coherentH Y 2).obj Y.structureSheafCoh))

  The degree-two self-Ext group is the second coherent cohomology of the structure sheaf.

• outside_surface_range (n : ℤ) : n < 0 ∨ 2 < n → ∀ (f : L.boundedDerivedObject ⟶ (CategoryTheory.shiftFunctor (DerivedCategory.SchemeBoundedCoherentDerivedCategory Y) n).obj L.boundedDerivedObject), f = 0

  Self-Ext vanishes in negative degrees and above the surface range.

theorem AlgebraicGeometry.EnriquesSurface.isExceptional_of_extComparison {k : Type u} [Field k] {Y : Scheme} [Y.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y] {C : SmoothProperVariety.CanonicalSheafData k Y 2} [hY : SmoothProperVariety.IsEnriquesSurface k Y C] (L : Scheme.Modules.LineBundleData Y) (comparison : ExtComparison L) (hTwo : CategoryTheory.Limits.IsZero ((Cohomology.coherentH Y 2).obj Y.structureSheafCoh)) : CategoryTheory.Triangulated.IsExceptional k L.boundedDerivedObject

A line bundle on an Enriques surface is exceptional once the available H¹ vanishing, a supplied H² vanishing, and the explicit self-Ext comparison boundary are assembled.

structure AlgebraicGeometry.EnriquesSurface.IsotropicCollection.ExceptionalityData {k : Type u} [Field k] {Y : Scheme} [Y.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y] {C : SmoothProperVariety.CanonicalSheafData k Y 2} [hY : SmoothProperVariety.IsEnriquesSurface k Y C] {D : Cohomology.FiniteCohomology k Y} {S : D.LinearConnectingSystem} (T : IsotropicCollection D S) : Prop

The supplied cohomological input needed to prove exceptionality of all ten line bundles in an isotropic collection. The common H² vanishing is stored once; each bundle has its own self-Ext comparison.

• h_two_vanishing : CategoryTheory.Limits.IsZero ((Cohomology.coherentH Y 2).obj Y.structureSheafCoh)

  H²(Y,O_Y) = 0, pending the Serre-duality realization described in Enriques.Basic.

• comparison (i : Fin 10) : ExtComparison (T.bundles i)

  The self-Ext comparison for each selected line bundle.

theorem AlgebraicGeometry.EnriquesSurface.IsotropicCollection.ExceptionalityData.bundle_isExceptional {k : Type u} [Field k] {Y : Scheme} [Y.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y] {C : SmoothProperVariety.CanonicalSheafData k Y 2} [hY : SmoothProperVariety.IsEnriquesSurface k Y C] {D : Cohomology.FiniteCohomology k Y} {S : D.LinearConnectingSystem} (T : IsotropicCollection D S) (data : T.ExceptionalityData) (i : Fin 10) : CategoryTheory.Triangulated.IsExceptional k (T.bundles i).boundedDerivedObject

Every member of an isotropic collection is exceptional from the shared degree-two vanishing and its supplied self-Ext comparison.