Kernel functors between triangulated categories

A Fourier--Mukai transform is assembled from a correspondence. Geometrically, for the projections p : X × Y ⟶ X and q : X × Y ⟶ Y and a kernel P ∈ D(X × Y), the transform is

Φ_P(E) = Rq_*(Lp^* E ⊗^L P).

This file records the three functors of that composite and nothing else about them: a Correspondence supplies a source functor in the role of Lp^*, a bifunctor in the role of ⊗^L, and a target functor in the role of Rq_*. The transform with a chosen kernel is their composite, and IsKernelFunctor is the property of being isomorphic to such a composite.

Following StabilityCondition.Families.ExactPullback, exactness is an explicit hypothesis rather than a conclusion. The Correspondence structure asks for no triangulated structure at all; the section that concludes the transform is triangulated states the hypotheses on the three constituents.

What this file does not assert

The geometric content of Fourier--Mukai theory is exactly the part that is absent here. This file does not

• construct any of the three functors, or assume a scheme, a product, a derived category, or a derived functor anywhere;
• assume pull and push are adjoint, in either order, or supply a projection formula relating tensor to either of them;
• assume tensor is monoidal, symmetric, associative, or unital, or that it is exact in either variable;
• convolve two kernels or prove that a composite of two transforms is a transform;
• prove that a kernel is determined by its transform, or that any particular class of functors consists of kernel functors (Orlov's theorem);
• connect a kernel functor to a stability condition, a t-structure, or a Grothendieck group.

The last of those is deliberate placement rather than difficulty: the Grothendieck-group statements need Triangulated.K₀, which lives under StabilityCondition.Foundation, and importing it here would point a generic module at the stability track.

structure CategoryTheory.Triangulated.FourierMukai.Correspondence (𝒳 : Type u) (𝒴 : Type u') (𝒵 : Type u'') [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] : Type (max (max (max (max (max u u') u'') v) v') v'')

The functorial data a Fourier--Mukai transform is built from, with no kernel chosen and no compatibility between the three functors assumed.

𝒵 plays the role of the derived category of the product, pull the role of Lp^*, tensor the role of ⊗^L on the product, and push the role of Rq_*. A caller supplies all three; nothing here constructs them.

• pull : Functor 𝒳 𝒵

  The functor in the role of derived pullback along the first projection.

• tensor : Functor 𝒵 (Functor 𝒵 𝒵)

  The bifunctor in the role of the derived tensor product on the product category. tensor.obj K is the twist by the kernel K.

• push : Functor 𝒵 𝒴

  The functor in the role of derived pushforward along the second projection.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.Correspondence.transform {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (K : 𝒵) : Functor 𝒳 𝒴

The Fourier--Mukai transform of C with kernel K: pull back, twist by K, push forward. An abbrev so that instance search sees the composite and derives the shift and triangulation instances from those of the three constituents.

Equations

• C.transform K = C.pull.comp ((C.tensor.obj K).comp C.push)

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.transform_obj {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (K : 𝒵) (E : 𝒳) : (C.transform K).obj E = C.push.obj ((C.tensor.obj K).obj (C.pull.obj E))

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.transform_map {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (K : 𝒵) {E F : 𝒳} (f : E ⟶ F) : (C.transform K).map f = C.push.map ((C.tensor.obj K).map (C.pull.map f))

def CategoryTheory.Triangulated.FourierMukai.Correspondence.transformMap {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) {K L : 𝒵} (f : K ⟶ L) : C.transform K ⟶ C.transform L

A morphism of kernels induces a natural transformation of transforms. This is the categorical map needed before a cone of kernels can be transported; it uses only the functoriality already present in the abstract correspondence and makes no claim that a suitable kernel morphism or cone exists.

Equations

• C.transformMap f = C.pull.whiskerLeft (CategoryTheory.Functor.whiskerRight (C.tensor.map f) C.push)

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.transformMap_app {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) {K L : 𝒵} (f : K ⟶ L) (E : 𝒳) : (C.transformMap f).app E = C.push.map ((C.tensor.map f).app (C.pull.obj E))

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.transformMap_id {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (K : 𝒵) : C.transformMap (CategoryStruct.id K) = CategoryStruct.id (C.transform K)

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.transformMap_comp {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) {K L M : 𝒵} (f : K ⟶ L) (g : L ⟶ M) : C.transformMap (CategoryStruct.comp f g) = CategoryStruct.comp (C.transformMap f) (C.transformMap g)

def CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelTransform {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) : Functor 𝒵 (Functor 𝒳 𝒴)

The Fourier--Mukai transform as a functor of its kernel.

Packaging transform and transformMap into one functor is the canonical interface for constructions, such as dg cones, which vary the kernel. It also makes the identity and composition laws available through ordinary functoriality rather than requiring each consumer to restate them.

Equations

• C.kernelTransform = { obj := fun (K : 𝒵) => C.transform K, map := fun {X Y : 𝒵} (f : X ⟶ Y) => C.transformMap f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelTransform_obj {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (K : 𝒵) : C.kernelTransform.obj K = C.transform K

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelTransform_map {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) {K L : 𝒵} (f : K ⟶ L) : C.kernelTransform.map f = C.transformMap f

def CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelEvaluation {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (E : 𝒳) : Functor 𝒵 𝒴

Evaluate the kernel-variable transform functor on one source object. This is the exact functor whose preservation of a kernel triangle says that the corresponding transforms form a pointwise distinguished triangle.

Equations

• C.kernelEvaluation E = C.kernelTransform.comp ((CategoryTheory.evaluation 𝒳 𝒴).obj E)

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelEvaluation_obj {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (E : 𝒳) (K : 𝒵) : (C.kernelEvaluation E).obj K = (C.transform K).obj E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelEvaluation_map {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (E : 𝒳) {K L : 𝒵} (f : K ⟶ L) : (C.kernelEvaluation E).map f = (C.transformMap f).app E

def CategoryTheory.Triangulated.FourierMukai.Correspondence.transformMapIso {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) {K L : 𝒵} (e : K ≅ L) : C.transform K ≅ C.transform L

Isomorphic kernels give isomorphic transforms. This is the only comparison between two kernels that holds with no hypothesis on tensor; the converse is the hard direction and is not asserted anywhere in this file.

Equations

• C.transformMapIso e = C.pull.isoWhiskerLeft (CategoryTheory.Functor.isoWhiskerRight (C.tensor.mapIso e) C.push)

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.transformMapIso_hom {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) {K L : 𝒵} (e : K ≅ L) : (C.transformMapIso e).hom = C.transformMap e.hom

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.transformMapIso_inv {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) {K L : 𝒵} (e : K ≅ L) : (C.transformMapIso e).inv = C.transformMap e.inv

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.transformMapIso_refl {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (K : 𝒵) : C.transformMapIso (Iso.refl K) = Iso.refl (C.transform K)

def CategoryTheory.Triangulated.FourierMukai.Correspondence.IsKernelFunctor {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (Φ : Functor 𝒳 𝒴) : Prop

A functor is a kernel functor for C when it is isomorphic to the transform of some kernel. The kernel is existentially quantified and the witnessing isomorphism is only Nonempty: this is the property, not a choice of kernel.

That every functor in a suitable setting has this property is the theorem Fourier--Mukai theory is aimed at. It is stated nowhere in this file.

Equations

• C.IsKernelFunctor Φ = ∃ (K : 𝒵), Nonempty (Φ ≅ C.transform K)

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.isKernelFunctor_transform {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (K : 𝒵) : C.IsKernelFunctor (C.transform K)

A transform is a kernel functor, witnessed by its own kernel.

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.IsKernelFunctor.of_natIso {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] {C : Correspondence 𝒳 𝒴 𝒵} {Φ Ψ : Functor 𝒳 𝒴} (h : C.IsKernelFunctor Φ) (e : Φ ≅ Ψ) : C.IsKernelFunctor Ψ

Being a kernel functor is invariant under natural isomorphism.

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.IsKernelFunctor.kernel {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] {C : Correspondence 𝒳 𝒴 𝒵} {Φ : Functor 𝒳 𝒴} (h : C.IsKernelFunctor Φ) : 𝒵

A named kernel for a kernel functor, together with its isomorphism. The choice is not canonical, and no result in this file depends on which kernel is returned.

Equations

• h.kernel = Exists.choose h

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.IsKernelFunctor.iso {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] {C : Correspondence 𝒳 𝒴 𝒵} {Φ : Functor 𝒳 𝒴} (h : C.IsKernelFunctor Φ) : Φ ≅ C.transform h.kernel

The isomorphism witnessing that Φ is the transform of the chosen kernel.

Equations

• h.iso = ⋯.some

theorem CategoryTheory.Triangulated.FourierMukai.transform_isTriangulated {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] [Limits.HasZeroObject 𝒳] [HasShift 𝒳 ℤ] [Preadditive 𝒳] [∀ (n : ℤ), (shiftFunctor 𝒳 n).Additive] [Pretriangulated 𝒳] [Limits.HasZeroObject 𝒴] [HasShift 𝒴 ℤ] [Preadditive 𝒴] [∀ (n : ℤ), (shiftFunctor 𝒴 n).Additive] [Pretriangulated 𝒴] [Limits.HasZeroObject 𝒵] [HasShift 𝒵 ℤ] [Preadditive 𝒵] [∀ (n : ℤ), (shiftFunctor 𝒵 n).Additive] [Pretriangulated 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (K : 𝒵) [C.pull.CommShift ℤ] [(C.tensor.obj K).CommShift ℤ] [C.push.CommShift ℤ] [C.pull.IsTriangulated] [(C.tensor.obj K).IsTriangulated] [C.push.IsTriangulated] : (C.transform K).IsTriangulated

The transform is triangulated as soon as its three constituents are.

Exactness of the twist tensor.obj K is a hypothesis on the chosen kernel, not a property of C: the geometric statement it stands for is that − ⊗^L P is exact, which for a general kernel needs the derived tensor product rather than the underived one.

theorem CategoryTheory.Triangulated.FourierMukai.transform_additive {𝒳 : Type u} {𝒴 : Type u'} {𝒵 : Type u''} [Category.{v, u} 𝒳] [Category.{v', u'} 𝒴] [Category.{v'', u''} 𝒵] [Limits.HasZeroObject 𝒳] [HasShift 𝒳 ℤ] [Preadditive 𝒳] [∀ (n : ℤ), (shiftFunctor 𝒳 n).Additive] [Pretriangulated 𝒳] [Limits.HasZeroObject 𝒴] [HasShift 𝒴 ℤ] [Preadditive 𝒴] [∀ (n : ℤ), (shiftFunctor 𝒴 n).Additive] [Pretriangulated 𝒴] [Limits.HasZeroObject 𝒵] [HasShift 𝒵 ℤ] [Preadditive 𝒵] [∀ (n : ℤ), (shiftFunctor 𝒵 n).Additive] [Pretriangulated 𝒵] (C : Correspondence 𝒳 𝒴 𝒵) (K : 𝒵) [C.pull.CommShift ℤ] [(C.tensor.obj K).CommShift ℤ] [C.push.CommShift ℤ] [C.pull.IsTriangulated] [(C.tensor.obj K).IsTriangulated] [C.push.IsTriangulated] : (C.transform K).Additive

A transform of triangulated constituents is additive. Immediate from transform_isTriangulated, and stated separately because Additive is the hypothesis the Grothendieck-group API asks for.