Categorical assembly of the refined Enriques Torelli arguments

This file connects the paper-specific Enriques data to the three categorical lanes used in the closing arguments of arXiv:1912.04332v2, Theorem 5.1, and arXiv:2104.13610v2, Theorem 3.3.

1. Residual spherical/pseudoprojective classification determines a unique matching of exceptional blocks (PaperMatching.lean).
2. Extension in both directions proves equality of the matched block lengths, while the adjacent k ⊕ k[-1] Ext profile proves that every member of a block has one common shift.
3. Iterated one-object Fourier--Mukai extension, together with admissibility of the total exceptional parts, promotes the residual equivalence to an ambient kernel equivalence.

The functorial dg cone and its pointwise transform triangle now live below this paper layer. The remaining geometric seam in OneStepExtensionCriterion is to realize the paper's kernel category as an H⁰, lift its actual kernel morphism to that enhancement, and prove exactness of kernel evaluation. No ambient equivalence, length equality, or common-shift conclusion is accepted as an extra axiom here: each is derived from its corresponding categorical input.

@[reducible, inline]

abbrev AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperAdjacentExtData {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} {I : Type t} [Fintype I] (B : T.PaperBlockData exceptional semiorthogonal I) : Prop

The adjacent k ⊕ k[-1] Ext computations for the actual exceptional blocks of an Enriques paper decomposition.

Equations

• AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperAdjacentExtData B = B.blocks.AdjacentExtData

Exact length and common-shift conclusions

@[reducible, inline]

abbrev AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBidirectionalPrefixData {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} (e : I ≃ J) : Type (max t t')

Prefix-by-prefix extension in both directions for two paper block decompositions.

Equations

• AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBidirectionalPrefixData e = CategoryTheory.Triangulated.BidirectionalPrefixBlockEmbeddingData B₁.blocks B₂.blocks e

theorem AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBidirectionalPrefixData.length_eq {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {e : I ≃ J} (A : PaperBidirectionalPrefixData e) (i : I) : B₁.blocks.length i = B₂.blocks.length (e i)

Corresponding Enriques blocks have equal length, derived from the two prefix extensions.

@[reducible, inline]

abbrev AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.MatchingPrefixData {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁} {P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂} {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₂) : Type (max t t')

Bidirectional prefix extension indexed by the block matching forced by the residual spherical/pseudoprojective classification.

Equations

• A₁.MatchingPrefixData A₂ F = AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBidirectionalPrefixData (A₁.matchingEquiv A₂ F)

theorem AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.matchingEquiv_length_eq {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁} {P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂} {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₂) (L : A₁.MatchingPrefixData A₂ F) (i : I) : B₁.blocks.length i = B₂.blocks.length ((A₁.matchingEquiv A₂ F) i)

Matched Paper II blocks have exactly equal length. Classification determines the matching, and the two prefix extensions determine its exact lengths.

@[reducible, inline]

abbrev AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperMemberwiseBlockShiftData {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} (e : I ≃ J) (length_eq : ∀ (i : I), B₁.blocks.length i = B₂.blocks.length (e i)) (G : CategoryTheory.Functor (DerivedCat Y₁) (DerivedCat Y₂)) : Type (max t (u + 1))

Memberwise images of two Enriques block decompositions, before adjacent Ext rigidity identifies the shifts.

Equations

• AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperMemberwiseBlockShiftData e length_eq G = CategoryTheory.Triangulated.MemberwiseBlockShiftData B₁.blocks B₂.blocks e length_eq G

@[reducible, inline]

abbrev AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionClassificationData.MatchingMemberwiseShiftData {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {P₁ : T₁.PaperCategoryData exceptional₁ semiorthogonal₁} {P₂ : T₂.PaperCategoryData exceptional₂ semiorthogonal₂} {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₂) (L : A₁.MatchingPrefixData A₂ F) (G : CategoryTheory.Functor (DerivedCat Y₁) (DerivedCat Y₂)) : Type (max t (u + 1))

Memberwise image data indexed by the classification-derived block matching and its prefix-derived exact length equality.

Equations

• A₁.MatchingMemberwiseShiftData A₂ F L G = AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperMemberwiseBlockShiftData (A₁.matchingEquiv A₂ F) ⋯ G

noncomputable def AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperMemberwiseBlockShiftData.commonShift {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {e : I ≃ J} {length_eq : ∀ (i : I), B₁.blocks.length i = B₂.blocks.length (e i)} {G : CategoryTheory.Functor (DerivedCat Y₁) (DerivedCat Y₂)} (M : PaperMemberwiseBlockShiftData e length_eq G) (i : I) : ℤ

The common shift attached to a matched block.

Equations

• M.commonShift i = M.shift i (B₁.blocks.firstIndex i)

theorem AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperMemberwiseBlockShiftData.shift_eq_common {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {e : I ≃ J} {length_eq : ∀ (i : I), B₁.blocks.length i = B₂.blocks.length (e i)} {G : CategoryTheory.Functor (DerivedCat Y₁) (DerivedCat Y₂)} [G.Additive] [CategoryTheory.Functor.Linear k G] [G.CommShift ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor (DerivedCat Y₂) n)] (M : PaperMemberwiseBlockShiftData e length_eq G) (A₁ : PaperAdjacentExtData B₁) (A₂ : PaperAdjacentExtData B₂) (hG : G.FullyFaithful) (i : I) (j : Fin (B₁.blocks.length i)) : M.shift i j = M.commonShift i

Every member of a matched Enriques block carries its block's common shift.

noncomputable def AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperMemberwiseBlockShiftData.commonObjectIso {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {e : I ≃ J} {length_eq : ∀ (i : I), B₁.blocks.length i = B₂.blocks.length (e i)} {G : CategoryTheory.Functor (DerivedCat Y₁) (DerivedCat Y₂)} [G.Additive] [CategoryTheory.Functor.Linear k G] [G.CommShift ℤ] [∀ (n : ℤ), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor (DerivedCat Y₂) n)] (M : PaperMemberwiseBlockShiftData e length_eq G) (A₁ : PaperAdjacentExtData B₁) (A₂ : PaperAdjacentExtData B₂) (hG : G.FullyFaithful) (i : I) (j : Fin (B₁.blocks.length i)) : G.obj ((B₁.blocks.collection i).obj j) ≅ (CategoryTheory.shiftFunctor (DerivedCat Y₂) (M.commonShift i)).obj ((B₂.blocks.collection (e i)).obj (Fin.cast ⋯ j))

The memberwise image isomorphisms can therefore be expressed with one shift per block, as required in Paper II, Theorem 3.3.

Equations

• M.commonObjectIso A₁ A₂ hG i j = ⋯.mpr (M.objectIso i j)

Finite Fourier--Mukai extension and ambient generation

@[reducible, inline]

abbrev AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperGeneratedExtensionSequenceData {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {W : Type u} [CategoryTheory.Category.{u_1, u} W] {corr : CategoryTheory.Triangulated.FourierMukai.Correspondence (DerivedCat Y₁) (DerivedCat Y₂) W} (R : CategoryTheory.Triangulated.FourierMukai.ResidualKernelEquivalence B₁.blocks B₂.blocks corr) : Type (max (u + 1) u_1)

The finite extension sequence for the two actual Enriques exceptional parts, including the admissibility data which certifies ambient generation.

Equations

• AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperGeneratedExtensionSequenceData R = CategoryTheory.Triangulated.FourierMukai.GeneratedBlockExtensionSequenceData B₁.blocks B₂.blocks corr R

noncomputable def AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperGeneratedExtensionSequenceData.toKernelEquivalence {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {W : Type u} [CategoryTheory.Category.{u_1, u} W] {corr : CategoryTheory.Triangulated.FourierMukai.Correspondence (DerivedCat Y₁) (DerivedCat Y₂) W} (R : CategoryTheory.Triangulated.FourierMukai.ResidualKernelEquivalence B₁.blocks B₂.blocks corr) (A : PaperGeneratedExtensionSequenceData R) : CategoryTheory.Triangulated.FourierMukai.KernelEquivalence corr

Ambient extension conclusion of Paper I, Theorem 5.1, and Paper II, Theorem 3.3.

The final equivalence of the ambient derived categories is presented by the last Fourier--Mukai kernel in the extension sequence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperGeneratedExtensionSequenceData.ambientEquivalence {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {W : Type u} [CategoryTheory.Category.{u_1, u} W] {corr : CategoryTheory.Triangulated.FourierMukai.Correspondence (DerivedCat Y₁) (DerivedCat Y₂) W} (R : CategoryTheory.Triangulated.FourierMukai.ResidualKernelEquivalence B₁.blocks B₂.blocks corr) (A : PaperGeneratedExtensionSequenceData R) : DerivedCat Y₁ ≌ DerivedCat Y₂

The underlying promoted equivalence of ambient derived categories.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperGeneratedExtensionSequenceData.transform_isEquivalence {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} {I : Type t} {J : Type t'} [Fintype I] [Fintype J] {B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I} {B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J} {W : Type u} [CategoryTheory.Category.{u_1, u} W] {corr : CategoryTheory.Triangulated.FourierMukai.Correspondence (DerivedCat Y₁) (DerivedCat Y₂) W} (R : CategoryTheory.Triangulated.FourierMukai.ResidualKernelEquivalence B₁.blocks B₂.blocks corr) (A : PaperGeneratedExtensionSequenceData R) : (corr.transform A.sequence.finalKernel).IsEquivalence

The final Fourier--Mukai transform is an equivalence of the ambient derived categories.