Kernel realizations of natural transformations

Two kernels may present functors through supplied endpoint isomorphisms. A KernelTransformationData says that a named natural transformation between those functors is induced by an ordinary kernel morphism. Its enhanced form retains a closed representative and chosen dg cone.

The enhancement-independent and enhanced records are deliberately generic: they know nothing about adjunctions, convolution, twists, or cotwists. The enhanced record produces KernelConeNormalizationData, so exactness in the kernel variable yields the corresponding literal, source-natural, pointwise-distinguished triangle without repeating endpoint transport.

Fullness of the kernel transform is only an explicit sufficient hypothesis for constructing an ordinary realization. Selected cocycles and cones are noncanonical; only the ordinary-to-enhanced-to-ordinary round trip is proved.

structure CategoryTheory.Triangulated.FourierMukai.KernelTransformationData {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] (E : Correspondence X Y W) (K L : W) (F G : Functor X Y) (sourceIso : E.transform K ≅ F) (targetIso : E.transform L ≅ G) (α : F ⟶ G) : Type vW

An ordinary kernel morphism realizing a named natural transformation between two functors presented by kernel transforms.

• arrow : K ⟶ L

  The realizing kernel morphism.

• transform_arrow : E.transformMap self.arrow = CategoryStruct.comp sourceIso.hom (CategoryStruct.comp α targetIso.inv)

  Its transform is the named transformation after changing both endpoint presentations.

structure CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] (E : Correspondence X Y W) (e : Enhancement W) (K L : W) (F G : Functor X Y) (sourceIso : E.transform K ≅ F) (targetIso : E.transform L ≅ G) (α : F ⟶ G) : Type (max uE vE)

An enhanced representative and chosen dg cone of a kernel morphism realizing a named natural transformation.

• arrow : ↥(cocycles (H0.of e.dgCat (e.equiv.inverse.obj K)) (H0.of e.dgCat (e.equiv.inverse.obj L)))

  A closed representative between the enhancement's chosen endpoint lifts.

• cone : e.dgCat

  A chosen dg cone of arrow.

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

  The cone representability witness.

• transform_arrow : E.transformMap (CategoryStruct.comp (e.equiv.counitIso.app K).inv (CategoryStruct.comp (e.equiv.functor.map (H0.homMk self.arrow)) (e.equiv.counitIso.app L).hom)) = CategoryStruct.comp sourceIso.hom (CategoryStruct.comp α targetIso.inv)

  After returning the representative to the ordinary kernel category, its transform is the named transformation in the supplied presentations.

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationData.ext {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} {S T : KernelTransformationData E K L F G sourceIso targetIso α} (h : S.arrow = T.arrow) : S = T

Ordinary realization data are determined by their kernel arrow.

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationData.ext_iff {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} {S T : KernelTransformationData E K L F G sourceIso targetIso α} : S = T ↔ S.arrow = T.arrow

noncomputable def CategoryTheory.Triangulated.FourierMukai.KernelTransformationData.ofFull {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} [E.kernelTransform.Full] : KernelTransformationData E K L F G sourceIso targetIso α

Fullness of the kernel transform is sufficient to realize any named natural transformation with supplied endpoint presentations.

Equations

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

noncomputable def CategoryTheory.Triangulated.FourierMukai.KernelTransformationData.toConeData {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationData E K L F G sourceIso targetIso α) (e : Enhancement W) : KernelTransformationConeData E e K L F G sourceIso targetIso α

Choose a closed representative and dg cone for an ordinary kernel realization. Both choices are noncanonical.

Equations

• S.toConeData e = { arrow := (e.conePresentation S.arrow).arrow, cone := (e.conePresentation S.arrow).cone, isCone := (e.conePresentation S.arrow).isCone, transform_arrow := ⋯ }

def CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.toKernelTransformationData {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : KernelTransformationData E K L F G sourceIso targetIso α

Forget the enhanced choices while retaining the ordinary kernel arrow they represent.

Equations

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

def CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.presentation {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : DGCategory.ConePresentation e.dgCat

The selected arrow and cone as a reusable dg cone presentation.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.presentation_source {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : S.presentation.source = H0.of e.dgCat (e.equiv.inverse.obj K)

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.presentation_target {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : S.presentation.target = H0.of e.dgCat (e.equiv.inverse.obj L)

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.presentation_arrow {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : S.presentation.arrow = S.arrow

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.presentation_cone {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : S.presentation.cone = S.cone

def CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.sourceTransformIso {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : E.transform (e.equiv.functor.obj (H0.of e.dgCat (e.equiv.inverse.obj K))) ≅ F

Compare the transformed enhanced source lift with the literal source functor.

Equations

• S.sourceTransformIso = E.transformMapIso (e.equiv.counitIso.app K) ≪≫ sourceIso

def CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.targetTransformIso {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : E.transform (e.equiv.functor.obj (H0.of e.dgCat (e.equiv.inverse.obj L))) ≅ G

Compare the transformed enhanced target lift with the literal target functor.

Equations

• S.targetTransformIso = E.transformMapIso (e.equiv.counitIso.app L) ≪≫ targetIso

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.sourceTransformIso_hom {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : S.sourceTransformIso.hom = CategoryStruct.comp (E.transformMap (e.equiv.counitIso.app K).hom) sourceIso.hom

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.targetTransformIso_hom {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : S.targetTransformIso.hom = CategoryStruct.comp (E.transformMap (e.equiv.counitIso.app L).hom) targetIso.hom

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.transform_arrow_square {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : CategoryStruct.comp (E.transformMap (e.equiv.functor.map (H0.homMk S.arrow))) S.targetTransformIso.hom = CategoryStruct.comp S.sourceTransformIso.hom α

The stored transform equation rewritten as the literal endpoint square.

def CategoryTheory.Triangulated.FourierMukai.KernelTransformationConeData.normalizationData {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {e : Enhancement W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationConeData E e K L F G sourceIso targetIso α) : E.KernelConeNormalizationData e S.presentation F G α

The endpoint square packaged for generic cone normalization.

Equations

• S.normalizationData = { sourceIso := S.sourceTransformIso, targetIso := S.targetTransformIso, square := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelTransformationData.toConeData_toKernelTransformationData {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {E : Correspondence X Y W} {K L : W} {F G : Functor X Y} {sourceIso : E.transform K ≅ F} {targetIso : E.transform L ≅ G} {α : F ⟶ G} (S : KernelTransformationData E K L F G sourceIso targetIso α) (e : Enhancement W) : (S.toConeData e).toKernelTransformationData = S

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