Kernel realizations of adjunction counits

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

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

Here conv Q P is the kernel of Φ_Q ⋙ Φ_P (ConvolutionData.compIso reads composition diagrammatically, so this is Huybrechts' P ∘ Q).

The missing geometric statement is that this natural transformation is induced by an actual kernel morphism conv Q P ⟶ O_Δ. CounitKernelData records that ordinary kernel arrow and the equality identifying its transform with the counit. Any enhancement of the kernel category then supplies a noncanonical closed representative and a noncanonical dg cone, packaged by CounitKernelData.toConeData. Exactness in the kernel variable sends that dg cone to a source-natural family of pointwise distinguished triangles. CounitKernelConeData.counitTriangleInSource transports their first two vertices to the composite adjoint transform and the identity functor, with first map literally the adjunction counit and third vertex the Fourier--Mukai twist candidate. The selected cone kernel is named twistKernel and definitionally presents that twist, so the candidate is explicitly a kernel functor without any exactness or invertibility conclusion.

The constructor CounitKernelData.ofFull produces the ordinary arrow when the kernel transform is explicitly assumed full. No fullness theorem is asserted here: without that strong hypothesis, producing the kernel arrow remains the genuine Fourier--Mukai realization obligation involving convolution, the diagonal kernel, and the adjunction trace.

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

An ordinary kernel arrow realizing the counit of a kernel-presented adjunction, together with the exact comparison between its transform and the counit. It deliberately contains no enhancement or cone choice.

• arrow : D.conv R.adjKernel P ⟶ U.unitKernel

  The kernel morphism conv Q P ⟶ O_Δ.

• transform_arrow : E.transformMap self.arrow = CategoryStruct.comp (D.compIso R.adjKernel P).inv (CategoryStruct.comp R.adj.counit U.unitIso.hom)

  Transforming the kernel morphism gives the adjunction counit after the convolution and unit-kernel identifications.

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

A dg kernel arrow realizing the counit of a kernel-presented adjunction, together with a chosen cone of that arrow, for an enhancement e of the kernel category.

The arrow lives between the enhancement's lifts e.equiv.inverse.obj _ of the convolution kernel and the unit kernel. The equality transform_arrow includes all the changes of presentation: the comparison equivalence identifies the transform of the arrow with a map between the two kernels, convolution identifies the source transform with Φ_Q ⋙ Φ_P, and the unit-kernel isomorphism identifies the target transform with 𝟭 Y.

• arrow : ↥(cocycles (H0.of e.dgCat (e.equiv.inverse.obj (D.conv R.adjKernel P))) (H0.of e.dgCat (e.equiv.inverse.obj U.unitKernel)))

  The closed kernel morphism conv Q P ⟶ O_Δ, in the enhancement.

• cone : e.dgCat

  Its chosen dg cone.

• isCone : IsConeOf (↑self.arrow) self.cone

  The cone representability witness.

• transform_arrow : E.transformMap (CategoryStruct.comp (e.equiv.counitIso.app (D.conv R.adjKernel P)).inv (CategoryStruct.comp (e.equiv.functor.map (H0.homMk self.arrow)) (e.equiv.counitIso.app U.unitKernel).hom)) = CategoryStruct.comp (D.compIso R.adjKernel P).inv (CategoryStruct.comp R.adj.counit U.unitIso.hom)

  Transforming the kernel arrow gives the adjunction counit after the enhancement, convolution and unit-kernel identifications.

def CategoryTheory.Triangulated.FourierMukai.CounitKernelData.toKernelTransformationData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelData C C' E P R D U) : KernelTransformationData E (D.conv R.adjKernel P) U.unitKernel ((C'.transform R.adjKernel).comp (C.transform P)) (Functor.id Y) (D.compIso R.adjKernel P).symm U.unitIso.symm R.adj.counit

Read counit-kernel data through the generic kernel-transformation realization interface.

Equations

• S.toKernelTransformationData = { arrow := S.arrow, transform_arrow := ⋯ }

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelData.ext {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} {S T : CounitKernelData C C' E P R D U} (h : S.arrow = T.arrow) : S = T

Ordinary counit-kernel data are determined by their kernel arrow.

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelData.ext_iff {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} {S T : CounitKernelData C C' E P R D U} : S = T ↔ S.arrow = T.arrow

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

Fullness of the kernel transform is a sufficient abstract hypothesis for lifting the adjunction counit comparison to an ordinary kernel morphism.

Equations

• CategoryTheory.Triangulated.FourierMukai.CounitKernelData.ofFull = { arrow := CategoryTheory.Triangulated.FourierMukai.KernelTransformationData.ofFull.arrow, transform_arrow := ⋯ }

noncomputable def CategoryTheory.Triangulated.FourierMukai.CounitKernelData.liftedArrow {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelData C C' E P R D U) (e : Enhancement W) : ↥(cocycles (have this := e.equiv.inverse.obj (D.conv R.adjKernel P); this) (have this := e.equiv.inverse.obj U.unitKernel; this))

A noncanonical closed degree-zero representative of the ordinary kernel arrow in an enhancement.

Equations

• S.liftedArrow e = e.liftedCocycle S.arrow

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelData.homMk_liftedArrow {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelData C C' E P R D U) (e : Enhancement W) : H0.homMk (S.liftedArrow e) = e.equiv.inverse.map S.arrow

The selected cocycle represents the inverse image of the ordinary kernel arrow in H⁰ of the enhancement.

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelData.counit_conjugate_liftedArrow {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelData C C' E P R D U) (e : Enhancement W) : CategoryStruct.comp (e.equiv.counitIso.app (D.conv R.adjKernel P)).inv (CategoryStruct.comp (e.equiv.functor.map (H0.homMk (S.liftedArrow e))) (e.equiv.counitIso.app U.unitKernel).hom) = S.arrow

Conjugating the selected representative by the counit of the enhancement equivalence recovers the original kernel arrow.

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

Choose a closed representative and a dg cone for an ordinary counit kernel arrow. Both choices are noncanonical; the resulting comparison equation is the exact equation stored in S.

Equations

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

def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.toKernelTransformationConeData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : KernelTransformationConeData E e (D.conv R.adjKernel P) U.unitKernel ((C'.transform R.adjKernel).comp (C.transform P)) (Functor.id Y) (D.compIso R.adjKernel P).symm U.unitIso.symm R.adj.counit

Read enhanced counit-kernel data through the generic kernel-transformation realization interface.

Equations

• S.toKernelTransformationConeData = { arrow := S.arrow, cone := S.cone, isCone := S.isCone, transform_arrow := ⋯ }

def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.toCounitKernelData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : CounitKernelData C C' E P R D U

Forget the chosen cocycle and cone while retaining the ordinary kernel arrow represented through the enhancement equivalence.

Equations

• S.toCounitKernelData = { arrow := S.toKernelTransformationConeData.toKernelTransformationData.arrow, transform_arrow := ⋯ }

def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.presentation {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : DGCategory.ConePresentation e.dgCat

The kernel arrow and its cone as a reusable dg cone presentation.

Equations

• S.presentation = S.toKernelTransformationConeData.presentation

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.presentation_source {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : S.presentation.source = H0.of e.dgCat (e.equiv.inverse.obj (D.conv R.adjKernel P))

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.presentation_target {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : S.presentation.target = H0.of e.dgCat (e.equiv.inverse.obj U.unitKernel)

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.presentation_cone {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : S.presentation.cone = S.cone

@[reducible, inline]

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

The ordinary kernel represented by the selected enhanced counit cone.

Equations

• S.twistKernel = e.equiv.functor.obj (have this := S.cone; this)

@[reducible, inline]

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

The Fourier--Mukai transform of the counit-cone kernel, read in the kernel category through the enhancement. This is the kernel-presented twist candidate.

Equations

• S.twist = E.transform S.twistKernel

def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.twistKernelIso {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : E.transform S.twistKernel ≅ S.twist

The named twist kernel presents the twist definitionally.

Equations

• S.twistKernelIso = CategoryTheory.Iso.refl (E.transform S.twistKernel)

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.isKernelFunctor_twist {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : E.IsKernelFunctor S.twist

The twist candidate is a kernel functor, witnessed by its selected cone kernel. This asserts neither exactness nor invertibility.

def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.sourceTransformIso {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (_S : CounitKernelConeData C C' E e P R D U) : E.transform (e.equiv.functor.obj (H0.of e.dgCat (e.equiv.inverse.obj (D.conv R.adjKernel P)))) ≅ (C'.transform R.adjKernel).comp (C.transform P)

Identify the enhanced lift of the convolution kernel first with the ordinary convolution kernel and then with the composite transform presenting the source of the adjunction counit.

Equations

• _S.sourceTransformIso = _S.toKernelTransformationConeData.sourceTransformIso

def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.targetTransformIso {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (_S : CounitKernelConeData C C' E e P R D U) : E.transform (e.equiv.functor.obj (H0.of e.dgCat (e.equiv.inverse.obj U.unitKernel))) ≅ Functor.id Y

Identify the enhanced lift of the unit kernel with the identity transform, using the enhancement comparison and the supplied unit-kernel presentation.

Equations

• _S.targetTransformIso = _S.toKernelTransformationConeData.targetTransformIso

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.sourceTransformIso_hom {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : S.sourceTransformIso.hom = CategoryStruct.comp (E.transformMap (e.equiv.counitIso.app (D.conv R.adjKernel P)).hom) (D.compIso R.adjKernel P).inv

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.targetTransformIso_hom {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : S.targetTransformIso.hom = CategoryStruct.comp (E.transformMap (e.equiv.counitIso.app U.unitKernel).hom) U.unitIso.inv

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

The stored kernel-transform equation, normalized to the naturality square whose bottom edge is literally the adjunction counit.

def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.normalizationData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : E.KernelConeNormalizationData e S.presentation ((C'.transform R.adjKernel).comp (C.transform P)) (Functor.id Y) R.adj.counit

The generic endpoint-normalization package underlying the literal counit triangle.

Equations

• S.normalizationData = S.toKernelTransformationConeData.normalizationData

noncomputable def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSource {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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 counit-kernel cone as a source-natural family of transform triangles. The first two vertices are the transforms of the enhancement's lifts of the convolution and unit kernels; the third is S.twist.

Equations

• S.triangleInSource hE = S.normalizationData.rawTriangle hE

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.triangleInSource hE).obj A).obj₁ = (E.transform (e.equiv.functor.obj (e.equiv.inverse.obj (D.conv R.adjKernel P)))).obj A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.triangleInSource hE).obj A).obj₂ = (E.transform (e.equiv.functor.obj (e.equiv.inverse.obj U.unitKernel))).obj A

@[simp]

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

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

Every objectwise triangle obtained from the counit-kernel cone is distinguished.

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSource_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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.triangleInSource hE).whiskerLeft Pretriangulated.Triangle.π₁Toπ₂ = E.transformMap (e.equiv.functor.map (H0.homMk S.arrow))

The first map of the raw transform triangle before endpoint normalization.

noncomputable def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSourceObj₁Iso {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.triangleInSource hE).comp Pretriangulated.Triangle.π₁ ≅ (C'.transform R.adjKernel).comp (C.transform P)

The source endpoint comparison, typed against the first projection of the raw triangle functor.

Equations

• S.triangleInSourceObj₁Iso hE = S.normalizationData.rawTriangleObj₁Iso hE

noncomputable def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSourceObj₂Iso {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.triangleInSource hE).comp Pretriangulated.Triangle.π₂ ≅ Functor.id Y

The target endpoint comparison, typed against the second projection of the raw triangle functor.

Equations

• S.triangleInSourceObj₂Iso hE = S.normalizationData.rawTriangleObj₂Iso hE

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSource_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 Y Y W} {e : Enhancement W} {P : W₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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) : CategoryStruct.comp ((S.triangleInSource hE).whiskerLeft Pretriangulated.Triangle.π₁Toπ₂) (S.triangleInSourceObj₂Iso hE).hom = CategoryStruct.comp (S.triangleInSourceObj₁Iso hE).hom R.adj.counit

The first square for the comparison from the raw transform triangle to the literal counit triangle.

noncomputable def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.counitToTwist {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.id Y ⟶ S.twist

The transported second map from the identity functor to the twist candidate. It retains the supplied enhancement and cone choices.

Equations

• S.counitToTwist hE = S.normalizationData.normalizedSecond hE

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

The transported connecting map from the twist candidate to the shifted composite of the right adjoint and the original transform.

Equations

• S.twistToShiftedComposite hE = S.normalizationData.normalizedThird hE

noncomputable def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.counitTriangleInSource {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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 counit triangle R P ⋙ P ⟶ 𝟙 Y ⟶ twist ⟶ (R P ⋙ P)⟦1⟧.

Its first map and all three vertices are literal. Its remaining maps retain the choices in S; this is only an objectwise distinguished family, not a distinguished triangle in a functor category.

Equations

• S.counitTriangleInSource hE = S.normalizationData.normalizedTriangle hE

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSourceIsoCounit {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.triangleInSource hE ≅ S.counitTriangleInSource hE

The raw exact-family triangle and the literal counit triangle are naturally isomorphic through the two endpoint comparisons and the identity on the twist candidate.

Equations

• S.triangleInSourceIsoCounit hE = S.normalizationData.rawTriangleIsoNormalized hE

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSourceIsoCounit_hom_app_hom₁ {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.triangleInSourceIsoCounit hE).hom.app A).hom₁ = (S.triangleInSourceObj₁Iso hE).hom.app A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSourceIsoCounit_hom_app_hom₂ {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.triangleInSourceIsoCounit hE).hom.app A).hom₂ = (S.triangleInSourceObj₂Iso hE).hom.app A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.triangleInSourceIsoCounit_hom_app_hom₃ {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R 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.triangleInSourceIsoCounit hE).hom.app A).hom₃ = CategoryStruct.id ((S.triangleInSource hE).obj A).obj₃

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

Every value of the literal counit triangle is distinguished.

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

Equations

• S.distinguishedCounitTriangleInSource hE = S.normalizationData.distinguishedNormalizedTriangle hE

@[simp]

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

def CategoryTheory.Triangulated.FourierMukai.KernelTransformationData.toCounitKernelData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : KernelTransformationData E (D.conv R.adjKernel P) U.unitKernel ((C'.transform R.adjKernel).comp (C.transform P)) (Functor.id Y) (D.compIso R.adjKernel P).symm U.unitIso.symm R.adj.counit) : CounitKernelData C C' E P R D U

Specialize a generic kernel realization of the adjunction counit to the stable counit-kernel interface.

Equations

• S.toCounitKernelData = { arrow := S.arrow, transform_arrow := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationData.toCounitKernelData_toKernelTransformationData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : KernelTransformationData E (D.conv R.adjKernel P) U.unitKernel ((C'.transform R.adjKernel).comp (C.transform P)) (Functor.id Y) (D.compIso R.adjKernel P).symm U.unitIso.symm R.adj.counit) : S.toCounitKernelData.toKernelTransformationData = S

def CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.toCounitKernelConeData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : KernelTransformationConeData E e (D.conv R.adjKernel P) U.unitKernel ((C'.transform R.adjKernel).comp (C.transform P)) (Functor.id Y) (D.compIso R.adjKernel P).symm U.unitIso.symm R.adj.counit) : CounitKernelConeData C C' E e P R D U

Specialize a generic enhanced realization of the adjunction counit to the stable counit-kernel cone interface.

Equations

• S.toCounitKernelConeData = { arrow := S.arrow, cone := S.cone, isCone := S.isCone, transform_arrow := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.toCounitKernelConeData_toKernelTransformationConeData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : KernelTransformationConeData E e (D.conv R.adjKernel P) U.unitKernel ((C'.transform R.adjKernel).comp (C.transform P)) (Functor.id Y) (D.compIso R.adjKernel P).symm U.unitIso.symm R.adj.counit) : S.toCounitKernelConeData.toKernelTransformationConeData = S

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelData.toConeData_toCounitKernelData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelData C C' E P R D U) (e : Enhancement W) : (S.toConeData e).toCounitKernelData = S

Forgetting the choices made by toConeData recovers the original ordinary kernel datum. This does not identify the selected cocycle or cone.

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelData.toKernelTransformationData_toCounitKernelData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelData C C' E P R D U) : S.toKernelTransformationData.toCounitKernelData = S

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.toKernelTransformationConeData_toCounitKernelConeData {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₁} {R : RightAdjointKernelData C C' P} {D : ConvolutionData C' C E} {U : UnitKernelData E} (S : CounitKernelConeData C C' E e P R D U) : S.toKernelTransformationConeData.toCounitKernelConeData = S