Convolution of Fourier--Mukai kernels #

Geometrically, for P ∈ D(X × Y) and Q ∈ D(Y × Z) the composite Φ_Q ∘ Φ_P is again a Fourier--Mukai transform, with kernel the convolution

Q ∗ P = Rπ_{XZ*}(π_{XY}^* P ⊗^L π_{YZ}^* Q) ∈ D(X × Z)

which is the classical composition law. Proving it from the three-projection description needs the projection formula and flat base change on a triple product, none of which the abstract Correspondence of FourierMukai.Basic carries.

So convolution enters here as supplied data, not as a theorem. A ConvolutionData names a kernel-level operation together with the family of isomorphisms that Prop. 5.10 asserts, for three correspondences that share their outer categories in the pattern 𝒳 → 𝒴 → 𝒵. What this file then proves are the consequences: that kernel functors are closed under composition, and that convolution is well behaved under isomorphism of either kernel.

This is the same division of labour as StabilityCondition.Families.Basic, where the geometric tests are supplied by a caller and the file proves what follows from them. The value is that a later geometric realization has one named obligation to discharge rather than an implicit one, and that everything downstream of Prop. 5.10 is already available once it is. For endocorrespondences whose kernels genuinely form a monoidal category, CoherentConvolutionData is the stable root: it makes the operation functorial and packages its associator, unitors, pentagon, and triangle together. It forgets one-way to ConvolutionData.

What this file does not assert #

Nothing constructs a ConvolutionData or CoherentConvolutionData, and no example is exhibited. That is not an omission for want of trying: compIso is required to hold uniformly in Q, so the cheap degenerate constructions — fold the middle transform into C₃.push, or take conv P Q = P — all fail, because they produce a C₃ whose transform has one fixed Q baked into it and so cannot meet the requirement for any other. The uniformity is what gives the structure content, and discharging it is a geometric obligation.
The legacy ConvolutionData.conv is a bare function 𝒲₁ → 𝒲₂ → 𝒲₃, not a functor. It is not assumed to be additive, exact, or even to send isomorphic kernels to isomorphic kernels — only to send them to kernels with isomorphic transforms, which is what transformMapConvIso proves and is strictly weaker.
Associativity of convolution splits. At the transform level it is a theorem, convolutionTransformAssoc, derived from the four compIso families alone — no new input. At the kernel level it is ConvolutionAssocData, a second layer of supplied data: recovering the kernel-level isomorphism from the transform-level one would need a kernel to be determined by its transform (Orlov uniqueness), which is not available here. No result here depends on the kernel-level layer, and nothing constructs it. CoherentConvolutionData is the stronger alternative when a caller can supply the full monoidal kernel structure.
Triangulatedness does not transport across compIso. Moving IsTriangulated along a natural isomorphism needs that isomorphism to commute with the shift (NatTrans.CommShift), which is an extra hypothesis on the supplied data rather than a consequence of it.
No kernel is claimed to be determined by its transform, so conv is not claimed to be the unique operation satisfying compIso.