The Enriques exceptional sequence and residual category #
The refined derived Torelli papers arXiv:1912.04332v2 and arXiv:2104.13610v2 study the right orthogonal to exceptional line-bundle collections on Enriques surfaces. This file builds the repository's formal counterpart from an isotropic 10-collection, its exceptionality data, and supplied pairwise semiorthogonality witnesses.
The output is deliberately neutral. residualComponent is the right
orthogonal to the union of the ten generated components, and
ResidualCategory is its full subcategory. No fullness, admissibility,
mutation, Torelli theorem, or equivalence with the papers' Kuznetsov
component is asserted.
The pairwise vanishing remains supplied geometric data: proving it from the intersection equations needs the effectiveness and line-bundle cohomology arguments that are not available at the current pin.
Main definitions #
IsotropicCollection.SemiorthogonalityData-- the pairwise shifted Hom vanishing in the classical exceptional-collection direction.IsotropicCollection.exceptionalCollection-- the ten line bundles as anExceptionalCollection.IsotropicCollection.collectionSequence-- the associated finite semiorthogonal sequence.IsotropicCollection.residualComponentandResidualCategory-- its right orthogonal and the corresponding full subcategory.
Main results #
bundle_mem_collectionSequence_component-- each bundle lies in its designated (order-reversed) component.residualComponent_isTriangulated-- the residual is triangulated.bundle_hom_residualCategory_eq_zero-- maps from any selected bundle to a residual object vanish.bundle_not_mem_residualComponent-- no selected exceptional bundle lies in the residual.
Pairwise shifted Hom-vanishing for the ten line bundles, in the classical exceptional-collection direction: maps from a later bundle to a shift of an earlier bundle vanish. This is the geometric input still missing from the intersection-theoretic collection API.
- hom_shift_eq_zero ⦃i j : Fin 10⦄ : i < j → ∀ (n : ℤ) (f : (T.bundles j).boundedDerivedObject ⟶ (CategoryTheory.shiftFunctor (DerivedCategory.SchemeBoundedCoherentDerivedCategory Y) n).obj (T.bundles i).boundedDerivedObject), f = 0
The pairwise vanishing witnesses for the selected line bundles.
Instances For
The ten selected line bundles as an exceptional collection. Individual
exceptionality is proved by ExceptionalityData.bundle_isExceptional; only
the pairwise geometric vanishing is read from SemiorthogonalityData.
Equations
- T.exceptionalCollection exceptional semiorthogonal = { obj := fun (i : Fin 10) => (T.bundles i).boundedDerivedObject, exceptional := ⋯, hom_shift_eq_zero := ⋯ }
Instances For
The finite semiorthogonal sequence generated by the ten selected bundles.
Its root convention is opposite to the classical collection convention, so
component i is generated by bundle i.rev.
Equations
- T.collectionSequence exceptional semiorthogonal = (T.exceptionalCollection exceptional semiorthogonal).toSemiorthogonalSequenceFin
Instances For
Bundle i lies in component i.rev of the root-oriented finite
semiorthogonal sequence.
The residual object property: the right orthogonal to the union of the ten generated components.
Equations
- T.residualComponent exceptional semiorthogonal = (T.collectionSequence exceptional semiorthogonal).residual
Instances For
The full subcategory on the residual object property. This name makes no admissibility or fullness claim.
Equations
- T.ResidualCategory exceptional semiorthogonal = (T.residualComponent exceptional semiorthogonal).FullSubcategory
Instances For
The residual object property is triangulated, because each generated component is triangulated and a right orthogonal to a shift-stable property is triangulated.
The underlying object of every object of ResidualCategory satisfies the
residual membership predicate.
Every map from a selected bundle to an object satisfying the residual predicate vanishes.
Full-subcategory consumer form of bundle_hom_residual_eq_zero.
No selected line bundle lies in the residual: its identity would vanish, contradicting exceptionality.