Comparing presented dg and Fourier--Mukai dual twists #
Let L ⊣ S be a strict dg adjunction whose H⁰ presentation identifies
S with a Fourier--Mukai transform and L with a kernel-presented left
adjoint. The dg unit cone and an independently chosen enhanced kernel cone
then produce two presentations of the dual twist of S.
This file is the semantic left-adjunction facade for the existing cotwist
comparison. It swaps the two endpoint categories and correspondences, then
reuses AdjunctionUnitKernelConeData through the definitional conversion
LeftAdjointKernelData.toRightAdjointKernelData. In particular, it does not
introduce a second comparison record or a second shift package. The
conventional dual twist is the pointwise [-1] shift of the unit cone, exactly
as in DualTwistKernelConeData.
The objectwise comparisons remain noncanonical. Natural comparison data,
equivalence of H⁰ of the unshifted dg unit cone, and shift compatibility are
all explicit inputs. Nothing here constructs those inputs, identifies an
inverse kernel, upgrades the dg functor to a quasi-equivalence, or asserts
sphericality.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.presentedLeftUnitTriangleObjIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eB.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : Y)
:
At each target object, the presented dg left-unit triangle is noncanonically isomorphic to the selected Fourier--Mukai left-unit triangle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.transportedDualTwistConeObjIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eB.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : Y)
:
The resulting noncanonical objectwise comparison of the unshifted dg and Fourier--Mukai left-unit cones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.presentedDualTwistTriangleObjIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eB.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : Y)
:
Inverse rotation gives the noncanonical objectwise comparison of the conventional dual-twist triangles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.transportedDualTwistObjIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eB.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : Y)
:
The resulting objectwise comparison from the conventional transported dg dual twist to the Fourier--Mukai dual twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.transportedDGDualTwistObjIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eB.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : Y)
:
The actual shifted dg unit cone is noncanonically objectwise isomorphic to the selected Fourier--Mukai dual twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Supplied natural comparison data #
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
:
Type (max uY vY)
Natural comparison data for the presented dg and Fourier--Mukai dual twists. This is the existing unit/cotwist comparison after swapping the two endpoints; no parallel record is introduced.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.ofConeIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(iso : K.transportedUnitCone eB ≅ T.dualTwistCone)
(second : CategoryStruct.comp (H.compositeToTransportedUnitCone K) iso.hom = T.compositeToDualTwistCone hE)
(third : H.transportedUnitConeToShiftedIdentity K = CategoryStruct.comp iso.hom (T.dualTwistConeToShiftedIdentity hE))
:
PresentedDualTwistComparisonData adj H K T hE
Supply a natural comparison of the unshifted left-unit cones and the two triangle-map squares not fixed by the common unit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.presentedLeftUnitTriangleIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
:
The supplied data give a natural comparison of the two left-unit triangle families.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.transportedDualTwistConeIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
:
The supplied natural isomorphism of the unshifted left-unit cones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.presentedDualTwistTriangleIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
:
Inverse rotation gives a natural comparison of the conventional dual-twist triangle families.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.transportedDualTwistIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
:
The induced natural isomorphism from the conventional transported dg dual twist to the selected Fourier--Mukai dual twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.transportedDGDualTwistIso
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
:
The transport of the actual shifted dg unit cone is naturally isomorphic to the selected Fourier--Mukai dual twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.transportedDualTwist_isKernelFunctor
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
:
E.IsKernelFunctor (K.transportedCotwist eB)
The conventional transported dg dual twist is a kernel functor through the supplied natural comparison.
theorem
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.transportedDGDualTwist_isKernelFunctor
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
:
E.IsKernelFunctor (K.transportedDGCotwist eB)
The actual shifted dg unit cone is a kernel functor through the composite natural comparison.
theorem
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.dualTwist_isEquivalence
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
(hK : (DGAdjunction.UnitConeData.unitCone adj K).h0.IsEquivalence)
:
An explicit equivalence hypothesis on H⁰ of the unshifted dg unit cone
transfers to the selected Fourier--Mukai dual twist.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.dualTwistKernelAutoequivalence
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
(hK : (DGAdjunction.UnitConeData.unitCone adj K).h0.IsEquivalence)
:
The selected shifted dual-twist kernel, packaged as a kernel
autoequivalence under the explicit H⁰ equivalence hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Compatibility with selected shift structures #
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.ShiftCompatibility
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
:
Type (max uY vY)
Shift compatibility for the dg/Fourier--Mukai dual-twist comparison. This is a semantic alias of the existing cotwist package, not a second structure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implicit_reducible]
noncomputable def
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.ShiftCompatibility.instCommShiftTransportedCotwistInt
{A : Type uA}
{B : Type uB}
{Y : Type uY}
[DGCategory A]
[DGCategory B]
[Category.{vY, uY} Y]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eB : H0 B ≌ Y}
[IsPretriangulated B]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[eB.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(K : adj.UnitConeData)
:
(K.transportedCotwist eB).CommShift ℤ
The sign-correct pointwise [-1] source shift used by the dual twist.
Equations
Instances For
def
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.ShiftCompatibility.ofCommShift
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
(dualTwistCommShift : T.dualTwist.CommShift ℤ)
(transportedDualTwistIso_commShift : NatTrans.CommShift (transportedDualTwistIso adj H K T hE N).hom ℤ)
:
FunctorIsoShiftCompatibility (K.transportedCotwist eB) T.dualTwist (transportedDualTwistIso adj H K T hE N)
Supply the selected Fourier--Mukai dual-twist shift structure and compatibility of the conventional comparison. The result is the existing cotwist compatibility record viewed through the semantic facade.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.ShiftCompatibility.dualTwistCommShift
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
(h : ShiftCompatibility adj H K T hE N)
:
The selected shift structure on the Fourier--Mukai dual twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.ShiftCompatibility.transportedDualTwistIso_commShift
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
(h : ShiftCompatibility adj H K T hE N)
:
NatTrans.CommShift (transportedDualTwistIso adj H K T hE N).hom ℤ
The conventional dual-twist comparison respects the canonical source shift package and the selected Fourier--Mukai shift package.
theorem
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.ShiftCompatibility.transportedDGDualTwistIso_commShift
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
(h : ShiftCompatibility adj H K T hE N)
[eB.functor.Additive]
:
NatTrans.CommShift (transportedDGDualTwistIso adj H K T hE N).hom ℤ
The comparison from the actual shifted dg unit cone respects the canonical source shift package and the selected Fourier--Mukai shift package.
theorem
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.ShiftCompatibility.dualTwistIsTriangulated
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
(h : ShiftCompatibility adj H K T hE N)
[eB.functor.IsTriangulated]
:
The selected Fourier--Mukai dual twist is triangulated when the comparison respects shifts and the endpoint presentation equivalence is triangulated.
theorem
CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.PresentedDualTwistComparisonData.ShiftCompatibility.dualTwistKernelAutoequivalenceIsTriangulated
{A : Type uA}
{B : Type uB}
{X : Type uX}
{Y : Type uY}
{W₁ : Type u₁}
{W₂ : Type u₂}
{W : Type uW}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
[Category.{vY, uY} Y]
[Category.{v₁, u₁} W₁]
[Category.{v₂, u₂} W₂]
[Category.{vW, uW} W]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : UnitKernelData E}
[IsPretriangulated B]
[Limits.HasZeroObject Y]
[HasShift Y ℤ]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[eB.functor.CommShift ℤ]
[Limits.HasZeroObject W]
[HasShift W ℤ]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
[e.equiv.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(H : DGAdjunction.H0Presentation eB eA (C'.transform Q) (C.transform P))
(K : adj.UnitConeData)
(T : DualTwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualTwistComparisonData adj H K T hE)
(h : ShiftCompatibility adj H K T hE N)
[eB.functor.IsTriangulated]
(hK : (DGAdjunction.UnitConeData.unitCone adj K).h0.IsEquivalence)
:
(dualTwistKernelAutoequivalence adj H K T hE N hK).equiv.IsTriangulated
The selected dual-twist kernel autoequivalence is exact relative to the selected target shift package.