Kernel realizations of left-adjunction dual twists

Let Φ_Q ⊣ Φ_P, where Φ_P : X ⥤ Y is presented by a kernel for a correspondence C and Φ_Q : Y ⥤ X is its supplied kernel-presented left adjoint. The adjunction unit has the form

id_Y ⟶ Φ_Q ⋙ Φ_P.

For the original functor Φ_P, the inverse rotation of the unit-cone triangle is conventionally called the dual twist triangle

dualTwist ⟶ id_Y ⟶ Φ_Q ⋙ Φ_P ⟶ dualTwist⟦1⟧.

The implementation introduces no second cone or normalization mechanism. LeftAdjointKernelData.toRightAdjointKernelData reads the same adjunction as a right adjunction for Φ_Q, and all constructions below delegate to the right-adjunction unit/cotwist interface with the two correspondences swapped. The public names here retain the dual-twist convention of the original functor.

The ordinary unit-kernel arrow, its enhanced representative, and its cone are still supplied or selected noncanonically. Nothing here makes the dual twist exact, invertible, canonical, or spherical, and no dual-cotwist construction is bundled into this lane.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.DualTwistKernelData {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] (C : Correspondence X Y W₁) (C' : Correspondence Y X W₂) (E : Correspondence Y Y W) (P : W₁) (L : LeftAdjointKernelData C C' P) (D : ConvolutionData C' C E) (U : UnitKernelData E) : Type vW

An ordinary kernel arrow realizing the unit of a kernel-presented left adjunction, named as the dual-twist input for the original functor.

Equations

• CategoryTheory.Triangulated.FourierMukai.DualTwistKernelData C C' E P L D U = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelData C' C E L.adjKernel L.toRightAdjointKernelData D U

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] (C : Correspondence X Y W₁) (C' : Correspondence Y X W₂) (E : Correspondence Y Y W) (e : Enhancement W) (P : W₁) (L : LeftAdjointKernelData C C' P) (D : ConvolutionData C' C E) (U : UnitKernelData E) : Type (max uE vE)

An enhanced representative and chosen cone for a left-adjunction unit kernel arrow, named as the dual-twist input for the original functor.

Equations

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

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelData.transform_arrow {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelData C C' E P L D U) : E.transformMap S.arrow = CategoryStruct.comp U.unitIso.inv (CategoryStruct.comp L.adj.unit (D.compIso L.adjKernel P).hom)

The specialized transform equation for the left-adjunction unit.

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualTwistKernelData.ofFull {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} [E.kernelTransform.Full] : DualTwistKernelData C C' E P L D U

Fullness of the kernel transform is sufficient to realize the left-adjunction unit by an ordinary kernel morphism.

Equations

• CategoryTheory.Triangulated.FourierMukai.DualTwistKernelData.ofFull = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelData.ofFull

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualTwistKernelData.toConeData {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelData C C' E P L D U) (e : Enhancement W) : DualTwistKernelConeData C C' E e P L D U

Choose a closed representative and dg cone for the dual-twist unit-kernel arrow. Both choices are noncanonical.

Equations

• S.toConeData e = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelData.toConeData S e

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistCone {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) : Functor Y Y

The unshifted cone of the left-adjunction unit.

Equations

• S.dualTwistCone = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistCone S

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwist {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [HasShift Y ℤ] : Functor Y Y

The choice-dependent ordinary dual twist: the pointwise [-1] shift of the selected left-unit cone transform.

Equations

• S.dualTwist = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwist S

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistKernel {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) : W

The shifted enhanced cone kernel presenting the dual twist.

Equations

• S.dualTwistKernel = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistKernel S

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistKernelIso {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [HasShift Y ℤ] [HasShift W ℤ] [e.equiv.functor.CommShift ℤ] (hShift : E.kernelTransform.CommShift ℤ) : E.transform S.dualTwistKernel ≅ S.dualTwist

The transform of dualTwistKernel is the dual twist.

Equations

• S.dualTwistKernelIso hShift = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistKernelIso S hShift

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.isKernelFunctor_dualTwist {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [HasShift Y ℤ] [HasShift W ℤ] [e.equiv.functor.CommShift ℤ] (hShift : E.kernelTransform.CommShift ℤ) : E.IsKernelFunctor S.dualTwist

The dual twist is a kernel functor for the endocorrespondence on Y. This does not assert exactness or invertibility.

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.transform_arrow_unit_square {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) : CategoryStruct.comp (E.transformMap (e.equiv.functor.map (H0.homMk S.arrow))) (KernelTransformationConeData.targetTransformIso S).hom = CategoryStruct.comp (KernelTransformationConeData.sourceTransformIso S).hom L.adj.unit

The transformed enhanced arrow forms the literal left-adjunction-unit square.

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.compositeToDualTwistCone {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : (C'.transform L.adjKernel).comp (C.transform P) ⟶ S.dualTwistCone

The transported second map from Φ_Q ⋙ Φ_P to the unshifted dual-twist cone.

Equations

• S.compositeToDualTwistCone hE = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.compositeToCotwistCone S hE

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistConeToShiftedIdentity {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : S.dualTwistCone ⟶ (Functor.id Y).comp (shiftFunctor Y 1)

The transported connecting map from the unshifted dual-twist cone to the shifted identity.

Equations

• S.dualTwistConeToShiftedIdentity hE = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistConeToShiftedIdentity S hE

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.unitTriangleInTarget {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : Functor Y (Pretriangulated.Triangle Y)

The source-natural unshifted left-unit triangle on the target Y of the original functor Φ_P.

Equations

• S.unitTriangleInTarget hE = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.unitTriangleInSource S hE

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.unitTriangleInTarget_obj₁ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.unitTriangleInTarget hE).obj A).obj₁ = A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.unitTriangleInTarget_obj₂ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.unitTriangleInTarget hE).obj A).obj₂ = ((C'.transform L.adjKernel).comp (C.transform P)).obj A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.unitTriangleInTarget_obj₃ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.unitTriangleInTarget hE).obj A).obj₃ = S.dualTwistCone.obj A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.unitTriangleInTarget_mor₁ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.unitTriangleInTarget hE).obj A).mor₁ = L.adj.unit.app A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.unitTriangleInTarget_mor₂ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.unitTriangleInTarget hE).obj A).mor₂ = (S.compositeToDualTwistCone hE).app A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.unitTriangleInTarget_mor₃ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.unitTriangleInTarget hE).obj A).mor₃ = (S.dualTwistConeToShiftedIdentity hE).app A

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.unitTriangleInTarget_obj_distinguished {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) [e.equiv.functor.IsTriangulated] (A : Y) : (S.unitTriangleInTarget hE).obj A ∈ Pretriangulated.distinguishedTriangles

Every value of the left-adjunction unit triangle is distinguished.

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.distinguishedUnitTriangleInTarget {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) [e.equiv.functor.IsTriangulated] : Functor Y Correspondence.KernelEvaluationExact.pointwiseDistinguishedTriangleProperty.FullSubcategory

The left-unit triangle family valued in distinguished triangles.

Equations

• S.distinguishedUnitTriangleInTarget hE = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.distinguishedUnitTriangleInSource S hE

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.distinguishedUnitTriangleInTarget_obj_val {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) [e.equiv.functor.IsTriangulated] (A : Y) : ((S.distinguishedUnitTriangleInTarget hE).obj A).obj = (S.unitTriangleInTarget hE).obj A

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : Functor Y (Pretriangulated.Triangle Y)

The conventional dual-twist triangle, obtained by inverse rotation of the left-adjunction unit triangle.

Equations

• S.dualTwistTriangleInTarget hE = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource S hE

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget_comp_π₁ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : (S.dualTwistTriangleInTarget hE).comp Pretriangulated.Triangle.π₁ = S.dualTwist

The first projection of the dual-twist triangle is strictly the dual twist.

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget_comp_π₂ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : (S.dualTwistTriangleInTarget hE).comp Pretriangulated.Triangle.π₂ = Functor.id Y

The second projection is strictly the identity.

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget_comp_π₃ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : (S.dualTwistTriangleInTarget hE).comp Pretriangulated.Triangle.π₃ = (C'.transform L.adjKernel).comp (C.transform P)

The third projection is strictly the left-adjoint composite.

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget_obj₁ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.dualTwistTriangleInTarget hE).obj A).obj₁ = S.dualTwist.obj A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget_obj₂ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.dualTwistTriangleInTarget hE).obj A).obj₂ = A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget_obj₃ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.dualTwistTriangleInTarget hE).obj A).obj₃ = ((C'.transform L.adjKernel).comp (C.transform P)).obj A

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget_unit {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : (S.dualTwistTriangleInTarget hE).whiskerLeft Pretriangulated.Triangle.π₂Toπ₃ = L.adj.unit

At the natural-transformation level, the second map is strictly the left-adjunction unit.

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget_mor₂ {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : Y) : ((S.dualTwistTriangleInTarget hE).obj A).mor₂ = L.adj.unit.app A

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.dualTwistTriangleInTarget_obj_distinguished {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) [e.equiv.functor.IsTriangulated] (A : Y) : (S.dualTwistTriangleInTarget hE).obj A ∈ Pretriangulated.distinguishedTriangles

Every value of the dual-twist triangle is distinguished.

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.distinguishedDualTwistTriangleInTarget {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) [e.equiv.functor.IsTriangulated] : Functor Y Correspondence.KernelEvaluationExact.pointwiseDistinguishedTriangleProperty.FullSubcategory

The dual-twist triangle family valued in distinguished triangles.

Equations

• S.distinguishedDualTwistTriangleInTarget hE = CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.distinguishedCotwistTriangleInSource S hE

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualTwistKernelConeData.distinguishedDualTwistTriangleInTarget_obj_val {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {C : Correspondence X Y W₁} {C' : Correspondence Y X W₂} {E : Correspondence Y Y W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : DualTwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) [e.equiv.functor.IsTriangulated] (A : Y) : ((S.distinguishedDualTwistTriangleInTarget hE).obj A).obj = (S.dualTwistTriangleInTarget hE).obj A