Convolution of Fourier--Mukai kernels: the second ledger #
KernelCorrespondence.lean reduced a geometric Correspondence to three named
inputs. This file does the same for the composition law: the abstract
ConvolutionData asks for a kernel operation conv and the family of
isomorphisms Φ_P ⋙ Φ_Q ≅ Φ_{conv P Q}, both as supplied data, and this ledger
reduces both.
What this ledger buys #
conv stops being supplied. Classically
conv P Q = Rπ_{XW*}(π_{XY}^* P ⊗^L π_{YW}^* Q) on the triple product. Every
functor in that expression is one the first ledger already names — two
derived pullbacks, one derived tensor, one derived pushforward — so given a
triple product with its three projections, convKernel is a definition.
compIso stops being supplied. Prop. 5.10 is derived here
(geometricCompIso) from seven named inputs: the projection formula on each
slot (HasProjectionFormula, HasProjectionFormulaRight), flat base change
(HasFlatBaseChange), monoidality of derived pullback
(HasMonoidalDerivedPullback), the coherent derived-tensor root
(HasCoherentDerivedTensor), and agreement of the two pullback and the two
pushforward routes across the triple product (HasCommonPullbackRoute,
HasCommonPushforwardRoute). The honest statement of this ledger's effect:
Both fields of
ConvolutionDataare now constructed; what is supplied is the classical comparison data above, rooted in coherent functorial structures with the geometry it encodes stated in its docstring.
The earlier form of this file supplied compIso whole, as a
HasConvolutionComparison class naming the projection formula and flat base
change beside it without consuming them. That class is gone: the derivation
consumes its inputs or they would not be here.
Where the product finally becomes load-bearing #
KernelCorrespondence.lean deliberately did not require its middle scheme to
be a product, because Correspondence does not consume that. Here the
situation is different and the docstrings say so: the seven inputs are jointly
false without it. The base-change square is cartesian precisely because the
intermediate objects are honest fibre products, and the two route classes'
comm guards hold precisely because the projections really are projections.
TripleProductGeometry still carries the projections as data and does not
assert that the objects are products — nothing in this file consumes that
assertion. What consumes it is a caller discharging the seven classes, and
each class docstring says which piece of product geometry its instance
encodes. Asserting productness here would be an unconsumed hypothesis, which
is the shape both review rounds attacked.
What this file does not assert #
- Nothing constructs an instance of any of the seven classes, and no
scheme is shown to admit any of them. Inhabitant-free, exactly like the
first ledger: a clean axiom report on
geometricCompIsomeans the derivation adds nothing, not that a geometric Fourier--Mukai transform exists in this repository. Nothing here constructs aCorrespondence. - No associativity of convolution —
Convolution.leansays that needs a second data layer relating the two bracketings, and this ledger does not supply it. - No unit:
𝒪_Δalong the diagonal is absent, soUnitKernelDatais still unreachable geometrically.
The triple product and its three projections, supplied.
triple plays X ×_S Y ×_S W, and the three morphisms play the projections
onto the pairwise products Z₁ = X ×_S Y, Z₂ = Y ×_S W, Z₃ = X ×_S W.
Carried as data rather than constructed. Over S does have binary products
when Scheme has pullbacks, and it does, but nothing makes the resulting
objects locally Noetherian — which Dᵇ(Coh) requires — so a caller supplies
the objects together with that hypothesis anyway.
Not asserted: that any of these objects is a product. Nothing in this file
consumes it. What consumes it is a caller discharging the seven input classes
of geometricCompIso, whose instances are exactly where the product geometry
lives; see their docstrings.
- triple : Families.SchemeBaseChange S
The triple product
X ×_S Y ×_S W. Projection to
X ×_S Y.Projection to
Y ×_S W.Projection to
X ×_S W, along which the convolution is pushed.
Instances For
The convolution of two kernels — a definition, not supplied data.
conv P Q = Rπ_{XW*}(π_{XY}^* P ⊗^L π_{YW}^* Q), the classical formula, built
from functors the first ledger already names. This is the field that
ConvolutionData asks for as data and that this ledger removes from the
obligation list.
The kernel π_{YW}^* Q sits in the first slot of the tensor bifunctor, with
π_{XY}^* P as the argument. That choice is aligned with
Correspondence.transform, which pins its kernel to the first slot; keeping
the two conventions aligned is what lets geometricCompIso avoid asking for a
braiding. Flip either one and a braiding becomes a genuine eighth input.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The projection formula, supplied.
Rq_*(Lq^* B ⊗^L A) ≅ B ⊗^L Rq_* A in the twist-by-Lq^* B reading: the
twist by a pulled-back kernel commutes with pushforward.
One of the seven inputs to geometricCompIso, consumed there at the morphism
πYW of the triple product. Discharging it for a projection of an honest
fibre product is the classical projection formula; for an arbitrary morphism
it is generally false, which is where the product geometry lives in this
input.
- iso (B : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left U)) : ((derivedTensor Z).obj ((Families.SchemeBaseChange.boundedCoherentDerivedPullback q).obj B)).comp (derivedPushforward q) ≅ (derivedPushforward q).comp ((derivedTensor U).obj B)
The projection isomorphism, natural in both arguments.
Instances
Flat base change, supplied.
For a cartesian square with u, v the two sides and q, q' the two
projections, Lv^* Rq_* ≅ Rq'_* Lu^*.
One of the seven inputs to geometricCompIso, consumed there at the square
(q₁, πYW, πXY, p₂). That square is cartesian because the objects are
products — the place where productness does work in this input. Stated
abstractly on a supplied square so that the class does not itself have to
assert productness.
- iso : (derivedPushforward q).comp (Families.SchemeBaseChange.boundedCoherentDerivedPullback v) ≅ (Families.SchemeBaseChange.boundedCoherentDerivedPullback u).comp (derivedPushforward q')
Base-change isomorphism.
Instances
Compatibility record containing only the tensorator of derived pullback.
New stable convolution APIs require HasMonoidalDerivedPullback, which also
states tensorator associativity, unitality, naturality, and invertibility.
- iso (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left U)) : ((derivedTensor U).obj K).comp (Families.SchemeBaseChange.boundedCoherentDerivedPullback f) ≅ (Families.SchemeBaseChange.boundedCoherentDerivedPullback f).comp ((derivedTensor T).obj ((Families.SchemeBaseChange.boundedCoherentDerivedPullback f).obj K))
Pullback carries a twist to the twist by the pullback.
Instances
Forget strong monoidality to the old tensorator-only capability.
Compatibility record for callers that have only a chosen tensor
associator. New stable convolution APIs require HasCoherentDerivedTensor,
whose Mathlib MonoidalCategory parent also supplies naturality, the pentagon,
and the triangle.
Braiding is genuinely not needed, and that is a fact about this repository's
conventions rather than a general one: Correspondence.transform pins the
kernel to the first slot of the bifunctor, and convKernel puts
πYW^* Q in that same slot with πXY^* P as the argument. Flipping either
convention would force a braiding.
- iso (A B : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) : ((derivedTensor Z).obj B).comp ((derivedTensor Z).obj A) ≅ (derivedTensor Z).obj (((derivedTensor Z).obj A).obj B)
A ⊗ (B ⊗ −) ≅ (A ⊗ B) ⊗ −.
Instances
Forget the coherent root to the old single-associator capability.
This adapter is retained for raw intermediate consumers. There is deliberately no instance in the opposite direction.
The projection formula on the other slot, Rq_*(Lq^* E ⊗^L A) ≅ Rq_* A-twisted:
as a functor in E, Lq^* ⋙ (A ⊗ −) ⋙ Rq_* ≅ (Rq_* A) ⊗ −.
A separate class from HasProjectionFormula, deliberately. The derivation
consumes the two at different morphisms — this one at πXW, that one at
πYW — so merging them into one class with two fields would leave one field
unconsumed at each of the two instances.
It is also not a consequence of HasProjectionFormula plus a braiding: that
one is a family in the target variable natural in the source, this one a family
in the source variable natural in the target.
- iso (A : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) : (Families.SchemeBaseChange.boundedCoherentDerivedPullback q).comp (((derivedTensor Z).obj A).comp (derivedPushforward q)) ≅ (derivedTensor U).obj ((derivedPushforward q).obj A)
The right-slot projection isomorphism.
Instances
Two pullback routes to the same place agree.
Bundles functoriality of derived pullback with the commuting triangle
π₁ ≫ p₁ = π₃ ≫ p₃, because the derivation needs exactly the composite and
never the two halves separately.
Not reducible to boundedCoherentDerivedPullbackComp: that is stated at the
literal f ≫ g, so bridging two different composites would need eqToHom
transport across compound terms.
The triangle commutes. A guard: it is what makes the isomorphism below the right thing to ask for, and it is deliberately not consumed by the derivation, which uses
isoalone.- iso : (Families.SchemeBaseChange.boundedCoherentDerivedPullback p₁).comp (Families.SchemeBaseChange.boundedCoherentDerivedPullback π₁) ≅ (Families.SchemeBaseChange.boundedCoherentDerivedPullback p₃).comp (Families.SchemeBaseChange.boundedCoherentDerivedPullback π₃)
The two pullback routes agree.
Instances
Two pushforward routes to the same place agree.
The pushforward companion of HasCommonPullbackRoute, and unlike it there is
no existing composition contract at all — nothing in the repository names
R(g ∘ f)_* ≅ Rf_* ⋙ Rg_*.
The triangle commutes. A guard, as above.
- iso : (derivedPushforward π₂).comp (derivedPushforward q₂) ≅ (derivedPushforward π₃).comp (derivedPushforward q₃)
The two pushforward routes agree.
Instances
Deriving Prop. 5.10 #
compIso is no longer supplied. geometricCompIso below is the classical
argument, written as eight intermediate functors E₀, …, E₇ and eight steps,
each naming the single input it consumes:
| step | rewrites | input |
|---|---|---|
| 1 | q₁_* ⋙ p₂^* → πXY^* ⋙ πYW_* | HasFlatBaseChange |
| 2 | (⊗P) ⋙ πXY^* → πXY^* ⋙ (⊗πXY^*P) | HasMonoidalDerivedPullback |
| 3 | πYW_* ⋙ (⊗Q) → (⊗πYW^*Q) ⋙ πYW_* | HasProjectionFormula (symm) |
| 4 | (⊗a) ⋙ (⊗b) → (⊗(b ⊗ a)) | HasCoherentDerivedTensor |
| 5 | πYW_* ⋙ q₂_* → πXW_* ⋙ q₃_* | HasCommonPushforwardRoute |
| 6 | p₁^* ⋙ πXY^* → p₃^* ⋙ πXW^* | HasCommonPullbackRoute |
| 7 | πXW^* ⋙ (⊗M) ⋙ πXW_* → (⊗ Rπ_{XW*} M) | HasProjectionFormulaRight |
Every intermediate and every step is written with a fully ascribed type,
inside a single definition, so that no signature is left to section-variable
inclusion order and no composite is left to higher-order unification — the
two failure modes that consumed the first attempt at this proof. Mathlib's
own note on Functor.associator warns that leaning on the definitional
Functor.assoc "tends to make Lean slow"; the three private combinators
below spell the associators out once each.
Naturality. Every intermediate is a functor Dᵇ(Coh X) ⥤ Dᵇ(Coh W) and
every step is an isomorphism of such functors, so naturality in the
argument object is free and never checked by hand. Naturality in P or Q
is neither obtained nor claimed: ConvolutionData.compIso is a bare family
and every consumer evaluates it at a point, so asserting more would be an
unconsumed strengthening.
Prop. 5.10, derived: Φ_P ⋙ Φ_Q ≅ Φ_{Q ∗ P} for the geometric
correspondences, with Q ∗ P = convKernel G P Q.
Natural in the argument object (each side is a functor and the isomorphism is
an isomorphism of functors); a bare family in P and Q, which is exactly
what ConvolutionData.compIso consumes.
The seven instance arguments beyond the first ledger's are the seven classical inputs; see the section docstring for which step consumes which. Nothing constructs any of them, so this derivation moves the trust boundary — from "Prop. 5.10 holds" to the seven standard isomorphisms it classically follows from — without shrinking it to zero.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The geometric convolution data, assembled — with no supplied fields.
A ConvolutionData for the three geometric correspondences, with conv the
constructed convKernel and compIso the derived geometricCompIso.
Compare the abstract structure, which asks for both as data; that reduction —
from two supplied fields to zero, given the seven named classical inputs — is
the whole content of this ledger.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What the two ledgers together leave #
For a geometric Fourier--Mukai theory with composition, a caller must supply:
HasDerivedTensoron each of the four relevant schemes — absent from the repository;HasDerivedPushforwardalong each of the five relevant morphisms — absent from the repository, and where properness lives;HasCoherentPullbackalong each pullback used — an existing contract from #460--462, so no new kind of obligation;- a
TripleProductGeometry— the objects and projections; - the classical comparison structures:
HasProjectionFormula,HasProjectionFormulaRight,HasFlatBaseChange,HasMonoidalDerivedPullback,HasCoherentDerivedTensor,HasCommonPullbackRoute,HasCommonPushforwardRoute— where the product structure of theTripleProductGeometryfinally does its work.
Prop. 5.10 itself is no longer on the list: geometricCompIso derives it from
item 5. Everything else in the Fourier--Mukai lane follows: transform,
transformK₀, closure of kernel functors under composition, the transport of
stability conditions, and — with a KernelAutoequivalence and a DualKernel
on top — the group action and the Mukai isometry.
Still unreachable geometrically, and not addressed by either ledger:
UnitKernelData (needs 𝒪_Δ), DualKernel (needs P^∨ ⊗ p^*ω[dim]), and
associativity of convolution (needs a second comparison layer).