Serre and object-classification data for the Enriques papers #
This file connects the abstract Serre, spherical, and pseudoprojective APIs to the Enriques residual category constructed from an isotropic 10-collection. It records exactly the categorical conclusions used in arXiv:1912.04332v2 and arXiv:2104.13610v2:
- the ambient derived category is
2-Enriques, so its Serre functor squares to shift by four; - the residual category has a chosen Serre autoequivalence;
- Paper I's ten
3-spherical candidates are classified up to shift; and - Paper II's length-one and longer-block candidates classify respectively the
3-spherical and3-pseudoprojective objects.
The geometry proving these statements is deliberately exposed as supplied data. The current repository constructs the residual full subcategory but does not yet construct its admissible projection or mutation functors, nor the Ext computations for the projected candidates. Consequently this file does not manufacture those deep theorems from weaker hypotheses. Its purpose is to give them a precise, reusable Lean interface and to prove their formal consumer consequences.
structure
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCategoryData
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
(T : IsotropicCollection D S)
(exceptional : T.ExceptionalityData)
(semiorthogonal : T.SemiorthogonalityData)
:
Type (u + 1)
The Serre-theoretic categorical input for the two Enriques papers.
The ambient field is the formal content of the statement that D^b(Y) is a
2-Enriques category. The residual field is kept separate: the papers give
the right orthogonal its own Serre autoequivalence, but do not assert that the
residual category is itself 2-Enriques.
- ambientEnriques : CategoryTheory.SerreFunctor.TwoEnriquesCategoryData k (DerivedCat Y)
The ambient derived category is
2-Enriques. - residualSerre : CategoryTheory.SerreFunctor.SerreCategoryData k (T.ResidualCategory exceptional semiorthogonal)
The chosen Serre autoequivalence of the residual category.
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCategoryData.ambientSerreSquareObjIso
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
{T : IsotropicCollection D S}
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
(P : T.PaperCategoryData exceptional semiorthogonal)
(E : DerivedCat Y)
:
P.ambientEnriques.serre.S.obj (P.ambientEnriques.serre.S.obj E) ≅ (CategoryTheory.shiftFunctor (DerivedCat Y) 4).obj E
Objectwise ambient relation S_Y²(E) ≅ E[4].
Equations
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCategoryData.residualSerreIsEquivalence
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
{T : IsotropicCollection D S}
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
(P : T.PaperCategoryData exceptional semiorthogonal)
:
The selected residual Serre functor is an autoequivalence.
@[reducible, inline]
abbrev
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperISphericalClassificationData
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
(T : IsotropicCollection D S)
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
(P : T.PaperCategoryData exceptional semiorthogonal)
:
Type (u + 1)
Paper I, Proposition 4.10, specialized to the residual category of the
isotropic 10-collection: ten 3-spherical candidates, pairwise distinct up to
shift, classify all 3-spherical objects.
Equations
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperISphericalClassificationData.spherical_iff
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
{T : IsotropicCollection D S}
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
{P : T.PaperCategoryData exceptional semiorthogonal}
(A : T.PaperISphericalClassificationData P)
(E : T.ResidualCategory exceptional semiorthogonal)
:
CategoryTheory.SerreFunctor.IsSphericalObject P.residualSerre.serre 3 E ↔ ∃ (i : Fin 10), CategoryTheory.SerreFunctor.IsShiftOf E (A.candidate i)
Exact Paper I classification: a residual object is 3-spherical exactly
when it is a shift of one of the ten candidates.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperISphericalClassificationData.candidate_not_shift
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
{T : IsotropicCollection D S}
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
{P : T.PaperCategoryData exceptional semiorthogonal}
(A : T.PaperISphericalClassificationData P)
{i j : Fin 10}
(hij : i ≠ j)
:
¬CategoryTheory.SerreFunctor.IsShiftOf (A.candidate i) (A.candidate j)
Distinct Paper I candidates are not isomorphic after any shift.
@[reducible, inline]
abbrev
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIObjectClassificationData
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
(T : IsotropicCollection D S)
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
(P : T.PaperCategoryData exceptional semiorthogonal)
(ι : Type t)
:
Type (max t (u + 1))
Paper II, Theorem 2.7, specialized to degree three. The index type keeps
track of the exceptional blocks and blockLength separates length-one
spherical candidates from longer pseudoprojective candidates.
Equations
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIObjectClassificationData.spherical_iff
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
{T : IsotropicCollection D S}
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
{P : T.PaperCategoryData exceptional semiorthogonal}
{ι : Type t}
(A : T.PaperIIObjectClassificationData P ι)
(E : T.ResidualCategory exceptional semiorthogonal)
:
CategoryTheory.SerreFunctor.IsSphericalObject P.residualSerre.serre 3 E ↔ ∃ (i : ι), A.blockLength i = 1 ∧ CategoryTheory.SerreFunctor.IsShiftOf E (A.candidate i)
Exact spherical half of Paper II's classification theorem.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIObjectClassificationData.pseudoprojective_iff
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
{T : IsotropicCollection D S}
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
{P : T.PaperCategoryData exceptional semiorthogonal}
{ι : Type t}
(A : T.PaperIIObjectClassificationData P ι)
(E : T.ResidualCategory exceptional semiorthogonal)
:
CategoryTheory.SerreFunctor.IsPseudoprojectiveObject P.residualSerre.serre 3 E ↔ ∃ (i : ι), 2 ≤ A.blockLength i ∧ CategoryTheory.SerreFunctor.IsShiftOf E (A.candidate i)
Exact pseudoprojective half of Paper II's classification theorem.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIObjectClassificationData.longer_candidate_not_spherical
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
{T : IsotropicCollection D S}
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
{P : T.PaperCategoryData exceptional semiorthogonal}
{ι : Type t}
(A : T.PaperIIObjectClassificationData P ι)
{i : ι}
(hi : 2 ≤ A.blockLength i)
:
A longer-block candidate cannot also be spherical.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIObjectClassificationData.spherical_candidate_not_shift
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
{T : IsotropicCollection D S}
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
{P : T.PaperCategoryData exceptional semiorthogonal}
{ι : Type t}
(A : T.PaperIIObjectClassificationData P ι)
{i j : ι}
(hi : A.blockLength i = 1)
(hij : i ≠ j)
:
¬CategoryTheory.SerreFunctor.IsShiftOf (A.candidate i) (A.candidate j)
Distinct spherical Paper II candidates are not isomorphic up to shift.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIObjectClassificationData.pseudoprojective_candidate_not_shift
{k : Type u}
[Field k]
{Y : Scheme}
[Y.Over (Spec (CommRingCat.of k))]
[IsSmoothProperVariety k Y]
{C : SmoothProperVariety.CanonicalSheafData k Y 2}
[SmoothProperVariety.IsEnriquesSurface k Y C]
{D : Cohomology.FiniteCohomology k Y}
{S : D.LinearConnectingSystem}
{T : IsotropicCollection D S}
{exceptional : T.ExceptionalityData}
{semiorthogonal : T.SemiorthogonalityData}
{P : T.PaperCategoryData exceptional semiorthogonal}
{ι : Type t}
(A : T.PaperIIObjectClassificationData P ι)
{i j : ι}
(hi : 2 ≤ A.blockLength i)
(hij : i ≠ j)
:
¬CategoryTheory.SerreFunctor.IsShiftOf (A.candidate i) (A.candidate j)
Distinct pseudoprojective Paper II candidates are not isomorphic up to shift.