Kernel realizations of left-adjunction dual cotwists

Let Φ_Q ⊣ Φ_P, where Φ_P : X ⥤ Y is a Fourier--Mukai transform and Φ_Q : Y ⥤ X is its supplied kernel-presented left adjoint. The adjunction counit is

Φ_P ⋙ Φ_Q ⟶ id_X.

Its cone is conventionally the dual cotwist of the original functor Φ_P. This file supplies the semantic left-adjunction API while reusing CounitKernelData and CounitKernelConeData with the correspondences swapped through LeftAdjointKernelData.toRightAdjointKernelData.

Thus an ordinary kernel arrow conv P Q ⟶ O_Δ, together with its exact transform equation, has a noncanonically selected enhanced representative and cone. Exact kernel evaluation produces the source-natural, pointwise distinguished family

Φ_P ⋙ Φ_Q ⟶ id_X ⟶ dualCotwist ⟶ (Φ_P ⋙ Φ_Q)⟦1⟧.

No new adjunction, cone, normalization, or rotation is constructed here. The dual cotwist remains choice-dependent; it is not asserted exact, invertible, canonical, or spherical.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelData {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 X X W) (P : W₁) (L : LeftAdjointKernelData C C' P) (D : ConvolutionData C C' E) (U : UnitKernelData E) : Type vW

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

Equations

• CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelData C C' E P L D U = CategoryTheory.Triangulated.FourierMukai.CounitKernelData C' C E L.adjKernel L.toRightAdjointKernelData D U

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData {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 X X 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 counit kernel arrow, named as the dual-cotwist input for the original functor.

Equations

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

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelData.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 X X W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelData C C' E P L D U) : E.transformMap S.arrow = CategoryStruct.comp (D.compIso P L.adjKernel).inv (CategoryStruct.comp L.adj.counit U.unitIso.hom)

The specialized transform equation for the left-adjunction counit.

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelData.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 X X W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} [E.kernelTransform.Full] : DualCotwistKernelData C C' E P L D U

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

Equations

• CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelData.ofFull = CategoryTheory.Triangulated.FourierMukai.CounitKernelData.ofFull

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelData.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 X X W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelData C C' E P L D U) (e : Enhancement W) : DualCotwistKernelConeData C C' E e P L D U

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

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistKernel {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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) : W

The selected enhanced counit cone read as an ordinary kernel.

Equations

• S.dualCotwistKernel = CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.twistKernel S

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwist {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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) : Functor X X

The transform of the selected cone kernel: the choice-dependent ordinary dual cotwist.

Equations

• S.dualCotwist = CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.twist S

def CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistKernelIso {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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) : E.transform S.dualCotwistKernel ≅ S.dualCotwist

The named dual-cotwist kernel presents the dual cotwist definitionally.

Equations

• S.dualCotwistKernelIso = CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.twistKernelIso S

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.isKernelFunctor_dualCotwist {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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) : E.IsKernelFunctor S.dualCotwist

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

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.transform_arrow_counit_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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) : CategoryStruct.comp (E.transformMap (e.equiv.functor.map (H0.homMk S.arrow))) (CounitKernelConeData.targetTransformIso S).hom = CategoryStruct.comp (CounitKernelConeData.sourceTransformIso S).hom L.adj.counit

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.counitToDualCotwist {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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : Functor.id X ⟶ S.dualCotwist

The transported second map from the identity to the dual cotwist.

Equations

• S.counitToDualCotwist hE = CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.counitToTwist S hE

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistToShiftedComposite {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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : S.dualCotwist ⟶ ((C.transform P).comp (C'.transform L.adjKernel)).comp (shiftFunctor X 1)

The transported connecting map from the dual cotwist to the shifted left-adjoint composite.

Equations

• S.dualCotwistToShiftedComposite hE = CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.twistToShiftedComposite S hE

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistTriangleInSource {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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : Functor X (Pretriangulated.Triangle X)

The source-natural dual-cotwist triangle for the original functor Φ_P : X ⥤ Y.

Equations

• S.dualCotwistTriangleInSource hE = CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.counitTriangleInSource S hE

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : X) : ((S.dualCotwistTriangleInSource hE).obj A).obj₁ = ((C.transform P).comp (C'.transform L.adjKernel)).obj A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : X) : ((S.dualCotwistTriangleInSource hE).obj A).obj₂ = A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : X) : ((S.dualCotwistTriangleInSource hE).obj A).obj₃ = S.dualCotwist.obj A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : X) : ((S.dualCotwistTriangleInSource hE).obj A).mor₁ = L.adj.counit.app A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : X) : ((S.dualCotwistTriangleInSource hE).obj A).mor₂ = (S.counitToDualCotwist hE).app A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) (A : X) : ((S.dualCotwistTriangleInSource hE).obj A).mor₃ = (S.dualCotwistToShiftedComposite hE).app A

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistTriangleInSource_counit {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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (hE : E.KernelEvaluationExact) : (S.dualCotwistTriangleInSource hE).whiskerLeft Pretriangulated.Triangle.π₁Toπ₂ = L.adj.counit

At the natural-transformation level, the first map is strictly the left-adjunction counit.

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.dualCotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [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 : X) : (S.dualCotwistTriangleInSource hE).obj A ∈ Pretriangulated.distinguishedTriangles

Every value of the dual-cotwist triangle is distinguished.

noncomputable def CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.distinguishedDualCotwistTriangleInSource {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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [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 X Correspondence.KernelEvaluationExact.pointwiseDistinguishedTriangleProperty.FullSubcategory

The dual-cotwist triangle family valued in distinguished triangles.

Equations

• S.distinguishedDualCotwistTriangleInSource hE = CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.distinguishedCounitTriangleInSource S hE

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.DualCotwistKernelConeData.distinguishedDualCotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {L : LeftAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : DualCotwistKernelConeData C C' E e P L D U) [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [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 : X) : ((S.distinguishedDualCotwistTriangleInSource hE).obj A).obj = (S.dualCotwistTriangleInSource hE).obj A