Kernel realizations of adjunction units

Let Φ_P : X ⥤ Y have a kernel-presented right adjoint Φ_Q. With a convolution kernel and a diagonal unit kernel on X, the adjunction unit has the form

Φ_{O_Δ} ⟶ Φ_{conv P Q}.

Here conv P Q presents Φ_P ⋙ Φ_Q. The abbreviations AdjunctionUnitKernelData and AdjunctionUnitKernelConeData specialize the generic kernel-transformation interfaces to an ordinary kernel morphism O_Δ ⟶ conv P Q, its enhanced representative, and a chosen dg cone. They are abbreviations rather than parallel records, since there is no legacy unit realization API to preserve.

Exactness in the kernel variable gives a source-natural, pointwise distinguished unshifted unit triangle

𝟭 X ⟶ Φ_P ⋙ Φ_Q ⟶ cotwistCone ⟶ (𝟭 X)⟦1⟧.

The third functor is the unshifted cotwist-cone candidate. Its pointwise [-1] shift is the conventional, choice-dependent ordinary cotwist, and inverse rotation gives the source-natural triangle

cotwist ⟶ 𝟭 X ⟶ Φ_P ⋙ Φ_Q ⟶ cotwist⟦1⟧.

The shift and inverse rotation reuse the functor-category HasShift instance and Mathlib's invRotate; no signed map is reconstructed here. The existing shift comparison of a shift-coherent kernel family presents the cotwist by the cone kernel shifted inside the enhancement's homotopy category. No representative or cone is canonical, and no exactness, autoequivalence, or sphericality claim is made.

AdjunctionUnitKernelData.ofFull is only a sufficient abstract constructor. Without the explicit fullness hypothesis, producing the kernel arrow remains the geometric unit-realization obligation.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelData {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₁) (R : RightAdjointKernelData C C' P) (D : ConvolutionData C C' E) (U : UnitKernelData E) : Type vW

An ordinary kernel arrow realizing the unit of a kernel-presented right adjunction. This is a definitional specialization of the generic kernel-transformation interface.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData {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₁) (R : RightAdjointKernelData C C' P) (D : ConvolutionData C C' E) (U : UnitKernelData E) : Type (max uE vE)

An enhanced representative and chosen dg cone of a kernel arrow realizing the unit of a kernel-presented right adjunction.

Equations

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

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelData.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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelData C C' E P R D U) : E.transformMap S.arrow = CategoryStruct.comp U.unitIso.inv (CategoryStruct.comp R.adj.unit (D.compIso P R.adjKernel).hom)

The specialized kernel-transform equation for the adjunction unit.

noncomputable def CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelData.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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} [E.kernelTransform.Full] : AdjunctionUnitKernelData C C' E P R D U

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

Equations

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelData.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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelData C C' E P R D U) (e : Enhancement W) : AdjunctionUnitKernelConeData C C' E e P R D U

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

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistCone {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R D U) : Functor X X

The transform of the selected cone: the unshifted cotwist-cone candidate.

Equations

• S.cotwistCone = (CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.normalizationData S).coneTransform

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwist {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R D U) [HasShift X ℤ] : Functor X X

The conventional, choice-dependent ordinary cotwist: the pointwise [-1] shift of the selected cotwist-cone transform. This is a functor only; no exactness or equivalence is asserted.

Equations

• S.cotwist = (CategoryTheory.shiftFunctor (CategoryTheory.Functor X X) (-1)).obj S.cotwistCone

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistKernel {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R D U) : W

The selected kernel presenting the conventional cotwist: shift the enhanced unit cone by -1 before transporting it to the ordinary kernel category.

Equations

• S.cotwistKernel = (CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.normalizationData S).shiftedConeKernel (-1)

noncomputable def CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistKernelIso {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R D U) [HasShift X ℤ] [HasShift W ℤ] [e.equiv.functor.CommShift ℤ] (hShift : E.kernelTransform.CommShift ℤ) : E.transform S.cotwistKernel ≅ S.cotwist

The kernel family's shift comparison identifies the transform of cotwistKernel with the pointwise shifted cotwist-cone functor.

Equations

• S.cotwistKernelIso hShift = (CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.normalizationData S).shiftedConeTransformIso hShift (-1)

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.isKernelFunctor_cotwist {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R D U) [HasShift X ℤ] [HasShift W ℤ] [e.equiv.functor.CommShift ℤ] (hShift : E.kernelTransform.CommShift ℤ) : E.IsKernelFunctor S.cotwist

The conventional cotwist is a Fourier--Mukai kernel functor, presented by the explicitly named shifted cone kernel. This asserts neither exactness nor invertibility of the cotwist.

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

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.compositeToCotwistCone {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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) : (C.transform P).comp (C'.transform R.adjKernel) ⟶ S.cotwistCone

The transported second map from Φ_P ⋙ Φ_Q to the unshifted cotwist-cone candidate.

Equations

• S.compositeToCotwistCone hE = (CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.normalizationData S).normalizedSecond hE

noncomputable def CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistConeToShiftedIdentity {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistCone ⟶ (Functor.id X).comp (shiftFunctor X 1)

The transported connecting map from the unshifted cotwist-cone candidate to the shifted identity functor.

Equations

• S.cotwistConeToShiftedIdentity hE = (CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.normalizationData S).normalizedThird hE

noncomputable def CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.unitTriangleInSource {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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 unshifted unit triangle 𝟙 X ⟶ Φ_P ⋙ Φ_Q ⟶ cotwistCone ⟶ (𝟙 X)⟦1⟧.

Its first map and all three vertices are literal. It is only an objectwise distinguished family, not a distinguished triangle in a functor category.

Equations

• S.unitTriangleInSource hE = (CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.normalizationData S).normalizedTriangle hE

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.unitTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.unitTriangleInSource hE).obj A).obj₁ = A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.unitTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.unitTriangleInSource hE).obj A).obj₂ = ((C.transform P).comp (C'.transform R.adjKernel)).obj A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.unitTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.unitTriangleInSource hE).obj A).obj₃ = S.cotwistCone.obj A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.unitTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.unitTriangleInSource hE).obj A).mor₁ = R.adj.unit.app A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.unitTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.unitTriangleInSource hE).obj A).mor₂ = (S.compositeToCotwistCone hE).app A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.unitTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.unitTriangleInSource hE).obj A).mor₃ = (S.cotwistConeToShiftedIdentity hE).app A

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.unitTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.unitTriangleInSource hE).obj A ∈ Pretriangulated.distinguishedTriangles

Every value of the literal unshifted unit triangle is distinguished.

noncomputable def CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.distinguishedUnitTriangleInSource {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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 literal unshifted unit-triangle family with codomain restricted to distinguished triangles.

Equations

• S.distinguishedUnitTriangleInSource hE = (CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.normalizationData S).distinguishedNormalizedTriangle hE

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.distinguishedUnitTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.distinguishedUnitTriangleInSource hE).obj A).obj = (S.unitTriangleInSource hE).obj A

The conventional cotwist triangle

noncomputable def CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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 inverse rotation of the unshifted unit triangle: cotwist ⟶ 𝟭 X ⟶ Φ_P ⋙ Φ_Q ⟶ cotwist⟦1⟧.

Mathlib's inverse rotation owns the minus sign in the first map.

Equations

• S.cotwistTriangleInSource hE = (S.unitTriangleInSource hE).comp (CategoryTheory.Pretriangulated.invRotate X)

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistTriangleInSource hE).comp Pretriangulated.Triangle.π₁ = S.cotwist

The first projection of the rotated triangle is strictly the pointwise shifted cotwist-cone functor.

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistTriangleInSource hE).comp Pretriangulated.Triangle.π₂ = Functor.id X

The second projection of the rotated triangle is strictly the identity.

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistTriangleInSource hE).comp Pretriangulated.Triangle.π₃ = (C.transform P).comp (C'.transform R.adjKernel)

The third projection of the rotated triangle is strictly the composite adjoint transform.

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistTriangleInSource hE).obj A).obj₁ = S.cotwist.obj A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistTriangleInSource hE).obj A).obj₂ = A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistTriangleInSource hE).obj A).obj₃ = ((C.transform P).comp (C'.transform R.adjKernel)).obj A

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource_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 X X W} {e : Enhancement W} {P : W₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistTriangleInSource hE).whiskerLeft Pretriangulated.Triangle.π₂Toπ₃ = R.adj.unit

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistTriangleInSource hE).obj A).mor₂ = R.adj.unit.app A

Inverse rotation moves the adjunction unit into the second map.

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.cotwistTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.cotwistTriangleInSource hE).obj A ∈ Pretriangulated.distinguishedTriangles

Every value of the conventional cotwist triangle is distinguished.

noncomputable def CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.distinguishedCotwistTriangleInSource {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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 conventional cotwist-triangle family with codomain restricted to distinguished triangles.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.distinguishedCotwistTriangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C C' E} {U : UnitKernelData E} (S : AdjunctionUnitKernelConeData C C' E e P R 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.distinguishedCotwistTriangleInSource hE).obj A).obj = (S.cotwistTriangleInSource hE).obj A