The dualizing twist, and a geometric adjoint kernel #
KernelAdjunction.lean produces a ConstituentRightAdjoints for the geometric
correspondence, so the geometric transform is left adjoint to the composite
q^! ⋙ (− ⊗ K^∨) ⋙ Rp_*.
It stops there, deliberately: nothing said that composite is again a
transform, and HasTwistedInversePullback was kept opaque about the shape of
q^! precisely so the two obligations would stay apart.
This file supplies the missing shape and closes the gap. One new class says
q^! is a twisted pullback; the tensor associator — from the existing coherent
tensor root — collects the two twists into one; and the
composite becomes the transform of the reversed correspondence with the
classical kernel
Q = K^∨ ⊗ ω_q.
The one new contract #
HasDualizingTwist q supplies an object ω_q and
q^! ≅ Lq^*(−) ⊗ ω_q. Two things about its shape are deliberate.
No shift index. Classically the twist is ω_q[dim q]. The relative
dimension appears nowhere here, because nothing consumes it: ω_q is asked for
as the object already carrying whatever shift it carries. Asking for a
dimension and a shift separately would add a hypothesis the derivation never
uses, which is the shape this lane's reviews have attacked twice.
A new contract at q. The class needs HasCoherentPullback q — pullback
along the pushforward's morphism — which geometricCorrespondence never asks
for. That is the mirror of KernelAdjunction.lean needing
HasDerivedPushforward p, and it is not an accident: the two extra contracts
are exactly what makes the reversed correspondence
geometricCorrespondence Y X Z q p expressible, and the adjoint kernel lives
there.
What comes out #
geometricRightAdjointKernelData is a genuine
FourierMukai.RightAdjointKernelData for the geometric correspondence, with
the reversed correspondence as its opposite and Q = K^∨ ⊗ ω_q as its kernel.
Everything #768 proves about a right adjoint kernel then applies: uniqueness of
the adjoint, that the adjoint is itself a kernel functor, and the transport
lemmas.
What does not come out, and why #
Not a DualKernel, and not for want of one more isomorphism.
KernelAutoequivalence.DualKernel asks for the quasi-inverse to be a transform
of the same correspondence — its field is
A.equiv.inverse ≅ A.corr.transform dual, one corr. What this file produces
is a transform of the reversed correspondence
geometricCorrespondence X X Z q p, and for p ≠ q that is a different
Correspondence value even when both endpoints are X.
So DualKernel.ofRightAdjointKernel does not apply here, and nothing in this
file pretends otherwise. Bridging the two needs an identification of the two
correspondences' transforms — classically pullback along the swap
σ : X × X → X × X. That is a further ledger, named in the closing section;
KernelSwap.lean is it, and it lands Rσ_* Q rather than σ^* Q — the two
agree for an involution isomorphism, which that file does not need to assume.
What this file does not assert #
- Nothing constructs a
HasDualizingTwist, and no morphism is shown to admit one. Inhabitant-free, like every ledger it builds on. - Nothing identifies
ω_qwith a relative dualizing complex, a canonical bundle, or a shift of either; it is an object with one stated property. - No Serre duality, no smoothness, no properness, no relative dimension.
- Nothing relates
HasDualizingTwist qtoHasDualizingTwist p, and no compatibility between the two directions is stated. - No claim that any geometric transform is an equivalence.
The twisted inverse image is a twisted pullback, supplied.
The shape HasTwistedInversePullback refuses to assume: f^!(−) ≅ Lf^*(−) ⊗ ω_f.
Classically this holds for f smooth and proper with ω_f the relative
dualizing complex placed in degree −dim f, and a caller discharging this class
is asserting exactly that much.
The shift is folded into dualizingTwist rather than carried separately,
because no consumer here uses a relative dimension.
- dualizingTwist : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left T)
The dualizing object, in the role of
ω_f[dim f]. - iso : twistedInversePullback f ≅ (Families.SchemeBaseChange.boundedCoherentDerivedPullback f).comp ((derivedTensor T).obj (dualizingTwist f))
f^!is pullback followed by the twist.
Instances
The dualizing object, named.
Equations
Instances For
The decomposition of f^!, named.
Equations
Instances For
The adjoint kernel, constructed.
Q = K^∨ ⊗ ω_q — the classical dual kernel, with the twist that
p^* ω_X [dim X] contributes in the smooth projective case here carried
wholesale by ω_q.
This is a def with a value, not a supplied field: both factors come from
classes already on the table. Written with explicit binders rather than from
the assembly section's variable block, because it depends on neither p nor
X and should not silently acquire them.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The composite right adjoint is the reversed transform.
The whole content of this file. Reading the composite
q^! ⋙ (− ⊗ K^∨) ⋙ Rp_* left to right: replace q^! by Lq^* ⋙ (− ⊗ ω_q),
then collect the two adjacent twists with the tensor associator. What is left
is Lq^* ⋙ (− ⊗ Q) ⋙ Rp_*, which is exactly the transform of the reversed
correspondence.
The associator is coherentDerivedTensorAssoc, from the existing
HasCoherentDerivedTensor root, consumed here at a further site. The root
rather than the legacy associator-only class: scripts/check_coherent_families.py
requires it, and it also removes a diamond — HasCoherentDerivedTensor supplies
HasDerivedTensor through hasDerivedTensorOfCoherent, so the correspondence,
the kernel dual and the associator all read the same tensor instance.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A geometric right adjoint kernel.
The payoff: a genuine RightAdjointKernelData for the geometric
correspondence, whose opposite is the reversed correspondence and whose kernel
is the constructed K^∨ ⊗ ω_q. Everything FourierMukai/Adjunction.lean
proves about a right adjoint kernel now applies geometrically, conditional on
the ledger.
It is not a DualKernel: that needs the opposite correspondence to be the
same one, and this one is reversed. See the module docstring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The composite adjoint is a kernel functor for the reversed correspondence.
RightAdjointKernelData.isKernelFunctor_of_adj at the assembled datum. Stated
because "the adjoint exists" and "the adjoint is again of Fourier--Mukai type"
are different claims, and the second is the one the lane is about.
The next ledger, and what is in it #
What stands between this file and a geometric DualKernel is not another
adjunction. It is that DualKernel asks for the quasi-inverse as a transform
of the same correspondence, while an adjoint is naturally a transform of
the reversed one.
Closing that needs, for an endocorrespondence X = Y:
- the swap
σ : Z ⟶ ZoverX × X, withσ ≫ p = qandσ ≫ q = p; - pullback along it, and the identification
(geometricCorrespondence X X Z q p).transform Q ≅ (geometricCorrespondence X X Z p q).transform (σ^* Q); - and only then, given a supplied
KernelAutoequivalenceon that correspondence,DualKernel.ofRightAdjointKernelapplies and the dual kernel isRσ_*(K^∨ ⊗ ω_q)— the classicalP^∨ ⊗ p^* ω_X [dim X].
None of that is stated here; KernelSwap.lean states it. Note that all three
bullets are about the product's symmetry, not about duality: the duality half
of the classical statement is finished once HasDualizingTwist is discharged.