Finite induction of Fourier--Mukai extension steps

ExceptionalExtension.lean states the output of one kernel-cone extension. This file performs the finite categorical induction which the two refined Torelli papers use: after adjoining corresponding exceptional objects one at a time, the final kernel restricts to an equivalence on the iterated spans.

The construction is deliberately separated from the dg seam. An ExtensionSequenceData can only be built by providing a genuine OneStepExtensionData at every successor. Once those steps exist, however, the final kernel, final equivalence, and its presentation by the transform are derived recursively rather than supplied as a second finite conclusion.

When the two final spans are the top object properties, the restricted equivalence is promoted directly to an equivalence of the ambient categories. This is the route taken in the papers and does not require a separate Bondal--Orlov unit/counit criterion.

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

Iteratively adjoin a finite ordered list of objects to a triangulated object property.

Equations

• CategoryTheory.Triangulated.FourierMukai.adjoinList P [] = P
• CategoryTheory.Triangulated.FourierMukai.adjoinList P (E :: objects) = CategoryTheory.Triangulated.FourierMukai.adjoinList (CategoryTheory.Triangulated.FourierMukai.adjoinObject P E) objects

@[simp]

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.adjoinList_cons {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) (objects : List X) : adjoinList P (E :: objects) = adjoinList (adjoinObject P E) objects

theorem CategoryTheory.Triangulated.FourierMukai.le_adjoinList {X : Type u} [Category.{v, u} X] [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] (P : ObjectProperty X) (objects : List X) : P ≤ adjoinList P objects

The initial component remains inside every finite iterated span.

theorem CategoryTheory.Triangulated.FourierMukai.singleton_le_adjoinList_of_mem {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} {objects : List X} (hE : E ∈ objects) : ObjectProperty.singleton E ≤ adjoinList P objects

Every object in the adjoining list belongs to the resulting iterated span.

theorem CategoryTheory.Triangulated.FourierMukai.adjoinList_isTriangulated {X : Type u} [Category.{v, u} X] [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [IsTriangulated X] (P : ObjectProperty X) (E : X) (objects : List X) : (adjoinList P (E :: objects)).IsTriangulated

Adjoining at least one object produces a triangulated iterated span.

theorem CategoryTheory.Triangulated.FourierMukai.adjoinList_isStableUnderRetracts {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) (objects : List X) : (adjoinList P (E :: objects)).IsStableUnderRetracts

Adjoining at least one object produces an iterated span closed under retracts.

theorem CategoryTheory.Triangulated.FourierMukai.adjoinList_eq_top_of_rightAdmissible {X : Type u} [Category.{v, u} X] [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [IsTriangulated X] (T P : ObjectProperty X) (E : X) (objects : List X) (hT : T.IsRightAdmissible) (hP : P = T.rightOrthogonal) (hcover : T ≤ adjoinList P (E :: objects)) : adjoinList P (E :: objects) = ⊤

If the objects adjoined to a residual component contain the entire exceptional part, right admissibility proves that the final iterated span is the whole category.

This is the generation step used after the finite kernel induction: the SOD triangle writes every object as an extension of an exceptional object by a residual object, and the final span is closed under those extensions.

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

A kernel whose transform presents an equivalence between two current extension stages.

• kernel : W

  The kernel at this stage.

• equiv : P.FullSubcategory ≌ Q.FullSubcategory

  The equivalence between the current source and target spans.

• restrictionIso : P.ι.comp (corr.transform self.kernel) ≅ self.equiv.functor.comp Q.ι

  The stage equivalence is induced by restricting the kernel transform.

def CategoryTheory.Triangulated.FourierMukai.ResidualKernelEquivalence.toStage {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} (R : ResidualKernelEquivalence B_X B_Y corr) : KernelExtensionStage B_X.residual B_Y.residual corr

A residual Fourier--Mukai equivalence is the initial stage of the finite exceptional-extension induction.

Equations

• R.toStage = { kernel := R.kernel, equiv := R.equiv, restrictionIso := R.restrictionIso }

def CategoryTheory.Triangulated.FourierMukai.OneStepExtensionData.toStage {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) : KernelExtensionStage (adjoinObject P E) (adjoinObject Q F) corr

One successful application of the extension proposition is the next kernel-extension stage.

Equations

• A.toStage = { kernel := A.newKernel, equiv := A.enlargedEquiv, restrictionIso := A.enlargedIso }

inductive CategoryTheory.Triangulated.FourierMukai.ExtensionSequenceData {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] (corr : Correspondence X Y W) {P : ObjectProperty X} {Q : ObjectProperty Y} : KernelExtensionStage P Q corr → List X → List Y → Type (max (max (max (max (max u u') u'') v) v') v'')

A finite derivation made only from one-step Fourier--Mukai extensions.

The indices record the current stage, so the successor constructor changes both object properties, the kernel, and the restricted equivalence before continuing.

• nil {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] {corr : Correspondence X Y W} {P : ObjectProperty X} {Q : ObjectProperty Y} (stage : KernelExtensionStage P Q corr) : ExtensionSequenceData corr stage [] []
• cons {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] {corr : Correspondence X Y W} {P : ObjectProperty X} {Q : ObjectProperty Y} {stage : KernelExtensionStage P Q corr} {E : X} {F : Y} {source : List X} {target : List Y} (step : OneStepExtensionData P Q E F stage.equiv corr stage.kernel) (tail : ExtensionSequenceData corr step.toStage source target) : ExtensionSequenceData corr stage (E :: source) (F :: target)

noncomputable def CategoryTheory.Triangulated.FourierMukai.ExtensionSequenceData.finalStage {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} {corr : Correspondence X Y W} {stage : KernelExtensionStage P Q corr} {source : List X} {target : List Y} (A : ExtensionSequenceData corr stage source target) : KernelExtensionStage (adjoinList P source) (adjoinList Q target) corr

The final stage obtained by recursively consuming all one-step extensions.

Equations

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.ExtensionSequenceData.finalKernel {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} {corr : Correspondence X Y W} {stage : KernelExtensionStage P Q corr} {source : List X} {target : List Y} (A : ExtensionSequenceData corr stage source target) : W

The final extended kernel.

Equations

• A.finalKernel = A.finalStage.kernel

noncomputable def CategoryTheory.Triangulated.FourierMukai.ExtensionSequenceData.finalEquiv {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} {corr : Correspondence X Y W} {stage : KernelExtensionStage P Q corr} {source : List X} {target : List Y} (A : ExtensionSequenceData corr stage source target) : (adjoinList P source).FullSubcategory ≌ (adjoinList Q target).FullSubcategory

The equivalence between the two final iterated spans.

Equations

• A.finalEquiv = A.finalStage.equiv

noncomputable def CategoryTheory.Triangulated.FourierMukai.ExtensionSequenceData.finalRestrictionIso {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} {corr : Correspondence X Y W} {stage : KernelExtensionStage P Q corr} {source : List X} {target : List Y} (A : ExtensionSequenceData corr stage source target) : (adjoinList P source).ι.comp (corr.transform A.finalKernel) ≅ A.finalEquiv.functor.comp (adjoinList Q target).ι

The final equivalence is presented by the restriction of the final kernel transform.

Equations

• A.finalRestrictionIso = A.finalStage.restrictionIso

noncomputable def CategoryTheory.Triangulated.FourierMukai.ExtensionSequenceData.ambientEquivalence {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} {corr : Correspondence X Y W} {stage : KernelExtensionStage P Q corr} {source : List X} {target : List Y} (A : ExtensionSequenceData corr stage source target) (hX : adjoinList P source = ⊤) (hY : adjoinList Q target = ⊤) : X ≌ Y

If the iterated spans exhaust both categories, the final stage gives an ambient equivalence directly.

Equations

• A.ambientEquivalence hX hY = (CategoryTheory.ObjectProperty.topEquivalence X).symm.trans ((⋯.mp (⋯.mp A.finalEquiv)).trans (CategoryTheory.ObjectProperty.topEquivalence Y))

noncomputable def CategoryTheory.Triangulated.FourierMukai.ExtensionSequenceData.toKernelEquivalence {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} {corr : Correspondence X Y W} {stage : KernelExtensionStage P Q corr} {source : List X} {target : List Y} (A : ExtensionSequenceData corr stage source target) (hX : adjoinList P source = ⊤) (hY : adjoinList Q target = ⊤) : KernelEquivalence corr

The ambient equivalence remains presented by the final Fourier--Mukai kernel.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.ExtensionSequenceData.toKernelEquivalence_kernel {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} {corr : Correspondence X Y W} {stage : KernelExtensionStage P Q corr} {source : List X} {target : List Y} (A : ExtensionSequenceData corr stage source target) (hX : adjoinList P source = ⊤) (hY : adjoinList Q target = ⊤) : (A.toKernelEquivalence hX hY).kernel = A.finalKernel

theorem CategoryTheory.Triangulated.FourierMukai.ExtensionSequenceData.finalTransform_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} {corr : Correspondence X Y W} {stage : KernelExtensionStage P Q corr} {source : List X} {target : List Y} (A : ExtensionSequenceData corr stage source target) (hX : adjoinList P source = ⊤) (hY : adjoinList Q target = ⊤) : (corr.transform A.finalKernel).IsEquivalence

The final kernel transform is an equivalence once the iterated spans exhaust both ambient categories.

Generation-certified finite extension

structure CategoryTheory.Triangulated.FourierMukai.GeneratedExtensionSequenceData {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] (corr : Correspondence X Y W) (T_X : ObjectProperty X) (T_Y : ObjectProperty Y) (stage : KernelExtensionStage T_X.rightOrthogonal T_Y.rightOrthogonal corr) : Type (max (max (max (max (max u u') u'') v) v') v'')

A finite exceptional extension sequence together with the admissibility and coverage data which prove that its final source and target spans are the ambient categories.

The source and target lists are visibly nonempty because the papers adjoin ten exceptional objects. Coverage says their iterated spans contain the total exceptional parts; sourceGenerates and targetGenerates derive generation rather than storing it.

• sourceHead : X

  First source exceptional object.

• sourceTail : List X

  Remaining source exceptional objects.

• targetHead : Y

  First target exceptional object.

• targetTail : List Y

  Remaining target exceptional objects.

• sequence : ExtensionSequenceData corr stage (self.sourceHead :: self.sourceTail) (self.targetHead :: self.targetTail)

  The dependent sequence of one-object kernel extensions.

• sourceRightAdmissible : T_X.IsRightAdmissible

  The total source exceptional part is right admissible.

• sourceCover : T_X ≤ adjoinList T_X.rightOrthogonal (self.sourceHead :: self.sourceTail)

  The source list covers the total exceptional part.

• targetRightAdmissible : T_Y.IsRightAdmissible

  The total target exceptional part is right admissible.

• targetCover : T_Y ≤ adjoinList T_Y.rightOrthogonal (self.targetHead :: self.targetTail)

  The target list covers the total exceptional part.

theorem CategoryTheory.Triangulated.FourierMukai.GeneratedExtensionSequenceData.sourceGenerates {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] {T_X : ObjectProperty X} {T_Y : ObjectProperty Y} {corr : Correspondence X Y W} {stage : KernelExtensionStage T_X.rightOrthogonal T_Y.rightOrthogonal corr} (A : GeneratedExtensionSequenceData corr T_X T_Y stage) [IsTriangulated X] : adjoinList T_X.rightOrthogonal (A.sourceHead :: A.sourceTail) = ⊤

The source residual category and adjoined exceptional objects generate the ambient source category.

theorem CategoryTheory.Triangulated.FourierMukai.GeneratedExtensionSequenceData.targetGenerates {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] {T_X : ObjectProperty X} {T_Y : ObjectProperty Y} {corr : Correspondence X Y W} {stage : KernelExtensionStage T_X.rightOrthogonal T_Y.rightOrthogonal corr} (A : GeneratedExtensionSequenceData corr T_X T_Y stage) [IsTriangulated Y] : adjoinList T_Y.rightOrthogonal (A.targetHead :: A.targetTail) = ⊤

The target residual category and adjoined exceptional objects generate the ambient target category.

noncomputable def CategoryTheory.Triangulated.FourierMukai.GeneratedExtensionSequenceData.ambientEquivalence {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] {T_X : ObjectProperty X} {T_Y : ObjectProperty Y} {corr : Correspondence X Y W} {stage : KernelExtensionStage T_X.rightOrthogonal T_Y.rightOrthogonal corr} (A : GeneratedExtensionSequenceData corr T_X T_Y stage) [IsTriangulated X] [IsTriangulated Y] : X ≌ Y

The generation-certified sequence promotes the residual equivalence to an ambient equivalence.

Equations

• A.ambientEquivalence = A.sequence.ambientEquivalence ⋯ ⋯

noncomputable def CategoryTheory.Triangulated.FourierMukai.GeneratedExtensionSequenceData.toKernelEquivalence {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] {T_X : ObjectProperty X} {T_Y : ObjectProperty Y} {corr : Correspondence X Y W} {stage : KernelExtensionStage T_X.rightOrthogonal T_Y.rightOrthogonal corr} (A : GeneratedExtensionSequenceData corr T_X T_Y stage) [IsTriangulated X] [IsTriangulated Y] : KernelEquivalence corr

The promoted ambient equivalence is presented by the final extended Fourier--Mukai kernel.

Equations

• A.toKernelEquivalence = A.sequence.toKernelEquivalence ⋯ ⋯

structure CategoryTheory.Triangulated.FourierMukai.GeneratedBlockExtensionSequenceData {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) (R : ResidualKernelEquivalence B_X B_Y corr) : Type (max (max (max (max (max u u') u'') v) v') v'')

The generation-certified finite extension specialized to orthogonal exceptional blocks.

Coverage is now expressed concretely: every member of every block occurs in the corresponding extension list. The inequality saying that the list spans the total exceptional part is derived from the universal property of the block spans.

• sourceHead : X

  First source exceptional object.

• sourceTail : List X

  Remaining source exceptional objects.

• targetHead : Y

  First target exceptional object.

• targetTail : List Y

  Remaining target exceptional objects.

• sequence : ExtensionSequenceData corr R.toStage (self.sourceHead :: self.sourceTail) (self.targetHead :: self.targetTail)

  The dependent sequence of one-object kernel extensions.

• sourceMember (i : I) (j : Fin (B_X.length i)) : (B_X.collection i).obj j ∈ self.sourceHead :: self.sourceTail

  Every source block member occurs in the extension order.

• targetMember (i : J) (j : Fin (B_Y.length i)) : (B_Y.collection i).obj j ∈ self.targetHead :: self.targetTail

  Every target block member occurs in the extension order.

• sourceRightAdmissible : B_X.total.IsRightAdmissible

  The total source exceptional part is right admissible.

• targetRightAdmissible : B_Y.total.IsRightAdmissible

  The total target exceptional part is right admissible.

theorem CategoryTheory.Triangulated.FourierMukai.GeneratedBlockExtensionSequenceData.sourceCover {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} {R : ResidualKernelEquivalence B_X B_Y corr} (A : GeneratedBlockExtensionSequenceData B_X B_Y corr R) [IsTriangulated X] : B_X.total ≤ adjoinList B_X.residual (A.sourceHead :: A.sourceTail)

The source extension list contains the total source exceptional part.

theorem CategoryTheory.Triangulated.FourierMukai.GeneratedBlockExtensionSequenceData.targetCover {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} {R : ResidualKernelEquivalence B_X B_Y corr} (A : GeneratedBlockExtensionSequenceData B_X B_Y corr R) [IsTriangulated Y] : B_Y.total ≤ adjoinList B_Y.residual (A.targetHead :: A.targetTail)

The target extension list contains the total target exceptional part.

def CategoryTheory.Triangulated.FourierMukai.GeneratedBlockExtensionSequenceData.toGeneratedExtensionSequenceData {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} {R : ResidualKernelEquivalence B_X B_Y corr} (A : GeneratedBlockExtensionSequenceData B_X B_Y corr R) [IsTriangulated X] [IsTriangulated Y] : GeneratedExtensionSequenceData corr B_X.total B_Y.total R.toStage

Forget the block enumeration after deriving its exceptional-part coverage.

Equations

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.GeneratedBlockExtensionSequenceData.toKernelEquivalence {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} {R : ResidualKernelEquivalence B_X B_Y corr} (A : GeneratedBlockExtensionSequenceData B_X B_Y corr R) [IsTriangulated X] [IsTriangulated Y] : KernelEquivalence corr

The block-enumerated sequence produces an ambient Fourier--Mukai equivalence.

Equations

• A.toKernelEquivalence = A.toGeneratedExtensionSequenceData.toKernelEquivalence