Composing two geometric Fourier--Mukai transports #
KernelSwap.lean gives a geometric kernel autoequivalence and shows it
transports a stability condition. KernelConvolution.lean gives the geometric
convolution of two kernels, with no supplied fields — its conv and
compIso are both derived. This file is the one statement that needs both:
transporting along two geometric Fourier--Mukai transforms is transporting along the transform of their convolved kernel.
Symmetry/Autoequivalence/FourierMukai proves that abstractly
(KernelAutoequivalence.actStab_trans), for a supplied ConvolutionData.
Here the convolution data is geometricConvolutionData — assembled from the
geometric ledger — so nothing in this file is supplied at all.
No new contracts #
Every hypothesis below already exists: the two autoequivalences' own ledgers,
and the seven classical inputs geometricConvolutionData names (flat base
change, the two projection formulas, the monoidal pullback, and the two route
classes). This file introduces no class and asks for no datum. It is
composition of what the two ledgers already produce.
That is also why it is short. The mathematics was done in #466 abstractly and
in KernelConvolution.lean geometrically; what was missing was that the two
could be joined, which needed the geometric autoequivalence to exist at all
(KernelSwap.lean) and its exactness to be reachable by instance search.
What this file does not assert #
- Nothing is constructed that was not already constructible. Every input is a hypothesis, and the whole ledger below it remains uninhabited: no scheme is shown to admit any of these contracts.
- No monoid or group of geometric kernel autoequivalences. This is the associativity clause of an action and nothing more — the abstract file's docstring explains at length why no identity law follows, and none is claimed here either.
- Nothing about
toAutPairorAutPairQuotfor the geometric composite. - No claim that any geometric transform is an equivalence; the invertibility of
each assembled adjunction's unit and counit is assumed, as in
KernelSwap.
The composite of two geometric kernel autoequivalences.
KernelAutoequivalence.trans at the two geometric autoequivalences and the
geometric convolution data. Its kernel is convKernel G K₁' K₂' for the two
adjoint-derived kernels, and its equivalence is the composite of the two.
Nothing is supplied: the convolution data comes from
geometricConvolutionData, whose own conv and compIso are derived.
Equations
- One or more equations did not get rendered due to their size.