Mutation, curve chains, Ext computations, and extension for the Enriques papers #
This is the geometric adapter for the next layer of arXiv:1912.04332v2 and arXiv:2104.13610v2.
- proposition-valued admissibility now produces an actual residual projection;
- the projection counit gives the paper's mutation triangle;
- an
A_nchain of effective Cartier divisors records the(-2)-curve geometry of Paper II, Proposition 1.4; - the line-bundle class formula supplies isomorphisms from the selected representatives to Cartier-prefix twists, whose exact sequences construct the successive distinguished triangles and block maps;
- self-Ext computations are separated from the Serre-shift and classification arguments, with constructors rebuilding the Paper I and Paper II theorem packages; and
- the closing aliases specialize the generic Fourier--Mukai extension result to the actual residual and ambient categories used here.
The remaining geometric gaps stay visible. The current Cartier-divisor API
has no predicate saying that an effective divisor is an irreducible curve,
and PaperCurveChainData still supplies residual orthogonality of each curve
quotient. It no longer supplies the triangles themselves. Likewise,
the abstract dg cone and its pointwise transform triangle are now functorial,
with DGFunctor.HomogeneousNatTrans.ConeData as the construction root and
FourierMukai.CounitKernelConeData as the adjunction-counit specialization.
Constructing the paper's extended Fourier--Mukai kernel still waits on the
geometric H⁰ model, the paper's ordinary kernel morphism with its exact
counit-transform equation, an enhancement, and exactness of kernel evaluation
(#853--#855); it is not silently identified with the counit specialization.
Its categorical consequences continue to use the existing kernel/adjunction
roots immediately.
Projection existence and mutation triangles #
structure
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperResidualAdmissibilityData
{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)
:
The geometric admissibility input for the residual component.
The papers obtain this from an admissible semiorthogonal decomposition. It is kept supplied here because the current Enriques construction proves only that the residual right orthogonal is triangulated.
- rightAdmissible : (T.residualComponent exceptional semiorthogonal).IsRightAdmissible
The residual inclusion has a right adjoint.
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperResidualAdmissibilityData.projectionData
{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}
(A : T.PaperResidualAdmissibilityData exceptional semiorthogonal)
:
T.PaperResidualProjectionData exceptional semiorthogonal
Choose the geometric residual projection from admissibility.
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperBlockData.mutationTriangle
{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)
(Q : T.PaperResidualProjectionData exceptional semiorthogonal)
(i : I)
:
The paper's objectwise mutation triangle
S_i ⟶ L_{i1} ⟶ L_{\mathcal K}(L_{i1}).
The first term is definitionally the residual projection object and the first map is its adjunction counit.
Equations
Instances For
(-2)-curve chains #
structure
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.MinusTwoCurveChain
{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)
(n : ℕ)
:
Type u
A supplied A_n chain of effective Cartier divisors with the numerical
intersection matrix of (-2)-curves.
Effectivity and the intersection matrix are genuine repository notions. Irreducibility/reducedness are not yet expressible, so the word "curve" in the declaration name records the intended geometric realization rather than an unavailable extra predicate.
- curve : Fin n → Scheme.EffectiveCartierDivisor
The effective Cartier divisors in the chain.
- selfIntersection (i : Fin n) : T.intersection.picardIntersectionNumber ![Scheme.CartierDivisor.toPic (self.curve i).divisor, Scheme.CartierDivisor.toPic (self.curve i).divisor] = -2
Every member has self-intersection
-2. - adjacentIntersection (i : ℕ) (hi : i + 1 < n) : T.intersection.picardIntersectionNumber ![Scheme.CartierDivisor.toPic (self.curve ⟨i, ⋯⟩).divisor, Scheme.CartierDivisor.toPic (self.curve ⟨i + 1, hi⟩).divisor] = 1
Consecutive members intersect once.
- nonAdjacentIntersection (i j : Fin n) : ↑i + 1 < ↑j ∨ ↑j + 1 < ↑i → T.intersection.picardIntersectionNumber ![Scheme.CartierDivisor.toPic (self.curve i).divisor, Scheme.CartierDivisor.toPic (self.curve j).divisor] = 0
Non-consecutive members are disjoint numerically.
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.MinusTwoCurveChain.prefixDivisor
{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}
{n : ℕ}
(A : T.MinusTwoCurveChain n)
(j : ℕ)
(hj : j ≤ n)
:
The sum of the first j divisors in the chain.
Instances For
@[simp]
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.MinusTwoCurveChain.prefixDivisor_zero
{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}
{n : ℕ}
(A : T.MinusTwoCurveChain n)
:
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.MinusTwoCurveChain.prefixDivisor_succ
{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}
{n : ℕ}
(A : T.MinusTwoCurveChain n)
(j : ℕ)
(hj : j < n)
:
Adding the next curve extends the prefix divisor by that curve.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.MinusTwoCurveChain.prefixDivisor_succ_sub
{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}
{n : ℕ}
(A : T.MinusTwoCurveChain n)
(j : ℕ)
(hj : j < n)
:
The source divisor in the normalized sequence for the next curve is the preceding prefix.
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.MinusTwoCurveChain.lineBundleStepTriangle
{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}
{n : ℕ}
(A : T.MinusTwoCurveChain n)
(L : Scheme.Modules.LineBundleData Y)
(j : ℕ)
(hj : j < n)
:
The canonical bounded-derived triangle for one step of the divisor
chain, after tensoring by an arbitrary base line bundle. Its first two
vertices are L ⊗ O(prefix j) and L ⊗ O(prefix (j+1)).
Equations
- A.lineBundleStepTriangle L j hj = (A.curve ⟨j, hj⟩).cohLineBundleTwistBoundedTriangle L (A.prefixDivisor (j + 1) ⋯)
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.MinusTwoCurveChain.lineBundleStepTriangle_distinguished
{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}
{n : ℕ}
(A : T.MinusTwoCurveChain n)
(L : Scheme.Modules.LineBundleData Y)
(j : ℕ)
(hj : j < n)
:
A divisor-chain step triangle is distinguished.
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.MinusTwoCurveChain.lineBundleStepTriangleObj₁Iso
{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}
{n : ℕ}
(A : T.MinusTwoCurveChain n)
(L : Scheme.Modules.LineBundleData Y)
(j : ℕ)
(hj : j < n)
:
(A.lineBundleStepTriangle L j hj).obj₁ ≅ (L.tensor (Scheme.CartierDivisor.lineBundleData (A.prefixDivisor j ⋯))).boundedDerivedObject
The first vertex of a divisor-chain step is the preceding prefix twist.
Equations
- A.lineBundleStepTriangleObj₁Iso L j hj = id (⋯.mp ((A.curve ⟨j, hj⟩).cohLineBundleTwistBoundedTriangleObj₁Iso L (A.prefixDivisor (j + 1) ⋯)))
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.MinusTwoCurveChain.lineBundleStepTriangleObj₂Iso
{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}
{n : ℕ}
(A : T.MinusTwoCurveChain n)
(L : Scheme.Modules.LineBundleData Y)
(j : ℕ)
(hj : j < n)
:
(A.lineBundleStepTriangle L j hj).obj₂ ≅ (L.tensor (Scheme.CartierDivisor.lineBundleData (A.prefixDivisor (j + 1) ⋯))).boundedDerivedObject
The second vertex of a divisor-chain step is the extended prefix twist.
Equations
- A.lineBundleStepTriangleObj₂Iso L j hj = (A.curve ⟨j, hj⟩).cohLineBundleTwistBoundedTriangleObj₂Iso L (A.prefixDivisor (j + 1) ⋯)
Instances For
structure
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData
{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)
:
Type (max t u)
The geometric data behind a block decomposition in Paper II, Proposition 1.4 and Lemma 1.9.
memberClass is the formula
L_{ij} = L_{i1} ⊗ O(R_{i1}+⋯+R_{i,j-1}) in the Picard group.
The Picard formula proves that each supplied line-bundle representative is
isomorphic to the corresponding tensor product by O(prefix j); the adapter
chooses such isomorphisms. The divisor-derived triangle is therefore
constructed below rather than stored. Only residual orthogonality of its
quotient remains supplied.
- chain (i : I) : T.MinusTwoCurveChain (B.blocks.length i - 1)
A chain of length one less than each exceptional block.
- memberClass (i : I) (j : Fin (B.blocks.length i)) : (T.bundles (B.bundleIndex ⟨i, j⟩)).toPic = (T.bundles (B.firstBundleIndex i)).toPic * Scheme.CartierDivisor.toPic ((self.chain i).prefixDivisor ↑j ⋯)
The Picard-class formula for every member of every block.
- quotientOrthogonal (i : I) (j : ℕ) (hj : j + 1 < B.blocks.length i) : (T.residualComponent exceptional semiorthogonal).rightOrthogonal ((self.chain i).lineBundleStepTriangle (T.bundles (B.firstBundleIndex i)) j ⋯).obj₃
The quotient in each canonical divisor-chain step is killed by the residual projection. This is the remaining geometric input after the distinguished triangle itself has been constructed from the Cartier sequence.
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.memberLineIso
{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}
(A : T.PaperCurveChainData B)
(i : I)
(j : Fin (B.blocks.length i))
:
(T.bundles (B.bundleIndex ⟨i, j⟩)).line ≅ ((T.bundles (B.firstBundleIndex i)).tensor
(Scheme.CartierDivisor.lineBundleData ((A.chain i).prefixDivisor ↑j ⋯))).line
The Picard-class formula chooses an isomorphism from each selected bundle to the first bundle tensored by the corresponding Cartier prefix.
Equations
- A.memberLineIso i j = Classical.choice ⋯
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.memberBoundedDerivedIso
{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}
(A : T.PaperCurveChainData B)
(i : I)
(j : Fin (B.blocks.length i))
:
(T.bundles (B.bundleIndex ⟨i, j⟩)).boundedDerivedObject ≅ ((T.bundles (B.firstBundleIndex i)).tensor
(Scheme.CartierDivisor.lineBundleData ((A.chain i).prefixDivisor ↑j ⋯))).boundedDerivedObject
The member-line isomorphism lifted to bounded coherent derived objects.
Equations
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.blockMemberTensorIso
{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}
(A : T.PaperCurveChainData B)
(i : I)
(j : Fin (B.blocks.length i))
:
(B.blocks.collection i).obj j ≅ ((T.bundles (B.firstBundleIndex i)).tensor
(Scheme.CartierDivisor.lineBundleData ((A.chain i).prefixDivisor ↑j ⋯))).boundedDerivedObject
Identify a block member with its canonical tensor-by-prefix derived object, combining the block presentation and the Picard-class formula.
Equations
- A.blockMemberTensorIso i j = B.bundleIso ⟨i, j⟩ ≪≫ A.memberBoundedDerivedIso i j
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.stepTriangle
{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}
(A : T.PaperCurveChainData B)
(i : I)
(j : ℕ)
(hj : j + 1 < B.blocks.length i)
:
The canonical divisor-derived triangle underlying the j-th step of a
paper block.
Equations
- A.stepTriangle i j hj = (A.chain i).lineBundleStepTriangle (T.bundles (B.firstBundleIndex i)) j ⋯
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.stepTriangleObj₁Iso
{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}
(A : T.PaperCurveChainData B)
(i : I)
(j : ℕ)
(hj : j + 1 < B.blocks.length i)
:
Identify the source of the canonical step triangle with the j-th block
member.
Equations
- A.stepTriangleObj₁Iso i j hj = (A.chain i).lineBundleStepTriangleObj₁Iso (T.bundles (B.firstBundleIndex i)) j ⋯ ≪≫ (A.blockMemberTensorIso i ⟨j, ⋯⟩).symm
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.stepTriangleObj₂Iso
{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}
(A : T.PaperCurveChainData B)
(i : I)
(j : ℕ)
(hj : j + 1 < B.blocks.length i)
:
Identify the target of the canonical step triangle with the next block member.
Equations
- A.stepTriangleObj₂Iso i j hj = (A.chain i).lineBundleStepTriangleObj₂Iso (T.bundles (B.firstBundleIndex i)) j ⋯ ≪≫ (A.blockMemberTensorIso i ⟨j + 1, hj⟩).symm
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.projectionTriangle
{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}
(A : T.PaperCurveChainData B)
(i : I)
(j : ℕ)
(hj : j + 1 < B.blocks.length i)
:
The canonical divisor triangle transported to the paper's chosen block representatives. Its first morphism is the required successive block map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.stepTriangleIso
{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}
(A : T.PaperCurveChainData B)
(i : I)
(j : ℕ)
(hj : j + 1 < B.blocks.length i)
:
Canonical comparison from the divisor step triangle to its transport onto the selected block representatives.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.projectionTriangle_distinguished
{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}
(A : T.PaperCurveChainData B)
(i : I)
(j : ℕ)
(hj : j + 1 < B.blocks.length i)
:
The transported paper-block step triangle is distinguished.
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.projectionTriangles
{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}
(A : T.PaperCurveChainData B)
:
B.blocks.ProjectionChainData (T.residualComponent exceptional semiorthogonal)
Construct the complete projection-chain triangle data from Cartier sequences, Picard-class identifications, and the supplied quotient orthogonality.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperCurveChainData.projectionIso
{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}
(A : T.PaperCurveChainData B)
(Q : T.PaperResidualProjectionData exceptional semiorthogonal)
(i : I)
(j : Fin (B.blocks.length i))
:
B.projectedObject Q i ≅ CategoryTheory.ObjectProperty.RightProjectionData.project Q ((B.blocks.collection i).obj j)
Paper II, Remark 2.3(ii): every member of a block has the same residual projection as its first member.
Unlike the earlier supplied statement seam, this is proved from the successive divisor triangles and their residual-orthogonality.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Ext computations and classification constructors #
structure
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionExtData
{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}
(B : T.PaperBlockData exceptional semiorthogonal (Fin 10))
(Q : T.PaperResidualProjectionData exceptional semiorthogonal)
:
Paper I's Ext computations for the ten projected objects, separated from their Serre-shift identifications and the completeness argument.
- selfExt (i : Fin 10) : CategoryTheory.SerreFunctor.SphericalExtProfile 3 (B.projectedObject Q i)
Every projected object has the 3-spherical self-Ext profile.
- pairwise {i j : Fin 10} : i ≠ j → CategoryTheory.SerreFunctor.IsGradedOrthogonal (B.projectedObject Q i) (B.projectedObject Q j)
Cross-Ext groups between distinct projections vanish in all degrees.
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIProjectionExtData.toProjectionClassificationData
{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.PaperIProjectionExtData B Q)
(singleton : ∀ (i : Fin 10), B.blocks.length i = 1)
(serreShift :
∀ (i : Fin 10),
Nonempty
(P.residualSerre.serre.S.obj (B.projectedObject Q i) ≅ (CategoryTheory.shiftFunctor (T.ResidualCategory exceptional semiorthogonal) 3).obj (B.projectedObject Q i)))
(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))
:
Assemble Paper I's projection classification package from the Ext calculation, the Serre action, and the remaining completeness theorem.
structure
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionExtData
{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)
{I : Type t}
[Fintype I]
(B : T.PaperBlockData exceptional semiorthogonal I)
(Q : T.PaperResidualProjectionData exceptional semiorthogonal)
:
Paper II's block-sensitive self-Ext and cross-Ext computations.
- sphericalExt (i : I) : B.blocks.length i = 1 → CategoryTheory.SerreFunctor.SphericalExtProfile 3 (B.projectedObject Q i)
Singleton blocks have the spherical Ext profile.
- pseudoprojectiveExt (i : I) : 2 ≤ B.blocks.length i → CategoryTheory.SerreFunctor.PseudoprojectiveExtProfile 3 (B.projectedObject Q i)
Longer blocks have the pseudoprojective Ext profile.
- serreShift (i : I) : Nonempty (P.residualSerre.serre.S.obj (B.projectedObject Q i) ≅ (CategoryTheory.shiftFunctor (T.ResidualCategory exceptional semiorthogonal) 3).obj (B.projectedObject Q i))
The common Serre-shift computation.
- pairwise {i j : I} : i ≠ j → CategoryTheory.SerreFunctor.IsGradedOrthogonal (B.projectedObject Q i) (B.projectedObject Q j)
Cross-Ext groups between distinct blocks vanish in every degree.
Instances For
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionExtData.spherical_of_singleton
{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}
{I : Type t}
[Fintype I]
{B : T.PaperBlockData exceptional semiorthogonal I}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionExtData P B Q)
(i : I)
(hi : B.blocks.length i = 1)
:
The Ext and Serre computations make a singleton projection spherical.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionExtData.pseudoprojective_of_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}
{P : T.PaperCategoryData exceptional semiorthogonal}
{I : Type t}
[Fintype I]
{B : T.PaperBlockData exceptional semiorthogonal I}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionExtData P B Q)
(i : I)
(hi : 2 ≤ B.blocks.length i)
:
The Ext and Serre computations make a longer-block projection pseudoprojective.
theorem
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperIIProjectionExtData.toProjectionClassificationData
{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}
{I : Type t}
[Fintype I]
{B : T.PaperBlockData exceptional semiorthogonal I}
{Q : T.PaperResidualProjectionData exceptional semiorthogonal}
(A : T.PaperIIProjectionExtData P B Q)
(sphericalComplete :
∀ (E : T.ResidualCategory exceptional semiorthogonal),
CategoryTheory.SerreFunctor.IsSphericalObject P.residualSerre.serre 3 E ↔ ∃ (i : I), B.blocks.length i = 1 ∧ CategoryTheory.SerreFunctor.IsShiftOf E (B.projectedObject Q i))
(pseudoprojectiveComplete :
∀ (E : T.ResidualCategory exceptional semiorthogonal),
CategoryTheory.SerreFunctor.IsPseudoprojectiveObject P.residualSerre.serre 3 E ↔ ∃ (i : I), 2 ≤ B.blocks.length i ∧ CategoryTheory.SerreFunctor.IsShiftOf E (B.projectedObject Q i))
:
Assemble Paper II's full classification package after supplying only the two global completeness statements.
Fourier--Mukai extension between two Enriques surfaces #
@[reducible, inline]
abbrev
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperResidualKernelEquivalence
{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 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)
:
Type (u + 1)
A Fourier--Mukai-type equivalence between the residual categories of two
Enriques block decompositions. The block residuals are identified with the
previously constructed neutral residual components by PaperBlockData.residual_eq.
Equations
- T₁.PaperResidualKernelEquivalence T₂ B₁ B₂ corr = CategoryTheory.Triangulated.FourierMukai.ResidualKernelEquivalence B₁.blocks B₂.blocks corr
Instances For
@[reducible, inline]
abbrev
AlgebraicGeometry.EnriquesSurface.IsotropicCollection.PaperExceptionalBlockExtensionData
{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 J : Type t}
[Fintype I]
[Fintype J]
(B₁ : T₁.PaperBlockData exceptional₁ semiorthogonal₁ I)
(B₂ : T₂.PaperBlockData exceptional₂ semiorthogonal₂ J)
{W W' : Type u}
[CategoryTheory.Category.{u_1, u} W]
[CategoryTheory.Category.{u_2, u} W']
(corr : CategoryTheory.Triangulated.FourierMukai.Correspondence (DerivedCat Y₁) (DerivedCat Y₂) W)
(corr' : CategoryTheory.Triangulated.FourierMukai.Correspondence (DerivedCat Y₂) (DerivedCat Y₁) W')
(R : T₁.PaperResidualKernelEquivalence T₂ B₁ B₂ corr)
:
Type (max (max (max t (u + 1)) u) (u + 1))
The conclusion of the papers' finite extension argument, specialized to
the exceptional blocks of two Enriques surfaces. Its
ambientEquivalence is the promoted equivalence of ambient derived
categories, and its objectIso uses one common shift on every member of a
block.
Equations
- T₁.PaperExceptionalBlockExtensionData T₂ B₁ B₂ corr corr' R = CategoryTheory.Triangulated.FourierMukai.ExceptionalBlockExtensionData B₁.blocks B₂.blocks corr corr' R