Matching Enriques exceptional blocks from their residual projections

This file specializes classification matching to the residual categories and projection objects of the two refined Torelli papers. A Serre-compatible equivalence determines the reindexing: completeness supplies a target projection up to shift, and graded orthogonality proves uniqueness.

For the singleton-block setting of Paper I this is the equality-of-count and reordering step in Theorem 5.1. For the block-shaped setting of Paper II it is the first part of Theorem 3.3: blocks are matched up to reordering, and the matching preserves the dichotomy between singleton and longer blocks. Exact equality of two longer block lengths is a consequence of the later extension induction, not of the object classification alone.

@[reducible, inline]

abbrev AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperResidualSerreEquivalence {k : Type u} [Field k] {Y₁ Y₂ : Scheme} [Y₁.Over (Spec (CommRingCat.of k))] [Y₂.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y₁] [IsSmoothProperVariety k Y₂] {C₁ : SmoothProperVariety.CanonicalSheafData k Y₁ 2} {C₂ : SmoothProperVariety.CanonicalSheafData k Y₂ 2} [SmoothProperVariety.IsEnriquesSurface k Y₁ C₁] [SmoothProperVariety.IsEnriquesSurface k Y₂ C₂] {D₁ : Cohomology.FiniteCohomology k Y₁} {D₂ : Cohomology.FiniteCohomology k Y₂} {S₁ : D₁.LinearConnectingSystem} {S₂ : D₂.LinearConnectingSystem} {T₁ : IsotropicCollection D₁ S₁} {T₂ : IsotropicCollection D₂ S₂} {exceptional₁ : T₁.ExceptionalityData} {exceptional₂ : T₂.ExceptionalityData} {semiorthogonal₁ : T₁.SemiorthogonalityData} {semiorthogonal₂ : T₂.SemiorthogonalityData} (P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁) (P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂) : Type (u + 1)

A Serre-compatible equivalence between the two residual categories. The compatibility remains explicit until #896--#898 derive it from an exact linear equivalence.

Equations

• AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperResidualSerreEquivalence P₁ P₂ = CategoryTheory.SerreFunctor.SerreCompatibleEquivalence P₁.residualSerre.serre P₂.residualSerre.serre

noncomputable def AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionClassificationData.matchingEquiv {k : Type u} [Field k] {Y₁ Y₂ : Scheme} [Y₁.Over (Spec (CommRingCat.of k))] [Y₂.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y₁] [IsSmoothProperVariety k Y₂] {C₁ : SmoothProperVariety.CanonicalSheafData k Y₁ 2} {C₂ : SmoothProperVariety.CanonicalSheafData k Y₂ 2} [SmoothProperVariety.IsEnriquesSurface k Y₁ C₁] [SmoothProperVariety.IsEnriquesSurface k Y₂ C₂] {D₁ : Cohomology.FiniteCohomology k Y₁} {D₂ : Cohomology.FiniteCohomology k Y₂} {S₁ : D₁.LinearConnectingSystem} {S₂ : D₂.LinearConnectingSystem} {T₁ : IsotropicCollection D₁ S₁} {T₂ : IsotropicCollection D₂ S₂} {exceptional₁ : T₁.ExceptionalityData} {exceptional₂ : T₂.ExceptionalityData} {semiorthogonal₁ : T₁.SemiorthogonalityData} {semiorthogonal₂ : T₂.SemiorthogonalityData} {P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁} {P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂} {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ (Fin 10)} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ (Fin 10)} {Q₁ : T₁.PaperResidualProjectionData exceptional₁ semiorthogonal₁} {Q₂ : T₂.PaperResidualProjectionData exceptional₂ semiorthogonal₂} (A₁ : T₁.PaperIProjectionClassificationData P₁ B₁ Q₁) (A₂ : T₂.PaperIProjectionClassificationData P₂ B₂ Q₂) (F : PaperResidualSerreEquivalence P₁ P₂) : Fin 10 ≃ Fin 10

The reordering of Paper I's ten singleton blocks forced by the residual equivalence.

Equations

• A₁.matchingEquiv A₂ F = CategoryTheory.SerreFunctor.SphericalClassificationData.matchingEquiv A₁.toSphericalClassificationData A₂.toSphericalClassificationData F

theorem AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionClassificationData.matchingEquiv_spec {k : Type u} [Field k] {Y₁ Y₂ : Scheme} [Y₁.Over (Spec (CommRingCat.of k))] [Y₂.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y₁] [IsSmoothProperVariety k Y₂] {C₁ : SmoothProperVariety.CanonicalSheafData k Y₁ 2} {C₂ : SmoothProperVariety.CanonicalSheafData k Y₂ 2} [SmoothProperVariety.IsEnriquesSurface k Y₁ C₁] [SmoothProperVariety.IsEnriquesSurface k Y₂ C₂] {D₁ : Cohomology.FiniteCohomology k Y₁} {D₂ : Cohomology.FiniteCohomology k Y₂} {S₁ : D₁.LinearConnectingSystem} {S₂ : D₂.LinearConnectingSystem} {T₁ : IsotropicCollection D₁ S₁} {T₂ : IsotropicCollection D₂ S₂} {exceptional₁ : T₁.ExceptionalityData} {exceptional₂ : T₂.ExceptionalityData} {semiorthogonal₁ : T₁.SemiorthogonalityData} {semiorthogonal₂ : T₂.SemiorthogonalityData} {P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁} {P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂} {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ (Fin 10)} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ (Fin 10)} {Q₁ : T₁.PaperResidualProjectionData exceptional₁ semiorthogonal₁} {Q₂ : T₂.PaperResidualProjectionData exceptional₂ semiorthogonal₂} (A₁ : T₁.PaperIProjectionClassificationData P₁ B₁ Q₁) (A₂ : T₂.PaperIProjectionClassificationData P₂ B₂ Q₂) (F : PaperResidualSerreEquivalence P₁ P₂) (i : Fin 10) : CategoryTheory.SerreFunctor.IsShiftOf (F.equiv.functor.obj (B₁.projectedObject Q₁ i)) (B₂.projectedObject Q₂ ((A₁.matchingEquiv A₂ F) i))

Each Paper I projection maps to a shift of the uniquely matched target projection.

noncomputable def AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.matchingEquiv {k : Type u} [Field k] {Y₁ Y₂ : Scheme} [Y₁.Over (Spec (CommRingCat.of k))] [Y₂.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y₁] [IsSmoothProperVariety k Y₂] {C₁ : SmoothProperVariety.CanonicalSheafData k Y₁ 2} {C₂ : SmoothProperVariety.CanonicalSheafData k Y₂ 2} [SmoothProperVariety.IsEnriquesSurface k Y₁ C₁] [SmoothProperVariety.IsEnriquesSurface k Y₂ C₂] {D₁ : Cohomology.FiniteCohomology k Y₁} {D₂ : Cohomology.FiniteCohomology k Y₂} {S₁ : D₁.LinearConnectingSystem} {S₂ : D₂.LinearConnectingSystem} {T₁ : IsotropicCollection D₁ S₁} {T₂ : IsotropicCollection D₂ S₂} {exceptional₁ : T₁.ExceptionalityData} {exceptional₂ : T₂.ExceptionalityData} {semiorthogonal₁ : T₁.SemiorthogonalityData} {semiorthogonal₂ : T₂.SemiorthogonalityData} {P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁} {P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {Q₁ : T₁.PaperResidualProjectionData exceptional₁ semiorthogonal₁} {Q₂ : T₂.PaperResidualProjectionData exceptional₂ semiorthogonal₂} (A₁ : T₁.PaperIIProjectionClassificationData P₁ B₁ Q₁) (A₂ : T₂.PaperIIProjectionClassificationData P₂ B₂ Q₂) (F : PaperResidualSerreEquivalence P₁ P₂) : I ≃ J

The reordering of Paper II's exceptional blocks forced by the spherical and pseudoprojective classifications.

Equations

• A₁.matchingEquiv A₂ F = CategoryTheory.SerreFunctor.MixedClassificationData.matchingEquiv A₁.toMixedClassificationData A₂.toMixedClassificationData F ⋯ ⋯

theorem AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.matchingEquiv_length_eq_one_iff {k : Type u} [Field k] {Y₁ Y₂ : Scheme} [Y₁.Over (Spec (CommRingCat.of k))] [Y₂.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y₁] [IsSmoothProperVariety k Y₂] {C₁ : SmoothProperVariety.CanonicalSheafData k Y₁ 2} {C₂ : SmoothProperVariety.CanonicalSheafData k Y₂ 2} [SmoothProperVariety.IsEnriquesSurface k Y₁ C₁] [SmoothProperVariety.IsEnriquesSurface k Y₂ C₂] {D₁ : Cohomology.FiniteCohomology k Y₁} {D₂ : Cohomology.FiniteCohomology k Y₂} {S₁ : D₁.LinearConnectingSystem} {S₂ : D₂.LinearConnectingSystem} {T₁ : IsotropicCollection D₁ S₁} {T₂ : IsotropicCollection D₂ S₂} {exceptional₁ : T₁.ExceptionalityData} {exceptional₂ : T₂.ExceptionalityData} {semiorthogonal₁ : T₁.SemiorthogonalityData} {semiorthogonal₂ : T₂.SemiorthogonalityData} {P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁} {P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {Q₁ : T₁.PaperResidualProjectionData exceptional₁ semiorthogonal₁} {Q₂ : T₂.PaperResidualProjectionData exceptional₂ semiorthogonal₂} (A₁ : T₁.PaperIIProjectionClassificationData P₁ B₁ Q₁) (A₂ : T₂.PaperIIProjectionClassificationData P₂ B₂ Q₂) (F : PaperResidualSerreEquivalence P₁ P₂) (i : I) : B₂.blocks.length ((A₁.matchingEquiv A₂ F) i) = 1 ↔ B₁.blocks.length i = 1

The matching preserves and reflects singleton blocks.

theorem AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.matchingEquiv_length_two_le_iff {k : Type u} [Field k] {Y₁ Y₂ : Scheme} [Y₁.Over (Spec (CommRingCat.of k))] [Y₂.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y₁] [IsSmoothProperVariety k Y₂] {C₁ : SmoothProperVariety.CanonicalSheafData k Y₁ 2} {C₂ : SmoothProperVariety.CanonicalSheafData k Y₂ 2} [SmoothProperVariety.IsEnriquesSurface k Y₁ C₁] [SmoothProperVariety.IsEnriquesSurface k Y₂ C₂] {D₁ : Cohomology.FiniteCohomology k Y₁} {D₂ : Cohomology.FiniteCohomology k Y₂} {S₁ : D₁.LinearConnectingSystem} {S₂ : D₂.LinearConnectingSystem} {T₁ : IsotropicCollection D₁ S₁} {T₂ : IsotropicCollection D₂ S₂} {exceptional₁ : T₁.ExceptionalityData} {exceptional₂ : T₂.ExceptionalityData} {semiorthogonal₁ : T₁.SemiorthogonalityData} {semiorthogonal₂ : T₂.SemiorthogonalityData} {P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁} {P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {Q₁ : T₁.PaperResidualProjectionData exceptional₁ semiorthogonal₁} {Q₂ : T₂.PaperResidualProjectionData exceptional₂ semiorthogonal₂} (A₁ : T₁.PaperIIProjectionClassificationData P₁ B₁ Q₁) (A₂ : T₂.PaperIIProjectionClassificationData P₂ B₂ Q₂) (F : PaperResidualSerreEquivalence P₁ P₂) (i : I) : 2 ≤ B₂.blocks.length ((A₁.matchingEquiv A₂ F) i) ↔ 2 ≤ B₁.blocks.length i

The matching preserves and reflects longer blocks.

theorem AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.matchingEquiv_spec {k : Type u} [Field k] {Y₁ Y₂ : Scheme} [Y₁.Over (Spec (CommRingCat.of k))] [Y₂.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y₁] [IsSmoothProperVariety k Y₂] {C₁ : SmoothProperVariety.CanonicalSheafData k Y₁ 2} {C₂ : SmoothProperVariety.CanonicalSheafData k Y₂ 2} [SmoothProperVariety.IsEnriquesSurface k Y₁ C₁] [SmoothProperVariety.IsEnriquesSurface k Y₂ C₂] {D₁ : Cohomology.FiniteCohomology k Y₁} {D₂ : Cohomology.FiniteCohomology k Y₂} {S₁ : D₁.LinearConnectingSystem} {S₂ : D₂.LinearConnectingSystem} {T₁ : IsotropicCollection D₁ S₁} {T₂ : IsotropicCollection D₂ S₂} {exceptional₁ : T₁.ExceptionalityData} {exceptional₂ : T₂.ExceptionalityData} {semiorthogonal₁ : T₁.SemiorthogonalityData} {semiorthogonal₂ : T₂.SemiorthogonalityData} {P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁} {P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {Q₁ : T₁.PaperResidualProjectionData exceptional₁ semiorthogonal₁} {Q₂ : T₂.PaperResidualProjectionData exceptional₂ semiorthogonal₂} (A₁ : T₁.PaperIIProjectionClassificationData P₁ B₁ Q₁) (A₂ : T₂.PaperIIProjectionClassificationData P₂ B₂ Q₂) (F : PaperResidualSerreEquivalence P₁ P₂) (i : I) : CategoryTheory.SerreFunctor.IsShiftOf (F.equiv.functor.obj (B₁.projectedObject Q₁ i)) (B₂.projectedObject Q₂ ((A₁.matchingEquiv A₂ F) i))

Each Paper II projection maps to a shift of the uniquely matched target projection.