Fourier--Mukai kernel autoequivalences

This is the categorical source of truth for a kernel functor that is an autoequivalence. It contains the presentation by a correspondence and kernel, dual and unit kernels, convolution of kernel autoequivalences, and the induced automorphism of K₀.

Direction of dependence

The Bridgeland action is deliberately absent. It is a consumer in WeakStabilityCondition/StabilityCondition/Symmetry/Autoequivalence/ which imports this module. Algebraic-geometric constructions of these generic objects, and the action of geometric kernels on stability conditions, live with the geometric objects under AlgebraicGeometry/DerivedCategory/.

What this file does not assert

• Nothing constructs a KernelAutoequivalence. The equivalence and the isomorphism to a transform are both supplied. That a Fourier--Mukai transform with a suitable kernel is an equivalence is the classical theorem, and it needs the geometry the abstract Correspondence does not carry.

• Nothing constructs a DualKernel from geometry. That the quasi-inverse of a Fourier--Mukai equivalence is again one — with the derived-dual kernel P^∨ ⊗ p^*ω[dim] — is classical, and supplying it is geometry. What this file proves the categorical consequences of having one available, including that the two kernels' class maps are mutually inverse (transformK₀_dual_comp).

  Since #559's adjunction stage there is one abstract constructor: DualKernel.ofLeftAdjointKernel builds a dual kernel from a LeftAdjointKernelData, by uniqueness of adjoints, and ofRightAdjointKernel does the same on the other side. That moves the supplied datum, it does not discharge it — LeftAdjointKernelData is itself supplied in FourierMukai/Adjunction.lean, and DualKernel.toLeftAdjointKernelData goes back, so for a kernel autoequivalence the two are interderivable and neither is weaker.

• No group of kernel autoequivalences. Composing two kernel autoequivalences needs a ConvolutionData supplied per pair (trans), and the unit needs a supplied UnitKernelData. No identity law relating those data is asserted here.

• Nothing constructs a UnitKernelData. That 𝒪_Δ presents the identity as a transform is the classical statement, and it needs the geometry the abstract Correspondence does not carry.

• Nothing constructs a non-trivial LeftAdjointKernelData or RightAdjointKernelData. UnitKernelData.toLeftAdjointKernelData produces one from a unit kernel, but it is the statement that 𝟭 C is its own adjoint, transported across unitIso; it says nothing about corr. That a general Φ_P has kernel-presented adjoints is Grothendieck duality.

• Nothing about stability conditions, Bridgeland's Stab(X) as a manifold, or continuity of an induced action.

structure CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence (C : Type u) [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (𝒲 : Type t) [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] : Type (max (max (max t u) w) x)

A kernel autoequivalence: an autoequivalence of C presented as a Fourier--Mukai transform.

The correspondence, the kernel, the equivalence, and the isomorphism between them are all supplied. Nothing here proves that any transform is an equivalence — that is the classical theorem and it needs geometry.

• corr : Correspondence C C 𝒲

  The correspondence from C to itself.

• kernel : 𝒲

  The kernel.

• equiv : C ≌ C

  The autoequivalence.

• iso : self.equiv.functor ≅ self.corr.transform self.kernel

  Its functor is the transform with that kernel.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.of_obj_eq {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (E : C) : K₀.of C (A.equiv.functor.obj E) = K₀.of C ((A.corr.transform A.kernel).obj E)

On classes of objects, the autoequivalence and its transform agree.

Stated this way round rather than as a simp lemma about K₀.map: the existing K₀.map_of already rewrites that left-hand side, so a lemma phrased against it would not be in simp-normal form.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.map_eq_transformK₀ {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) [A.corr.pull.CommShift ℤ] [(A.corr.tensor.obj A.kernel).CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [(A.corr.tensor.obj A.kernel).IsTriangulated] [A.corr.push.IsTriangulated] [A.equiv.functor.CommShift ℤ] [A.equiv.functor.IsTriangulated] : K₀.map A.equiv.functor = A.corr.transformK₀ A.kernel

The action on classes is computed by the kernel.

Exactly Correspondence.K₀_map_eq_transformK₀ at the supplied isomorphism. It is what makes the kernel, rather than the functor's construction, the thing that determines the transported charge.

Until #487 this proof had a step in it: the stability track carried its own endofunctor-only K₀.mapF, definitionally equal to K₀.map but a different constant, and the theorem had to cross that identification. mapF is retired and the crossing is gone.

structure CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) : Type (max (max t u) w)

A dual kernel for a kernel autoequivalence: a kernel presenting the quasi-inverse as a transform of the same correspondence.

Classically this is the derived dual P^∨ ⊗ p^*ω_X[dim X], and its existence is a theorem about smooth projective varieties. Here it is supplied. What it buys is that both directions of the equivalence become kernel-computable, which is what turns actStab's remaining hypothesis into kernel data.

• dual : 𝒲

  The kernel of the quasi-inverse.

• invIso : A.equiv.inverse ≅ A.corr.transform self.dual

  The quasi-inverse is the transform with that kernel.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.map_inverse_eq_transformK₀ {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] {A : KernelAutoequivalence C 𝒲} (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] [A.equiv.inverse.CommShift ℤ] [A.equiv.inverse.IsTriangulated] : K₀.map A.equiv.inverse = A.corr.transformK₀ D.dual

The quasi-inverse's action on classes is computed by the dual kernel. The mirror of map_eq_transformK₀, and the reason actStabOfDual can state its hypothesis in kernel terms.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.transformK₀_dual_comp {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] {A : KernelAutoequivalence C 𝒲} (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] [A.equiv.inverse.CommShift ℤ] [A.equiv.inverse.IsTriangulated] [(A.corr.tensor.obj A.kernel).CommShift ℤ] [(A.corr.tensor.obj A.kernel).IsTriangulated] [A.equiv.functor.CommShift ℤ] [A.equiv.functor.IsTriangulated] : (A.corr.transformK₀ D.dual).comp (A.corr.transformK₀ A.kernel) = AddMonoidHom.id (K₀ C)

The two kernels' class maps are mutually inverse.

Proved from K₀.map_comp_map_eq_id on the equivalence's unit, then transported across both kernel identifications. Neither convolution nor an identity kernel is involved: the inverse relation comes from the supplied equivalence, not from conv P P^∨ ≅ 𝒪_Δ.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.transformK₀_comp_dual {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] {A : KernelAutoequivalence C 𝒲} (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] [A.equiv.inverse.CommShift ℤ] [A.equiv.inverse.IsTriangulated] [(A.corr.tensor.obj A.kernel).CommShift ℤ] [(A.corr.tensor.obj A.kernel).IsTriangulated] [A.equiv.functor.CommShift ℤ] [A.equiv.functor.IsTriangulated] : (A.corr.transformK₀ A.kernel).comp (A.corr.transformK₀ D.dual) = AddMonoidHom.id (K₀ C)

The composite in the other order is also the identity.

def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.transformK₀AddEquiv {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] {A : KernelAutoequivalence C 𝒲} (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] [A.equiv.inverse.CommShift ℤ] [A.equiv.inverse.IsTriangulated] [(A.corr.tensor.obj A.kernel).CommShift ℤ] [(A.corr.tensor.obj A.kernel).IsTriangulated] [A.equiv.functor.CommShift ℤ] [A.equiv.functor.IsTriangulated] : K₀ C ≃+ K₀ C

The kernel's class map, as an automorphism of K₀ C.

The two comp lemmas above are exactly the two round-trip identities AddMonoidHom.toAddEquiv asks for, so the bundling is bookkeeping. What it records is that having a DualKernel is what makes the class map invertible: transformK₀ on its own is not claimed invertible anywhere (FourierMukai/GrothendieckGroup.lean says so explicitly), and the inverse here is the dual kernel's class map, not an abstract inverse.

The equivalence is on K₀ C, not on a class lattice Λ. Nothing here maps Λ — toAutPair still takes its lam as supplied data.

Equations

• D.transformK₀AddEquiv = (A.corr.transformK₀ A.kernel).toAddEquiv (A.corr.transformK₀ D.dual) ⋯ ⋯

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.transformK₀AddEquiv_apply {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] {A : KernelAutoequivalence C 𝒲} (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] [A.equiv.inverse.CommShift ℤ] [A.equiv.inverse.IsTriangulated] [(A.corr.tensor.obj A.kernel).CommShift ℤ] [(A.corr.tensor.obj A.kernel).IsTriangulated] [A.equiv.functor.CommShift ℤ] [A.equiv.functor.IsTriangulated] (x : K₀ C) : D.transformK₀AddEquiv x = (A.corr.transformK₀ A.kernel) x

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.transformK₀AddEquiv_symm_apply {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] {A : KernelAutoequivalence C 𝒲} (D : A.DualKernel) [A.corr.pull.CommShift ℤ] [A.corr.push.CommShift ℤ] [A.corr.pull.IsTriangulated] [A.corr.push.IsTriangulated] [(A.corr.tensor.obj D.dual).CommShift ℤ] [(A.corr.tensor.obj D.dual).IsTriangulated] [A.equiv.inverse.CommShift ℤ] [A.equiv.inverse.IsTriangulated] [(A.corr.tensor.obj A.kernel).CommShift ℤ] [(A.corr.tensor.obj A.kernel).IsTriangulated] [A.equiv.functor.CommShift ℤ] [A.equiv.functor.IsTriangulated] (x : K₀ C) : D.transformK₀AddEquiv.symm x = (A.corr.transformK₀ D.dual) x

Dual kernels derived from adjunction data

FourierMukai/Adjunction.lean supplies LeftAdjointKernelData and RightAdjointKernelData: a kernel for the opposite correspondence together with an adjunction between the two transforms. For a kernel autoequivalence those give a DualKernel outright, by uniqueness of adjoints — the quasi-inverse of an equivalence is both its left and its right adjoint, so an adjoint presented by a kernel is isomorphic to it.

toLeftAdjointKernelData and toRightAdjointKernelData go back, so for a kernel autoequivalence the three data are interderivable and the constructors below buy no new existence. What they buy is the shape of the input: LeftAdjointKernelData is stated for an arbitrary kernel with no equivalence in sight, which is the form a geometric adjunction theorem has, whereas DualKernel.invIso presupposes the equivalence and names its inverse.

def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.ofLeftAdjointKernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (L : LeftAdjointKernelData A.corr A.corr A.kernel) : A.DualKernel

A dual kernel derived from left-adjoint kernel data.

A.equiv.inverse is left adjoint to A.equiv.functor, hence — across A.iso — to A.corr.transform A.kernel. L.adj says the same of A.corr.transform L.adjKernel. Uniqueness of left adjoints identifies the two, and that identification is exactly DualKernel.invIso.

This is the first constructor of a DualKernel from something other than a directly supplied invIso. It is not a geometric construction: the adjunction is still supplied.

Equations

• CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.ofLeftAdjointKernel A L = { dual := L.adjKernel, invIso := L.isoOfAdj (A.equiv.symm.toAdjunction.ofNatIsoRight A.iso) }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.ofLeftAdjointKernel_dual {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (L : LeftAdjointKernelData A.corr A.corr A.kernel) : (ofLeftAdjointKernel A L).dual = L.adjKernel

def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.ofRightAdjointKernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (R : RightAdjointKernelData A.corr A.corr A.kernel) : A.DualKernel

A dual kernel derived from right-adjoint kernel data.

The mirror of ofLeftAdjointKernel, through Adjunction.rightAdjointUniq. Both exist because the quasi-inverse of an equivalence is an adjoint on both sides; classically the two adjoint kernels of a general Φ_P differ by the dualizing twist, and it is Serre duality that collapses the difference when Φ_P is an equivalence.

The collapse is reachable here — (ofLeftAdjointKernel A L).toRightAdjointKernelData is right-adjoint data with the same kernel L.adjKernel — but read where it comes from: the supplied A.equiv, whose inverse is an adjoint on both sides by construction. No dualizing object and no duality theorem is involved, and for a kernel with no equivalence attached FourierMukai/Adjunction.lean still relates the two sides not at all.

Equations

• CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.ofRightAdjointKernel A R = { dual := R.adjKernel, invIso := R.isoOfAdj (A.equiv.toAdjunction.ofNatIsoLeft A.iso) }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.ofRightAdjointKernel_dual {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (R : RightAdjointKernelData A.corr A.corr A.kernel) : (ofRightAdjointKernel A R).dual = R.adjKernel

def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.toLeftAdjointKernelData {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (D : A.DualKernel) : LeftAdjointKernelData A.corr A.corr A.kernel

A dual kernel already carries the left adjunction.

The converse of ofLeftAdjointKernel, and the reason its docstring does not claim to weaken the hypothesis: transporting A.equiv.symm.toAdjunction along A.iso and D.invIso recovers the adjunction. So for a kernel autoequivalence the two data are interderivable.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.toLeftAdjointKernelData_adjKernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (D : A.DualKernel) : (toLeftAdjointKernelData A D).adjKernel = D.dual

def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.toRightAdjointKernelData {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (D : A.DualKernel) : RightAdjointKernelData A.corr A.corr A.kernel

A dual kernel already carries the right adjunction, mirroring toLeftAdjointKernelData.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.toRightAdjointKernelData_adjKernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (D : A.DualKernel) : (toRightAdjointKernelData A D).adjKernel = D.dual

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.ofLeftAdjointKernel_toLeftAdjointKernelData_dual {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (D : A.DualKernel) : (ofLeftAdjointKernel A (toLeftAdjointKernelData A D)).dual = D.dual

The left round trip is the identity on the kernel.

Only on the kernel. The reconstructed dual kernel's invIso is D.invIso carried across two transports and Adjunction.leftAdjointUniq; it is not claimed equal to D.invIso, and proving it so would need that lemma's coherence statements, which nothing here consumes.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.DualKernel.ofRightAdjointKernel_toRightAdjointKernelData_dual {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (D : A.DualKernel) : (ofRightAdjointKernel A (toRightAdjointKernelData A D)).dual = D.dual

The right round trip is the identity on the kernel, with the same caveat.

@[reducible]

def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.trans {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲₁ : Type t₁} {𝒲₂ : Type t₂} {𝒲₃ : Type t₃} [Category.{x₁, t₁} 𝒲₁] [Limits.HasZeroObject 𝒲₁] [HasShift 𝒲₁ ℤ] [Preadditive 𝒲₁] [∀ (n : ℤ), (shiftFunctor 𝒲₁ n).Additive] [Pretriangulated 𝒲₁] [Category.{x₂, t₂} 𝒲₂] [Limits.HasZeroObject 𝒲₂] [HasShift 𝒲₂ ℤ] [Preadditive 𝒲₂] [∀ (n : ℤ), (shiftFunctor 𝒲₂ n).Additive] [Pretriangulated 𝒲₂] [Category.{x₃, t₃} 𝒲₃] [Limits.HasZeroObject 𝒲₃] [HasShift 𝒲₃ ℤ] [Preadditive 𝒲₃] [∀ (n : ℤ), (shiftFunctor 𝒲₃ n).Additive] [Pretriangulated 𝒲₃] (A₁ : KernelAutoequivalence C 𝒲₁) (A₂ : KernelAutoequivalence C 𝒲₂) (corr₃ : Correspondence C C 𝒲₃) (D : ConvolutionData A₁.corr A₂.corr corr₃) : KernelAutoequivalence C 𝒲₃

Composing two kernel autoequivalences, given convolution data.

The composite is again a kernel autoequivalence, and its kernel is the convolution of the two. The isomorphism is the one ConvolutionData.isKernelFunctor_comp already uses: whisker each supplied isomorphism into place, then apply compIso.

corr₃ and the convolution data are supplied — this constructs the composite from them, it does not produce a correspondence for the composite out of nothing.

Marked @[reducible] so that instance search sees equiv as A₁.equiv.trans A₂.equiv and picks up the six Equivalence.trans instances from Stability/Composition. Declaring them by hand for the composite instead does not work: IsTriangulated is indexed by the CommShift instance, so a hand-rolled copy is a different term from the one the use site finds.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.trans_kernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲₁ : Type t₁} {𝒲₂ : Type t₂} {𝒲₃ : Type t₃} [Category.{x₁, t₁} 𝒲₁] [Limits.HasZeroObject 𝒲₁] [HasShift 𝒲₁ ℤ] [Preadditive 𝒲₁] [∀ (n : ℤ), (shiftFunctor 𝒲₁ n).Additive] [Pretriangulated 𝒲₁] [Category.{x₂, t₂} 𝒲₂] [Limits.HasZeroObject 𝒲₂] [HasShift 𝒲₂ ℤ] [Preadditive 𝒲₂] [∀ (n : ℤ), (shiftFunctor 𝒲₂ n).Additive] [Pretriangulated 𝒲₂] [Category.{x₃, t₃} 𝒲₃] [Limits.HasZeroObject 𝒲₃] [HasShift 𝒲₃ ℤ] [Preadditive 𝒲₃] [∀ (n : ℤ), (shiftFunctor 𝒲₃ n).Additive] [Pretriangulated 𝒲₃] (A₁ : KernelAutoequivalence C 𝒲₁) (A₂ : KernelAutoequivalence C 𝒲₂) (corr₃ : Correspondence C C 𝒲₃) (D : ConvolutionData A₁.corr A₂.corr corr₃) : (A₁.trans A₂ corr₃ D).kernel = D.conv A₁.kernel A₂.kernel

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.trans_equiv {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲₁ : Type t₁} {𝒲₂ : Type t₂} {𝒲₃ : Type t₃} [Category.{x₁, t₁} 𝒲₁] [Limits.HasZeroObject 𝒲₁] [HasShift 𝒲₁ ℤ] [Preadditive 𝒲₁] [∀ (n : ℤ), (shiftFunctor 𝒲₁ n).Additive] [Pretriangulated 𝒲₁] [Category.{x₂, t₂} 𝒲₂] [Limits.HasZeroObject 𝒲₂] [HasShift 𝒲₂ ℤ] [Preadditive 𝒲₂] [∀ (n : ℤ), (shiftFunctor 𝒲₂ n).Additive] [Pretriangulated 𝒲₂] [Category.{x₃, t₃} 𝒲₃] [Limits.HasZeroObject 𝒲₃] [HasShift 𝒲₃ ℤ] [Preadditive 𝒲₃] [∀ (n : ℤ), (shiftFunctor 𝒲₃ n).Additive] [Pretriangulated 𝒲₃] (A₁ : KernelAutoequivalence C 𝒲₁) (A₂ : KernelAutoequivalence C 𝒲₂) (corr₃ : Correspondence C C 𝒲₃) (D : ConvolutionData A₁.corr A₂.corr corr₃) : (A₁.trans A₂ corr₃ D).equiv = A₁.equiv.trans A₂.equiv

structure CategoryTheory.Triangulated.FourierMukai.UnitKernelData {C : Type u} [Category.{w, u} C] {𝒲 : Type t} [Category.{x, t} 𝒲] (corr : Correspondence C C 𝒲) : Type (max (max t u) w)

A unit kernel: a kernel presenting the identity functor as a transform.

Classically this is 𝒪_Δ ∈ D(X × X), and that its transform is the identity is a theorem about the diagonal. Here it is supplied, like every other geometric input to this file.

• unitKernel : 𝒲

  The kernel.

• unitIso : Functor.id C ≅ corr.transform self.unitKernel

  It presents 𝟭 C as a transform of corr.

@[reducible]

def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.id {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (U : UnitKernelData corr) : KernelAutoequivalence C 𝒲

The identity kernel autoequivalence, from a unit kernel.

Equivalence.refl.functor and Equivalence.refl.inverse are both 𝟭 C definitionally, so the one supplied isomorphism serves as iso here and as invIso in UnitKernelData.toDualKernel.

@[reducible] for the same reason as trans: a use site's instance search has to see equiv as Equivalence.refl.

This produces the unit object, and only that. It is not proved to be a unit for trans, and cannot be without convolution data comparing corr with itself — see the module docstring.

Equations

• CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.id corr U = { corr := corr, kernel := U.unitKernel, equiv := CategoryTheory.Equivalence.refl, iso := U.unitIso }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.id_kernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (U : UnitKernelData corr) : (id corr U).kernel = U.unitKernel

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.id_equiv {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (U : UnitKernelData corr) : (id corr U).equiv = Equivalence.refl

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.id_corr {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (U : UnitKernelData corr) : (id corr U).corr = corr

def CategoryTheory.Triangulated.FourierMukai.UnitKernelData.toDualKernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] {corr : Correspondence C C 𝒲} (U : UnitKernelData corr) : (KernelAutoequivalence.id corr U).DualKernel

The identity's dual kernel is the unit kernel itself.

The one place the identity costs nothing extra: Equivalence.refl.inverse is 𝟭 C, so the same supplied isomorphism discharges DualKernel.invIso. Every DualKernel consequence — transformK₀AddEquiv, actStabOfDual, toAutPair — therefore applies to KernelAutoequivalence.id with no further geometric input.

Equations

• U.toDualKernel = { dual := U.unitKernel, invIso := U.unitIso }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.UnitKernelData.toDualKernel_dual {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] {corr : Correspondence C C 𝒲} (U : UnitKernelData corr) : U.toDualKernel.dual = U.unitKernel

def CategoryTheory.Triangulated.FourierMukai.UnitKernelData.toLeftAdjointKernelData {C : Type u} [Category.{w, u} C] {𝒲 : Type t} [Category.{x, t} 𝒲] {corr : Correspondence C C 𝒲} (U : UnitKernelData corr) : LeftAdjointKernelData corr corr U.unitKernel

The unit kernel is a left adjoint kernel for itself.

𝟭 C ⊣ 𝟭 C, transported along U.unitIso on both sides. This is the only LeftAdjointKernelData this repository produces, and it is the trivial one: it says the identity is its own adjoint, which is true in any category and carries no information about corr.

Its point is that LeftAdjointKernelData is inhabited from data the tree already has, so the adjunction layer is not an interface nothing can reach. A non-trivial instance is Grothendieck duality and is not available here.

Equations

• U.toLeftAdjointKernelData = { adjKernel := U.unitKernel, adj := (CategoryTheory.Adjunction.id.ofNatIsoLeft U.unitIso).ofNatIsoRight U.unitIso }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.UnitKernelData.toLeftAdjointKernelData_adjKernel {C : Type u} [Category.{w, u} C] {𝒲 : Type t} [Category.{x, t} 𝒲] {corr : Correspondence C C 𝒲} (U : UnitKernelData corr) : U.toLeftAdjointKernelData.adjKernel = U.unitKernel

theorem CategoryTheory.Triangulated.FourierMukai.UnitKernelData.ofLeftAdjointKernel_dual {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] {corr : Correspondence C C 𝒲} (U : UnitKernelData corr) : (KernelAutoequivalence.DualKernel.ofLeftAdjointKernel (KernelAutoequivalence.id corr U) U.toLeftAdjointKernelData).dual = U.toDualKernel.dual

The derived dual kernel of the identity is the supplied one.

On the kernel object. Running U.toLeftAdjointKernelData through DualKernel.ofLeftAdjointKernel lands on U.unitKernel, which is what toDualKernel supplies directly. The two invIso fields are not claimed equal — toDualKernel uses U.unitIso itself, while the derived one is the image of an adjunction under Adjunction.leftAdjointUniq.

def CategoryTheory.Triangulated.FourierMukai.trivialUnitKernelData {C : Type u} [Category.{w, u} C] (K : C) : UnitKernelData (trivialCorrespondence C)

UnitKernelData is satisfiable.

The trivial correspondence's transform is the identity definitionally, so the identity functor is presented by every kernel and unitIso is Iso.refl.

Satisfiability only, exactly as in FourierMukai/Witness.lean: this says the structure's fields can be met simultaneously. It says nothing about 𝒪_Δ, nothing about any diagonal, and nothing about whether Families.geometricUnitKernelData's contracts are dischargeable.

Equations

• CategoryTheory.Triangulated.FourierMukai.trivialUnitKernelData K = { unitKernel := K, unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id C) }

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.trivialUnitKernelData_unitKernel {C : Type u} [Category.{w, u} C] (K : C) : (trivialUnitKernelData K).unitKernel = K

The equivalence, derived rather than supplied

KernelAutoequivalence takes its equivalence and the comparison isomorphism as supplied fields, and every consequence in this file is conditional on them. This section removes that particular supply point: a RightAdjointKernelData whose adjunction has invertible unit and counit already is an equivalence, by Adjunction.toEquivalence, and its functor is the transform definitionally — so the comparison isomorphism is Iso.refl.

This is not a weakening, and isIso_unit/isIso_counit below prove it. Given a kernel autoequivalence together with a right adjoint kernel, the adjunction's unit and counit are invertible: Mathlib supplies that as instances once the functors are equivalences. So the two data are interderivable, exactly as DualKernel and LeftAdjointKernelData are.

What changes is the shape of the hypothesis, and that is the whole point. "There exists an equivalence and an isomorphism to the transform" is not something a geometric theorem produces. "The unit and counit of this adjunction are isomorphisms" is: it is pointwise, it is checkable, and its two halves are full faithfulness and essential surjectivity — which is the form the Bondal--Orlov criterion actually takes. ofFullyFaithful below is that split, using Mathlib's unit_isIso_of_L_fully_faithful.

Nothing here supplies the invertibility. That is the second half of the layer-3 work and it needs geometry this repository does not have.

@[reducible]

noncomputable def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.ofRightAdjointKernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (K : 𝒲) (R : RightAdjointKernelData corr corr K) [∀ (X : C), IsIso (R.adj.unit.app X)] [∀ (Y : C), IsIso (R.adj.counit.app Y)] : KernelAutoequivalence C 𝒲

A kernel autoequivalence, from an adjoint kernel with invertible unit and counit.

Adjunction.toEquivalence on the supplied adjunction. Its functor field is corr.transform K definitionally, so iso is Iso.refl and nothing is transported.

The first constructor of a KernelAutoequivalence from anything other than a directly supplied equivalence.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.ofRightAdjointKernel_corr {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (K : 𝒲) (R : RightAdjointKernelData corr corr K) [∀ (X : C), IsIso (R.adj.unit.app X)] [∀ (Y : C), IsIso (R.adj.counit.app Y)] : (ofRightAdjointKernel corr K R).corr = corr

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.ofRightAdjointKernel_kernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (K : 𝒲) (R : RightAdjointKernelData corr corr K) [∀ (X : C), IsIso (R.adj.unit.app X)] [∀ (Y : C), IsIso (R.adj.counit.app Y)] : (ofRightAdjointKernel corr K R).kernel = K

@[reducible]

noncomputable def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.dualKernelOfRightAdjointKernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (K : 𝒲) (R : RightAdjointKernelData corr corr K) [∀ (X : C), IsIso (R.adj.unit.app X)] [∀ (Y : C), IsIso (R.adj.counit.app Y)] : (ofRightAdjointKernel corr K R).DualKernel

The same datum also gives the dual kernel, for free.

toEquivalence's inverse is the adjunction's right adjoint, which is corr.transform R.adjKernel definitionally — so invIso is Iso.refl and DualKernel.ofRightAdjointKernel's trip through Adjunction.rightAdjointUniq is not needed here. One RightAdjointKernelData with invertible unit and counit yields the equivalence and its dual kernel.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.dualKernelOfRightAdjointKernel_dual {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (K : 𝒲) (R : RightAdjointKernelData corr corr K) [∀ (X : C), IsIso (R.adj.unit.app X)] [∀ (Y : C), IsIso (R.adj.counit.app Y)] : (dualKernelOfRightAdjointKernel corr K R).dual = R.adjKernel

noncomputable def CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.ofFullyFaithful {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (K : 𝒲) (R : RightAdjointKernelData corr corr K) [(corr.transform K).Full] [(corr.transform K).Faithful] [∀ (Y : C), IsIso (R.adj.counit.app Y)] : KernelAutoequivalence C 𝒲

The hypothesis split the way a criterion would deliver it.

Full faithfulness of the transform gives the unit, by Mathlib's unit_isIso_of_L_fully_faithful; the counit is still asked for, and it is the essential-surjectivity half. Stated because this is the shape Bondal--Orlov has — fully faithful, plus a condition — and a geometric criterion would land here rather than on the raw unit.

Equations

• CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.ofFullyFaithful corr K R = CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.ofRightAdjointKernel corr K R

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.ofFullyFaithful_kernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (corr : Correspondence C C 𝒲) (K : 𝒲) (R : RightAdjointKernelData corr corr K) [(corr.transform K).Full] [(corr.transform K).Faithful] [∀ (Y : C), IsIso (R.adj.counit.app Y)] : (ofFullyFaithful corr K R).kernel = K

The converse: nothing above weakens the hypothesis

If a kernel autoequivalence and a right adjoint kernel for the same kernel are both on the table, the adjunction's unit and counit are already invertible. So ofRightAdjointKernel does not lower the bar — it restates it in a form a geometric criterion can attack. This is the same honesty check DualKernel.toLeftAdjointKernelData performs one layer down.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.transform_isEquivalence {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) : (A.corr.transform A.kernel).IsEquivalence

The transform of a kernel autoequivalence is an equivalence. Transport of A.equiv along the supplied A.iso, and the hinge of both lemmas below.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.isIso_counit {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (R : RightAdjointKernelData A.corr A.corr A.kernel) : IsIso R.adj.counit

The counit of any right adjoint kernel is invertible, given the equivalence.

theorem CategoryTheory.Triangulated.FourierMukai.KernelAutoequivalence.isIso_unit {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {𝒲 : Type t} [Category.{x, t} 𝒲] [Limits.HasZeroObject 𝒲] [HasShift 𝒲 ℤ] [Preadditive 𝒲] [∀ (n : ℤ), (shiftFunctor 𝒲 n).Additive] [Pretriangulated 𝒲] (A : KernelAutoequivalence C 𝒲) (R : RightAdjointKernelData A.corr A.corr A.kernel) : IsIso R.adj.unit

The unit of any right adjoint kernel is invertible, given the equivalence.

Through isEquivalence_right_of_isEquivalence_left: the right adjoint of an equivalence is an equivalence, and Mathlib's instance then gives the unit.