The swap of an endocorrespondence, and a geometric dual kernel #

KernelDualizingTwist.lean produces a RightAdjointKernelData whose opposite is the reversed correspondence geometricCorrespondence X X Z q p. KernelAutoequivalence.DualKernel needs the same correspondence on both sides, and for p ≠ q those are different values. That mismatch — not any remaining duality — is all that stood between the previous file and a dual kernel.

This file closes it. Classically Z = X × X and the missing ingredient is the swap σ exchanging the two factors, under which the reversed correspondence becomes the original one and the kernel is carried along.

The derivation, and why the kernel is `Rσ_Q` rather than `σ^Q` #

With q = σ ≫ p and p = σ ≫ q, pullback is contravariant and pushforward covariant, so Lq^* ≅ Lp^* ⋙ Lσ^* and Rp_* ≅ Rσ_* ⋙ Rq_*. Substituting both into the reversed transform leaves

Lp^* ⋙ [ Lσ^* ⋙ (Q ⊗ −) ⋙ Rσ_* ] ⋙ Rq_*

and the bracket is exactly the right-slot projection formula at σ, which collapses it to (Rσ_* Q) ⊗ −. So the transported kernel is Rσ_* Q.

The classical statement uses σ^* Q, and the two agree because σ is an involution isomorphism. That hypothesis is not assumed here: nothing in the derivation needs σ invertible, and asking for it would be an unconsumed hypothesis. Rσ_* is what the projection formula hands back, so Rσ_* is what the kernel is written with.

The three inputs #

HasPullbackSwap σ p q — Lq^* ≅ Lp^* ⋙ Lσ^*, with σ ≫ p = q as a guard;
HasPushforwardSwap σ p q — Rp_* ≅ Rσ_* ⋙ Rq_*, with σ ≫ q = p as a guard;
HasProjectionFormulaRight σ — an existing class, consumed here at a further site.

The guards follow HasPullbackRetraction and HasPushforwardRetraction: the composition identity is carried but not consumed, and the iso field is what the derivation uses. The guard is what makes iso the right thing to ask for.

Neither swap class is reduced to boundedCoherentDerivedPullbackComp, for the reason KernelConvolution.lean already gives about a different pair: that isomorphism is stated at the literal f ≫ g, so bridging it to q would need eqToHom transport across compound terms.

What comes out #

geometricDualAdjointKernelData is a RightAdjointKernelData for the geometric correspondence against itself, so DualKernel.ofRightAdjointKernel applies. geometricDualKernel is the result: a DualKernel for a kernel autoequivalence built on the geometric correspondence, with dual kernel

Rσ_*(K^∨ ⊗ ω_q)

— the classical P^∨ ⊗ p^*ω_X[dim X], assembled entirely from named contracts.

What this file does not assert #

Nothing constructs a HasPullbackSwap or a HasPushforwardSwap, and no morphism is shown to admit one. Inhabitant-free, like every ledger below it.
Nothing identifies Z with X × X or σ with an actual factor exchange; the classes are stated at an arbitrary σ : Z ⟶ Z with the guards making the intended instantiation precise.
σ is not assumed invertible, an involution, or an isomorphism, and Rσ_* ≅ σ^* is not claimed.
No criterion for the equivalence. geometricKernelAutoequivalence takes the equivalence and its comparison isomorphism as arguments. geometricKernelAutoequivalenceOfAdjoint does not — it derives both from the invertibility of one adjunction's unit and counit — but that invertibility is itself assumed, and nothing here establishes it. Classically it is the Bondal--Orlov criterion, which needs geometry this repository does not have. So a transform is still never shown to be an equivalence; what changed is only the shape of the assumption.
No Serre duality, no smoothness, no properness, no relative dimension.

The swap of an endocorrespondence, and a geometric dual kernel #

The derivation, and why the kernel is Rσ_*Q rather than σ^*Q #

The three inputs #

What comes out #

What this file does not assert #

The equivalence, no longer supplied #

The derivation, and why the kernel is `Rσ_Q` rather than `σ^Q` #