Exceptional blocks and residual projection objects in the Enriques papers #
This file formalizes the common paper-content layer of arXiv:1912.04332v2, Setup 4.5 and Lemmas 4.7--4.8, and arXiv:2104.13610v2, Proposition 1.4, Setup 2.5, Lemma 2.4, and Theorem 2.7.
An PaperBlockData partitions the ten selected exceptional line bundles into
positive-length, mutually orthogonal exceptional blocks. Its residual is
identified with the already constructed neutral residual component. A
PaperResidualProjectionData then chooses the right adjoint to the residual
inclusion, and projectedObject is exactly the paper's
S_i := ζ_K^!(L_{i1}).
The spherical, pseudoprojective, orthogonality, and completeness statements remain supplied theorem data: their proofs use mutation triangles and Ext computations not yet constructed in the repository. The new classification constructors ensure, however, that these theorems concern the actual residual projections of the actual block objects, rather than arbitrary candidates.
The chains of (-2)-curves appearing in Paper II, Proposition 1.4 and the
mutation/Ext consequences they feed are recorded in the downstream
PaperExtension module.
structure
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData
{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 t)
[Fintype ι]
:
Type (max t (u + 1))
A block-shaped presentation of the ten selected exceptional line bundles.
bundleIndex and bundleIso say that the dependent family of block members
is precisely the original family of ten bundles, up to reindexing and
isomorphism. residual_eq records that taking the right orthogonal after
grouping into triangulated block spans gives the same neutral residual
property already constructed in Enriques.Residual.
- blocks : CategoryTheory.Triangulated.OrthogonalExceptionalBlocks k (DerivedCat Y) ι
The mutually orthogonal exceptional blocks.
The block positions enumerate exactly ten objects.
- bundleIso (x : (i : ι) × Fin (self.blocks.length i)) : (self.blocks.collection x.fst).obj x.snd ≅ (T.bundles (self.bundleIndex x)).boundedDerivedObject
Each block member is the corresponding selected line bundle.
Grouping the exceptional objects into blocks does not change their residual right orthogonal.
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.totalLength_eq_ten
{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 t}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
:
The block lengths sum to ten, derived from the supplied enumeration rather than stored as a second numerical field.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.decompositionType_sum_eq_ten
{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 t}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
:
The entries of the unordered block-decomposition type sum to ten.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.card_le_ten
{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 t}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
:
The number of blocks is at most ten.
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.firstBundleIndex
{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 t}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
(i : ι)
:
Fin 10
The original bundle index corresponding to the first member of block
i.
Equations
- B.firstBundleIndex i = B.bundleIndex ⟨i, B.blocks.firstIndex i⟩
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.firstObjectIso
{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 t}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
(i : ι)
:
The first object of a block is one of the original ten bounded derived line bundles.
Equations
- B.firstObjectIso i = B.bundleIso ⟨i, B.blocks.firstIndex i⟩
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.singleton_or_longer
{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 t}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
(i : ι)
:
Every block is either a singleton block or a longer block.
@[reducible, inline]
abbrev
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperResidualProjectionData
{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)
A chosen right-adjoint projection from the ambient derived category onto the already constructed residual category.
Equations
- T.PaperResidualProjectionData exceptional semiorthogonal = (T.residualComponent exceptional semiorthogonal).RightProjectionData
Instances For
@[reducible, inline]
noncomputable abbrev
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.projectedObject
{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 t}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
(Q : T.PaperResidualProjectionData exceptional semiorthogonal)
(i : ι)
:
T.ResidualCategory exceptional semiorthogonal
The paper's residual projection object
S_i := ζ_K^!(L_{i1}).
Equations
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.projectedObjectHomEquiv
{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 t}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
(Q : T.PaperResidualProjectionData exceptional semiorthogonal)
(R : T.ResidualCategory exceptional semiorthogonal)
(i : ι)
:
(R ⟶ B.projectedObject Q i) ≃ ((T.residualComponent exceptional semiorthogonal).ι.obj R ⟶ B.blocks.firstObject i)
Paper I, Remark 4.9(i), in its formal adjunction form: maps from a
residual object to S_i are ambient maps to the first object of block i.
Equations
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.projectedObjectHomEquiv_id
{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 t}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
(Q : T.PaperResidualProjectionData exceptional semiorthogonal)
(i : ι)
:
(B.projectedObjectHomEquiv Q (B.projectedObject Q i) i) (CategoryTheory.CategoryStruct.id (B.projectedObject Q i)) = CategoryTheory.ObjectProperty.RightProjectionData.counitApp Q (B.blocks.firstObject i)
The identity of S_i corresponds to its projection counit
S_i → L_{i1}.
structure
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionClassificationData
{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)
(B : T.PaperBlockData exceptional semiorthogonal (Fin 10))
(Q : T.PaperResidualProjectionData exceptional semiorthogonal)
:
Paper I's singleton-block projection statements and classification. This combines Lemma 4.8 and Proposition 4.10 while fixing the candidate family to the residual projections above.
Paper I has ten singleton blocks.
- spherical (i : Fin 10) : CategoryTheory.SerreFunctor.IsSphericalObject P.residualSerre.serre 3 (B.projectedObject Q i)
Each residual projection is
3-spherical. - pairwise_orthogonal {i j : Fin 10} : i ≠ j → CategoryTheory.SerreFunctor.IsGradedOrthogonal (B.projectedObject Q i) (B.projectedObject Q j)
Projections from distinct blocks are graded-orthogonal.
- complete (E : T.ResidualCategory exceptional semiorthogonal) : CategoryTheory.SerreFunctor.IsSphericalObject P.residualSerre.serre 3 E ↔ ∃ (i : Fin 10), CategoryTheory.SerreFunctor.IsShiftOf E (B.projectedObject Q i)
Every
3-spherical residual object is a shift of one projection.
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionClassificationData.toSphericalClassificationData
{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}
{B : T.PaperBlockData exceptional semiorthogonal (Fin 10)}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIProjectionClassificationData P B Q)
:
Forget the block/projection realization and recover the previously landed Paper I classification interface.
Equations
- A.toSphericalClassificationData = { candidate := B.projectedObject Q, candidate_spherical := ⋯, pairwise_orthogonal := ⋯, complete := ⋯ }
Instances For
@[simp]
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionClassificationData.toSphericalClassificationData_candidate
{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}
{B : T.PaperBlockData exceptional semiorthogonal (Fin 10)}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIProjectionClassificationData P B Q)
(i : Fin 10)
:
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionClassificationData.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}
{B : T.PaperBlockData exceptional semiorthogonal (Fin 10)}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIProjectionClassificationData P B Q)
(E : T.ResidualCategory exceptional semiorthogonal)
:
CategoryTheory.SerreFunctor.IsSphericalObject P.residualSerre.serre 3 E ↔ ∃ (i : Fin 10), CategoryTheory.SerreFunctor.IsShiftOf E (B.projectedObject Q i)
Exact Paper I classification for the actual residual projection objects.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionClassificationData.projectedObject_not_isZero
{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}
{B : T.PaperBlockData exceptional semiorthogonal (Fin 10)}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIProjectionClassificationData P B Q)
(i : Fin 10)
:
Every Paper I residual projection object is nonzero.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionClassificationData.projectedObject_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}
{B : T.PaperBlockData exceptional semiorthogonal (Fin 10)}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIProjectionClassificationData P B Q)
{i j : Fin 10}
(hij : i ≠ j)
:
¬CategoryTheory.SerreFunctor.IsShiftOf (B.projectedObject Q i) (B.projectedObject Q j)
Distinct Paper I projection objects are not isomorphic up to shift.
structure
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData
{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}
[Fintype ι]
(B : T.PaperBlockData exceptional semiorthogonal ι)
(Q : T.PaperResidualProjectionData exceptional semiorthogonal)
:
Paper II's block-sensitive projection statements and classification. The first three fields are Lemma 2.4; the final two are Theorem 2.7.
- spherical_of_singleton (i : ι) : B.blocks.length i = 1 → CategoryTheory.SerreFunctor.IsSphericalObject P.residualSerre.serre 3 (B.projectedObject Q i)
Singleton blocks produce
3-spherical residual projections. - pseudoprojective_of_longer (i : ι) : 2 ≤ B.blocks.length i → CategoryTheory.SerreFunctor.IsPseudoprojectiveObject P.residualSerre.serre 3 (B.projectedObject Q i)
Longer blocks produce
3-pseudoprojective residual projections. - pairwise_orthogonal {i j : ι} : i ≠ j → CategoryTheory.SerreFunctor.IsGradedOrthogonal (B.projectedObject Q i) (B.projectedObject Q j)
Projections from distinct blocks are graded-orthogonal.
- spherical_complete (E : T.ResidualCategory exceptional semiorthogonal) : CategoryTheory.SerreFunctor.IsSphericalObject P.residualSerre.serre 3 E ↔ ∃ (i : ι), B.blocks.length i = 1 ∧ CategoryTheory.SerreFunctor.IsShiftOf E (B.projectedObject Q i)
Classification of all
3-spherical residual objects. - pseudoprojective_complete (E : T.ResidualCategory exceptional semiorthogonal) : CategoryTheory.SerreFunctor.IsPseudoprojectiveObject P.residualSerre.serre 3 E ↔ ∃ (i : ι), 2 ≤ B.blocks.length i ∧ CategoryTheory.SerreFunctor.IsShiftOf E (B.projectedObject Q i)
Classification of all
3-pseudoprojective residual objects.
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.toMixedClassificationData
{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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
:
Forget the block/projection realization and recover the previously landed Paper II mixed classification interface.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.toMixedClassificationData_blockLength
{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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
(i : ι)
:
@[simp]
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.toMixedClassificationData_candidate
{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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
(i : ι)
:
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
(E : T.ResidualCategory exceptional semiorthogonal)
:
CategoryTheory.SerreFunctor.IsSphericalObject P.residualSerre.serre 3 E ↔ ∃ (i : ι), B.blocks.length i = 1 ∧ CategoryTheory.SerreFunctor.IsShiftOf E (B.projectedObject Q i)
Exact spherical half of Paper II's classification for the actual residual projection objects of singleton blocks.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
(E : T.ResidualCategory exceptional semiorthogonal)
:
CategoryTheory.SerreFunctor.IsPseudoprojectiveObject P.residualSerre.serre 3 E ↔ ∃ (i : ι), 2 ≤ B.blocks.length i ∧ CategoryTheory.SerreFunctor.IsShiftOf E (B.projectedObject Q i)
Exact pseudoprojective half of Paper II's classification for the actual residual projection objects of longer blocks.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.projectedObject_dichotomy
{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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
(i : ι)
:
Every Paper II projection object is either 3-spherical or
3-pseudoprojective.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.projectedObject_not_isZero
{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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
(i : ι)
:
Every Paper II residual projection object is nonzero.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.longer_projectedObject_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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
{i : ι}
(hi : 2 ≤ B.blocks.length i)
:
A longer-block residual projection cannot also be spherical.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.singleton_projectedObject_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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
{i j : ι}
(hi : B.blocks.length i = 1)
(hij : i ≠ j)
:
¬CategoryTheory.SerreFunctor.IsShiftOf (B.projectedObject Q i) (B.projectedObject Q j)
Distinct singleton-block projection objects are not isomorphic up to shift.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.longer_projectedObject_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}
[Fintype ι]
{B : T.PaperBlockData exceptional semiorthogonal ι}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionClassificationData P B Q)
{i j : ι}
(hi : 2 ≤ B.blocks.length i)
(hij : i ≠ j)
:
¬CategoryTheory.SerreFunctor.IsShiftOf (B.projectedObject Q i) (B.projectedObject Q j)
Distinct longer-block projection objects are not isomorphic up to shift.