Fourier--Mukai extension across exceptional blocks

This file gives precise interfaces for the extension results used in arXiv:1912.04332v2, Propositions 2.4--2.5 and Theorem 5.1, and arXiv:2104.13610v2, Proposition 3.2 and Theorem 3.3.

There are three layers.

• KernelEquivalence is a Fourier--Mukai transform known to be an equivalence. Its constructor from a kernel-presented right adjoint with invertible unit and counit is a theorem, not supplied data.
• OneStepExtensionData is the exact conclusion of the one-object extension proposition: a new kernel agrees on the old component, maps the new exceptional object, kills the remaining orthogonal, and is an equivalence on the enlarged triangulated span.
• ExceptionalBlockExtensionData is the finite iteration's conclusion: an ambient kernel equivalence extending the residual equivalence and matching every object of every exceptional block, with one common shift per block.

The kernel constructed in the papers is a cone of a morphism of kernels. The abstract functorial dg-cone construction is rooted at DGFunctor.HomogeneousNatTrans.ConeData; FourierMukai.KernelCone maps such cones pointwise through a correspondence, and FourierMukai.CounitKernelConeData is the reusable specialization when the kernel morphism realizes an adjunction counit. The geometric identification of the kernel category with an H⁰, the ordinary kernel morphism with its exact counit-transform equation, an enhancement, and exactness of kernel evaluation remain the #853--#855 realization boundary. Accordingly the two extension structures are still explicitly result data. Once their adjunction fields are supplied, however, the ambient equivalence itself is derived through Adjunction.toEquivalence.

structure CategoryTheory.Triangulated.FourierMukai.KernelEquivalence {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Category.{v', u'} Y] [Category.{v'', u''} W] (corr : Correspondence X Y W) : Type (max (max (max (max u u') u'') v) v')

An equivalence between two categories presented by a Fourier--Mukai kernel. Unlike KernelAutoequivalence, the source and target may differ.

• kernel : W

  The kernel presenting the forward equivalence.

• equiv : X ≌ Y

  The underlying equivalence.

• iso : self.equiv.functor ≅ corr.transform self.kernel

  Identification of the equivalence functor with the kernel transform.

@[reducible]

noncomputable def CategoryTheory.Triangulated.FourierMukai.KernelEquivalence.ofRightAdjointKernel {X : Type u} {Y : Type u'} {W : Type u''} {W' : Type u'''} [Category.{v, u} X] [Category.{v', u'} Y] [Category.{v'', u''} W] [Category.{v''', u'''} W'] (corr : Correspondence X Y W) (corr' : Correspondence Y X W') (K : W) (R : RightAdjointKernelData corr corr' K) [∀ (A : X), IsIso (R.adj.unit.app A)] [∀ (B : Y), IsIso (R.adj.counit.app B)] : KernelEquivalence corr

A kernel-presented right adjunction with invertible unit and counit gives a kernel equivalence. The equivalence is Adjunction.toEquivalence, and the forward functor is the original transform definitionally.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelEquivalence.ofRightAdjointKernel_kernel {X : Type u} {Y : Type u'} {W : Type u''} {W' : Type u'''} [Category.{v, u} X] [Category.{v', u'} Y] [Category.{v'', u''} W] [Category.{v''', u'''} W'] (corr : Correspondence X Y W) (corr' : Correspondence Y X W') (K : W) (R : RightAdjointKernelData corr corr' K) [∀ (A : X), IsIso (R.adj.unit.app A)] [∀ (B : Y), IsIso (R.adj.counit.app B)] : (ofRightAdjointKernel corr corr' K R).kernel = K

theorem CategoryTheory.Triangulated.FourierMukai.KernelEquivalence.transform_isEquivalence {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Category.{v', u'} Y] [Category.{v'', u''} W] (corr : Correspondence X Y W) (A : KernelEquivalence corr) : (corr.transform A.kernel).IsEquivalence

The transform presented by a kernel equivalence is an equivalence.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.adjoinObject {X : Type u} [Category.{v, u} X] [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] (P : ObjectProperty X) (E : X) : ObjectProperty X

The full triangulated property generated by an old component P and one new object E.

Equations

• CategoryTheory.Triangulated.FourierMukai.adjoinObject P E = (P ⊔ CategoryTheory.ObjectProperty.singleton E).triangEnvelope

structure CategoryTheory.Triangulated.FourierMukai.ResidualKernelEquivalence {k : Type w} [Field k] {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Linear k X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Linear k Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {I : Type t} {J : Type t'} (B_X : OrthogonalExceptionalBlocks k X I) (B_Y : OrthogonalExceptionalBlocks k Y J) (corr : Correspondence X Y W) : Type (max (max (max (max u u') u'') v) v')

A residual equivalence presented by the restriction of an ambient Fourier--Mukai transform.

This is the papers' phrase "an equivalence of Fourier--Mukai type" written against the existing correspondence interface.

• equiv : B_X.ResidualCategory ≌ B_Y.ResidualCategory

  The equivalence of residual categories.

• kernel : W

  An ambient kernel inducing that equivalence on the residual category.

• restrictionIso : B_X.residual.ι.comp (corr.transform self.kernel) ≅ self.equiv.functor.comp B_Y.residual.ι

  The restriction of the transform is the given residual equivalence.

structure CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] (P : ObjectProperty X) (Q : ObjectProperty Y) (E : X) (F : Y) (base : P.FullSubcategory ≌ Q.FullSubcategory) (corr : Correspondence X Y W) (oldKernel : W) : Type (max (max (max (max (max u u') u'') v) v') v'')

The conclusion of one application of the Fourier--Mukai extension proposition across a single exceptional object.

The fields are intentionally conclusions rather than assumptions disguised as a theorem: constructing newKernel requires the functorial cone of kernels which the dg lane has not yet delivered.

• newKernel : W

  The extended Fourier--Mukai kernel.

• kernelMap : self.newKernel ⟶ oldKernel

  The kernel morphism from the extension to the preceding kernel, as in Paper I, Proposition 2.4.

• agreesWithOld : P.ι.comp (corr.transform self.newKernel) ≅ P.ι.comp (corr.transform oldKernel)

  The induced transform comparison is an isomorphism on the old component. This is the categorical content of Proposition 2.4(1).

• transformCommShift : (corr.transform self.newKernel).CommShift ℤ

  The extended transform commutes with shifts.

• transformTriangulated : (corr.transform self.newKernel).IsTriangulated

  The extended transform is exact.

• mapsAdjoin (A : (adjoinObject P E).FullSubcategory) : adjoinObject Q F ((corr.transform self.newKernel).obj A.obj)

  The extended transform maps the enlarged source span into the enlarged target span.

• enlargedEquiv : (adjoinObject P E).FullSubcategory ≌ (adjoinObject Q F).FullSubcategory

  The induced equivalence of enlarged components.

• enlargedIso : (adjoinObject P E).ι.comp (corr.transform self.newKernel) ≅ self.enlargedEquiv.functor.comp (adjoinObject Q F).ι

  The enlarged equivalence is induced by the extended transform.

• agreesOnBase : P.ι.comp (corr.transform self.newKernel) ≅ base.functor.comp Q.ι

  On the old component the new transform agrees with the old equivalence.

• objectIso : (corr.transform self.newKernel).obj E ≅ F

  The newly adjoined source object is sent to the newly adjoined target object.

• annihilates (A : X) : (adjoinObject P E).leftOrthogonal A → Limits.IsZero ((corr.transform self.newKernel).obj A)

  The remaining left orthogonal is annihilated, allowing the next induction step.

noncomputable def CategoryTheory.Triangulated.FourierMukai.restrictedTransform {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] (P : ObjectProperty X) (Q : ObjectProperty Y) (E : X) (F : Y) (corr : Correspondence X Y W) (kernel : W) (mapsAdjoin : ∀ (A : (adjoinObject P E).FullSubcategory), adjoinObject Q F ((corr.transform kernel).obj A.obj)) : Functor (adjoinObject P E).FullSubcategory (adjoinObject Q F).FullSubcategory

The restriction of a kernel transform to a one-object enlargement, provided the transform maps that enlargement to the target enlargement.

Equations

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

structure CategoryTheory.Triangulated.FourierMukai.OneStepExtensionCriterion {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] (P : ObjectProperty X) (Q : ObjectProperty Y) (E : X) (F : Y) (base : P.FullSubcategory ≌ Q.FullSubcategory) (corr : Correspondence X Y W) (oldKernel : W) : Type (max (max (max (max u u'') v) v') v'')

A one-step extension criterion in the form proved in the papers.

The enlarged equivalence is not a field: it follows from full faithfulness and essential surjectivity of the restricted extended transform. This is the categorical implication in the final part of the one-object extension argument, separated from the geometric/dg construction of newKernel.

• newKernel : W

  The extended Fourier--Mukai kernel.

• kernelMap : self.newKernel ⟶ oldKernel

  The kernel morphism from the extension to the preceding kernel.

• agreesWithOld : P.ι.comp (corr.transform self.newKernel) ≅ P.ι.comp (corr.transform oldKernel)

  The extended transform agrees with the old one on the old component.

• transformCommShift : (corr.transform self.newKernel).CommShift ℤ

  The extended transform commutes with shifts.

• transformTriangulated : (corr.transform self.newKernel).IsTriangulated

  The extended transform is exact.

• mapsAdjoin (A : (adjoinObject P E).FullSubcategory) : adjoinObject Q F ((corr.transform self.newKernel).obj A.obj)

  The extended transform preserves the enlarged spans.

• restrictedFullyFaithful : (restrictedTransform P Q E F corr self.newKernel ⋯).FullyFaithful

  The restricted transform is fully faithful.

• restrictedEssSurj : (restrictedTransform P Q E F corr self.newKernel ⋯).EssSurj

  The restricted transform is essentially surjective.

• agreesOnBase : P.ι.comp (corr.transform self.newKernel) ≅ base.functor.comp Q.ι

  On the old component the new transform induces the old equivalence.

• objectIso : (corr.transform self.newKernel).obj E ≅ F

  The newly adjoined object maps to its target.

• annihilates (A : X) : (adjoinObject P E).leftOrthogonal A → Limits.IsZero ((corr.transform self.newKernel).obj A)

  The remaining left orthogonal is annihilated.

noncomputable def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionCriterion.enlargedEquiv {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionCriterion P Q E F base corr oldKernel) : (adjoinObject P E).FullSubcategory ≌ (adjoinObject Q F).FullSubcategory

The equivalence of enlarged spans derived from full faithfulness and essential surjectivity of the restricted transform.

Equations

• A.enlargedEquiv = (CategoryTheory.Triangulated.FourierMukai.restrictedTransform P Q E F corr A.newKernel ⋯).asEquivalence

noncomputable def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionCriterion.enlargedIso {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionCriterion P Q E F base corr oldKernel) : (adjoinObject P E).ι.comp (corr.transform A.newKernel) ≅ A.enlargedEquiv.functor.comp (adjoinObject Q F).ι

The derived enlarged equivalence is induced by the extended kernel transform.

Equations

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionCriterion.toExtensionData {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionCriterion P Q E F base corr oldKernel) : OneStepExtensionData P Q E F base corr oldKernel

Package the criterion as the one-step result consumed by finite extension induction.

Equations

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.restrictedFunctor {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) : Functor (adjoinObject P E).FullSubcategory (adjoinObject Q F).FullSubcategory

The actual restricted functor induced by the new kernel.

Equations

• A.restrictedFunctor = CategoryTheory.Triangulated.FourierMukai.restrictedTransform P Q E F corr A.newKernel ⋯

noncomputable def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.restrictedFunctorIso {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) : A.restrictedFunctor ≅ A.enlargedEquiv.functor

The supplied enlarged equivalence has the restricted transform as its underlying functor, up to natural isomorphism.

Equations

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

def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.transformKernelMap {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) : corr.transform A.newKernel ⟶ corr.transform oldKernel

The supplied kernel map has a canonical transform map. This is the natural-transformation seam consumed by an eventual dg kernel-cone construction; the extension data still supplies the kernel and the map.

Equations

• A.transformKernelMap = corr.kernelTransform.map A.kernelMap

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.transformKernelMap_app {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) (E✝ : X) : A.transformKernelMap.app E✝ = corr.push.map ((corr.tensor.map A.kernelMap).app (corr.pull.obj E✝))

def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.oldAgreesOnBase {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) : P.ι.comp (corr.transform oldKernel) ≅ base.functor.comp Q.ι

The old transform also presents the original base equivalence.

The supplied comparison agreesWithOld points from the new transform to the old one, while agreesOnBase points from the new transform to the base equivalence. Cancelling the former is the restriction statement that is needed when the kernel-cone stage is fed into the next induction step.

Equations

• A.oldAgreesOnBase = A.agreesWithOld.symm ≪≫ A.agreesOnBase

def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.restrictedTransformCompιIso {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) : A.restrictedFunctor.comp (adjoinObject Q F).ι ≅ (adjoinObject P E).ι.comp (corr.transform A.newKernel)

The restricted transform, followed by the target inclusion, is the ambient transform restricted to the enlarged source.

This is the canonical comparison supplied by the full-subcategory lift; it does not use the enlarged equivalence and therefore remains available at the kernel-cone boundary.

Equations

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.restrictedEquivalence {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) : (adjoinObject P E).FullSubcategory ≌ (adjoinObject Q F).FullSubcategory

The enlarged equivalence with its functor changed to the actual restricted transform.

Equations

• A.restrictedEquivalence = A.enlargedEquiv.changeFunctor A.restrictedFunctorIso.symm

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.restrictedEquivalence_functor {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) : A.restrictedEquivalence.functor = A.restrictedFunctor

noncomputable def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.restrictedAdjunction {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) : A.restrictedFunctor ⊣ A.enlargedEquiv.inverse

The adjunction between the restricted transform and the inverse of the enlarged equivalence. It is derived from the equivalence and the comparison restrictedFunctorIso; no ambient adjoint is being asserted here.

Equations

• A.restrictedAdjunction = A.enlargedEquiv.toAdjunction.ofNatIsoLeft A.restrictedFunctorIso.symm

theorem CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.restrictedFunctor_isEquivalence {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) : A.restrictedFunctor.IsEquivalence

Kernel-presented adjunctions on one extension stages

structure CategoryTheory.Triangulated.FourierMukai.RightAdjunctionData {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) {W' : Type u'''} [Category.{v''', u'''} W'] (corr' : Correspondence Y X W') : Type (max (max (max (max u u') u''') v) v')

Data which restricts a kernel-presented ambient right adjoint to the enlarged one-step stages.

The ambient adjunction and the target-to-source preservation are genuine geometric inputs. The comparison between the restricted right adjoint and the inverse of the enlarged equivalence is deliberately not a field: both are right adjoint to the same restricted transform, so right-adjoint uniqueness supplies the canonical comparison.

• rightAdjoint : RightAdjointKernelData corr corr' A.newKernel

  A kernel-presented right adjoint of the extended transform.

• mapsAdjoin (B : (adjoinObject Q F).FullSubcategory) : adjoinObject P E ((corr'.transform self.rightAdjoint.adjKernel).obj B.obj)

  The right-adjoint transform preserves the target enlarged span.

noncomputable def CategoryTheory.Triangulated.FourierMukai.RightAdjunctionData.restrictedRightAdjoint {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) {W' : Type u'''} [Category.{v''', u'''} W'] {corr' : Correspondence Y X W'} (R : RightAdjunctionData A corr') : Functor (adjoinObject Q F).FullSubcategory (adjoinObject P E).FullSubcategory

The right adjoint restricted to the enlarged target and source spans.

Equations

• CategoryTheory.Triangulated.FourierMukai.RightAdjunctionData.restrictedRightAdjoint A R = CategoryTheory.Triangulated.FourierMukai.restrictedTransform Q P F E corr' R.rightAdjoint.adjKernel ⋯

noncomputable def CategoryTheory.Triangulated.FourierMukai.RightAdjunctionData.kernelRestrictedAdjunction {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) {W' : Type u'''} [Category.{v''', u'''} W'] {corr' : Correspondence Y X W'} (R : RightAdjunctionData A corr') : A.restrictedFunctor ⊣ restrictedRightAdjoint A R

Restrict the ambient kernel-presented adjunction to the two enlarged stages. The two comparison isomorphisms are the canonical lift comparisons, so the construction is exactly Adjunction.restrictFullyFaithful.

Equations

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.RightAdjunctionData.restrictedInverseIso {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) {W' : Type u'''} [Category.{v''', u'''} W'] {corr' : Correspondence Y X W'} (R : RightAdjunctionData A corr') : restrictedRightAdjoint A R ≅ A.enlargedEquiv.inverse

The canonical comparison between the restricted kernel-presented right adjoint and the inverse of the enlarged equivalence. It is forced by the two adjunctions with common left adjoint A.restrictedFunctor.

Equations

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

theorem CategoryTheory.Triangulated.FourierMukai.RightAdjunctionData.restrictedRightAdjoint_isEquivalence {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) {W' : Type u'''} [Category.{v''', u'''} W'] {corr' : Correspondence Y X W'} (R : RightAdjunctionData A corr') : (restrictedRightAdjoint A R).IsEquivalence

The restricted kernel-presented right adjoint is an equivalence because it is canonically isomorphic to the inverse of the enlarged equivalence.

noncomputable def CategoryTheory.Triangulated.FourierMukai.RightAdjunctionData.stageAdjunction {X : Type u} {Y : Type u'} {W : Type u''} [Category.{v, u} X] [Preadditive X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] {P : ObjectProperty X} {Q : ObjectProperty Y} {E : X} {F : Y} {base : P.FullSubcategory ≌ Q.FullSubcategory} {corr : Correspondence X Y W} {oldKernel : W} (A : OneStepExtensionData P Q E F base corr oldKernel) {W' : Type u'''} [Category.{v''', u'''} W'] {corr' : Correspondence Y X W'} (R : RightAdjunctionData A corr') : A.restrictedFunctor ⊣ A.enlargedEquiv.inverse

Express the canonical restricted kernel adjunction with the inverse of the supplied stage equivalence as its right adjoint.

Equations

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

structure CategoryTheory.Triangulated.FourierMukai.ExceptionalBlockExtensionData {k : Type w} [Field k] {X : Type u} {Y : Type u'} {W : Type u''} {W' : Type u'''} [Category.{v, u} X] [Preadditive X] [Linear k X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Linear k Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] [Category.{v''', u'''} W'] {I : Type t} {J : Type t'} (B_X : OrthogonalExceptionalBlocks k X I) (B_Y : OrthogonalExceptionalBlocks k Y J) (corr : Correspondence X Y W) (corr' : Correspondence Y X W') (R : ResidualKernelEquivalence B_X B_Y corr) : Type (max (max (max (max (max (max (max t t') u) u') u'') u''') v) v')

The finite blockwise extension conclusion of Paper I, Theorem 5.1 and Paper II, Theorem 3.3.

blockEquiv and length_eq record equality of decomposition type. objectIso uses the same shift for every member of a block, exactly as in Paper II. The ambient equivalence is not stored redundantly: a kernel-presented right adjoint and pointwise invertibility of its unit and counit are stored, and toKernelEquivalence derives it.

• kernel : W

  The final extended kernel.

• rightAdjoint : RightAdjointKernelData corr corr' self.kernel

  A kernel-presented right adjoint of the final transform.

• unitIsIso (A : X) : IsIso (self.rightAdjoint.adj.unit.app A)

  Full faithfulness half of the final equivalence.

• counitIsIso (B : Y) : IsIso (self.rightAdjoint.adj.counit.app B)

  Essential-surjectivity half of the final equivalence.

• transformCommShift : (corr.transform self.kernel).CommShift ℤ

  The final transform commutes with shifts.

• transformTriangulated : (corr.transform self.kernel).IsTriangulated

  The final transform is exact.

• residualIso : B_X.residual.ι.comp (corr.transform self.kernel) ≅ R.equiv.functor.comp B_Y.residual.ι

  The final transform still restricts to the original residual equivalence.

• blockEquiv : I ≃ J

  Reordering of the exceptional blocks.

• length_eq (i : I) : B_X.length i = B_Y.length (self.blockEquiv i)

  Corresponding blocks have equal length.

• shift : I → ℤ

  The common shift attached to each source block.

• objectIso (i : I) (j : Fin (B_X.length i)) : (corr.transform self.kernel).obj ((B_X.collection i).obj j) ≅ (shiftFunctor Y (self.shift i)).obj ((B_Y.collection (self.blockEquiv i)).obj (Fin.cast ⋯ j))

  Every member of a source block maps to the corresponding member of the target block with the common block shift.

noncomputable def CategoryTheory.Triangulated.FourierMukai.ExceptionalBlockExtensionData.toKernelEquivalence {k : Type w} [Field k] {X : Type u} {Y : Type u'} {W : Type u''} {W' : Type u'''} [Category.{v, u} X] [Preadditive X] [Linear k X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Linear k Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] [Category.{v''', u'''} W'] {I : Type t} {J : Type t'} {B_X : OrthogonalExceptionalBlocks k X I} {B_Y : OrthogonalExceptionalBlocks k Y J} {corr : Correspondence X Y W} {corr' : Correspondence Y X W'} {R : ResidualKernelEquivalence B_X B_Y corr} (A : ExceptionalBlockExtensionData B_X B_Y corr corr' R) : KernelEquivalence corr

The ambient Fourier--Mukai equivalence, derived from the final adjunction and its invertible unit and counit.

Equations

• A.toKernelEquivalence = CategoryTheory.Triangulated.FourierMukai.KernelEquivalence.ofRightAdjointKernel corr corr' A.kernel A.rightAdjoint

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.ExceptionalBlockExtensionData.toKernelEquivalence_kernel {k : Type w} [Field k] {X : Type u} {Y : Type u'} {W : Type u''} {W' : Type u'''} [Category.{v, u} X] [Preadditive X] [Linear k X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Linear k Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] [Category.{v''', u'''} W'] {I : Type t} {J : Type t'} {B_X : OrthogonalExceptionalBlocks k X I} {B_Y : OrthogonalExceptionalBlocks k Y J} {corr : Correspondence X Y W} {corr' : Correspondence Y X W'} {R : ResidualKernelEquivalence B_X B_Y corr} (A : ExceptionalBlockExtensionData B_X B_Y corr corr' R) : A.toKernelEquivalence.kernel = A.kernel

theorem CategoryTheory.Triangulated.FourierMukai.ExceptionalBlockExtensionData.transform_isEquivalence {k : Type w} [Field k] {X : Type u} {Y : Type u'} {W : Type u''} {W' : Type u'''} [Category.{v, u} X] [Preadditive X] [Linear k X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Linear k Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] [Category.{v''', u'''} W'] {I : Type t} {J : Type t'} {B_X : OrthogonalExceptionalBlocks k X I} {B_Y : OrthogonalExceptionalBlocks k Y J} {corr : Correspondence X Y W} {corr' : Correspondence Y X W'} {R : ResidualKernelEquivalence B_X B_Y corr} (A : ExceptionalBlockExtensionData B_X B_Y corr corr' R) : (corr.transform A.kernel).IsEquivalence

The final kernel transform is an equivalence of the ambient categories.

noncomputable def CategoryTheory.Triangulated.FourierMukai.ExceptionalBlockExtensionData.ambientEquivalence {k : Type w} [Field k] {X : Type u} {Y : Type u'} {W : Type u''} {W' : Type u'''} [Category.{v, u} X] [Preadditive X] [Linear k X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Linear k Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] [Category.{v''', u'''} W'] {I : Type t} {J : Type t'} {B_X : OrthogonalExceptionalBlocks k X I} {B_Y : OrthogonalExceptionalBlocks k Y J} {corr : Correspondence X Y W} {corr' : Correspondence Y X W'} {R : ResidualKernelEquivalence B_X B_Y corr} (A : ExceptionalBlockExtensionData B_X B_Y corr corr' R) : X ≌ Y

The induced ambient equivalence, exposed directly for downstream Torelli consumers.

Equations

• A.ambientEquivalence = A.toKernelEquivalence.equiv

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.ExceptionalBlockExtensionData.ambientEquivalence_functor {k : Type w} [Field k] {X : Type u} {Y : Type u'} {W : Type u''} {W' : Type u'''} [Category.{v, u} X] [Preadditive X] [Linear k X] [Limits.HasZeroObject X] [HasShift X ℤ] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Category.{v', u'} Y] [Preadditive Y] [Linear k Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Category.{v'', u''} W] [Category.{v''', u'''} W'] {I : Type t} {J : Type t'} {B_X : OrthogonalExceptionalBlocks k X I} {B_Y : OrthogonalExceptionalBlocks k Y J} {corr : Correspondence X Y W} {corr' : Correspondence Y X W'} {R : ResidualKernelEquivalence B_X B_Y corr} (A : ExceptionalBlockExtensionData B_X B_Y corr corr' R) : A.ambientEquivalence.functor = corr.transform A.kernel