Fourier--Mukai presentations of dg adjunctions #
DGAdjunction.H0Presentation turns a strict dg adjunction into an ordinary
adjunction between named functors after transport through equivalences out of
the two homotopy categories. When those named functors are Fourier--Mukai
transforms, the resulting ordinary adjunction is exactly the datum required
by RightAdjointKernelData or LeftAdjointKernelData.
The constructors in this file perform that specialization. They reuse the existing kernel-adjunction structures rather than adding a dg-flavoured copy, and their two orientations agree definitionally with the existing operation that reads a right-adjoint kernel as a left-adjoint kernel after swapping the correspondences.
What remains supplied #
The equivalences and both endpoint natural isomorphisms are inputs. Thus no
dg lift or kernel is constructed here. In particular, these constructors do
not produce the kernel morphism realizing the unit or counit, an enhanced
kernel cone, or any comparison between a dg cone and a Fourier--Mukai kernel
cone. Those are the separate realization obligations recorded by
CounitKernelData and its companions.
Build a right-adjoint kernel datum from a strict dg adjunction whose two
H⁰ functors are presented by the indicated Fourier--Mukai transforms.
The kernel Q and both functor identifications are supplied by P; this
constructor contributes only the ordinary adjunction obtained from the
generic H0Presentation bridge.
Equations
- CategoryTheory.Triangulated.FourierMukai.RightAdjointKernelData.ofH0Presentation P adj = { adjKernel := Q, adj := P.toAdjunction adj }
Instances For
The constructor records the supplied right-adjoint kernel Q verbatim;
it performs no kernel selection.
The adjunction stored by ofH0Presentation is exactly the generic
presented adjunction, with no second transport.
Build a left-adjoint kernel datum from a strict dg adjunction whose two
H⁰ functors are presented by the indicated Fourier--Mukai transforms.
Here L : B ⥤ A presents the opposite-correspondence transform with
kernel Q, while S : A ⥤ B presents the original transform with kernel
K.
Equations
- CategoryTheory.Triangulated.FourierMukai.LeftAdjointKernelData.ofH0Presentation P adj = { adjKernel := Q, adj := P.toAdjunction adj }
Instances For
The constructor records the supplied left-adjoint kernel Q verbatim;
it performs no kernel selection.
The adjunction stored by ofH0Presentation is exactly the generic
presented adjunction, with no second transport.
The two specialization directions agree with the existing operation that reads a right-adjoint kernel datum as a left-adjoint kernel datum for the swapped correspondences.
The mirror conversion from a left-adjoint kernel datum back to a right-adjoint kernel datum also agrees definitionally with the presentation constructor.