Comparing presented dg and Fourier--Mukai dual cotwists #
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 counit cone and an independently chosen enhanced kernel cone
then produce two presentations of the dual cotwist of S.
This file is the semantic left-adjunction facade for the existing twist
comparison. It swaps the two endpoint categories and correspondences, then
reuses CounitKernelConeData through the definitional conversion
LeftAdjointKernelData.toRightAdjointKernelData. It introduces neither a
second comparison record nor a second shift package. Unlike the conventional
dual twist, the dual cotwist is the unshifted counit cone.
The objectwise comparison remains noncanonical. Natural comparison data,
equivalence of H⁰ of the dg counit cone, and shift compatibility are 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.DualCotwistKernelConeData.presentedLeftCounitTriangleObjIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
At each source object, the presented dg left-counit triangle is noncanonically isomorphic to the selected Fourier--Mukai left-counit triangle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.transportedDualCotwistObjIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
The resulting noncanonical objectwise comparison from the transported dg counit cone to the selected Fourier--Mukai dual cotwist.
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.DualCotwistKernelConeData.PresentedDualCotwistComparisonData
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
:
Type (max uX vX)
Natural comparison data for the presented dg and Fourier--Mukai dual cotwists. This is the existing counit/twist 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.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.ofDualCotwistIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(iso : K.transportedTwist eA ≅ T.dualCotwist)
(second : CategoryStruct.comp (H.counitToTransportedTwist K) iso.hom = T.counitToDualCotwist hE)
(third : H.transportedTwistToShiftedComposite K = CategoryStruct.comp iso.hom (T.dualCotwistToShiftedComposite hE))
:
PresentedDualCotwistComparisonData adj H K T hE
Supply a natural dual-cotwist comparison and the two triangle-map squares not fixed by the common left-adjunction counit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.presentedLeftCounitTriangleIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
:
The supplied data give a natural comparison of the two left-counit triangle families.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.transportedDualCotwistIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
:
The induced natural isomorphism from the transported dg counit cone to the selected Fourier--Mukai dual cotwist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.transportedDualCotwist_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
:
E.IsKernelFunctor (K.transportedTwist eA)
The transported dg counit cone is a kernel functor through the supplied natural dual-cotwist comparison.
theorem
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.dualCotwist_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
(hK : (DGAdjunction.CounitConeData.twist adj K).h0.IsEquivalence)
:
An explicit equivalence hypothesis on H⁰ of the dg counit cone transfers
to the selected Fourier--Mukai dual cotwist.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.dualCotwistKernelAutoequivalence
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
(hK : (DGAdjunction.CounitConeData.twist adj K).h0.IsEquivalence)
:
The selected dual-cotwist 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.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
:
Type (max uX vX)
Shift compatibility for the dg/Fourier--Mukai dual-cotwist comparison. This is a semantic alias of the existing twist 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.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.ShiftCompatibility.instCommShiftTransportedTwistInt
{A : Type uA}
{B : Type uB}
{X : Type uX}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
{L : DGFunctor B A}
{S : DGFunctor A B}
{eA : H0 A ≌ X}
[IsPretriangulated A]
[HasShift X ℤ]
[eA.functor.CommShift ℤ]
(adj : DGAdjunction L S)
(K : adj.CounitConeData)
:
(K.transportedTwist eA).CommShift ℤ
The transported H⁰ twist shift structure used by the dual cotwist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
(dualCotwistCommShift : T.dualCotwist.CommShift ℤ)
(transportedDualCotwistIso_commShift : NatTrans.CommShift (transportedDualCotwistIso adj H K T hE N).hom ℤ)
:
FunctorIsoShiftCompatibility (K.transportedTwist eA) T.dualCotwist (transportedDualCotwistIso adj H K T hE N)
Supply the selected Fourier--Mukai dual-cotwist shift structure and compatibility of the dg comparison. The result is the existing twist 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.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.ShiftCompatibility.dualCotwistCommShift
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
(h : ShiftCompatibility adj H K T hE N)
:
The selected shift structure on the Fourier--Mukai dual cotwist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.ShiftCompatibility.transportedDualCotwistIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
(h : ShiftCompatibility adj H K T hE N)
:
NatTrans.CommShift (transportedDualCotwistIso adj H K T hE N).hom ℤ
The dual-cotwist comparison respects the canonical source shift package and the selected Fourier--Mukai shift package.
theorem
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.ShiftCompatibility.dualCotwistIsTriangulated
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
(h : ShiftCompatibility adj H K T hE N)
[eA.functor.IsTriangulated]
:
The selected Fourier--Mukai dual cotwist is triangulated when the comparison respects shifts and the endpoint presentation equivalence is triangulated.
theorem
CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.PresentedDualCotwistComparisonData.ShiftCompatibility.dualCotwistKernelAutoequivalenceIsTriangulated
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : UnitKernelData E}
[IsPretriangulated A]
[Limits.HasZeroObject X]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[Pretriangulated X]
[eA.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.CounitConeData)
(T : DualCotwistKernelConeData C C' E e P (LeftAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedDualCotwistComparisonData adj H K T hE)
(h : ShiftCompatibility adj H K T hE N)
[eA.functor.IsTriangulated]
(hK : (DGAdjunction.CounitConeData.twist adj K).h0.IsEquivalence)
:
(dualCotwistKernelAutoequivalence adj H K T hE N hK).equiv.IsTriangulated
The selected dual-cotwist kernel autoequivalence is exact relative to the selected target shift package.