The unit kernel 𝒪_Δ: the third ledger

Symmetry/Autoequivalence/FourierMukai.lean defines UnitKernelData — a kernel presenting the identity functor as a transform — and until now nothing geometric could discharge it: the classical unit kernel is 𝒪_Δ = Rδ_* 𝒪_X along the diagonal δ : X ⟶ X ×_S X, and neither 𝒪_X nor anything about δ was named.

This file is the ledger for it, in the same shape as the two kernel ledgers:

• diagonalKernel is a definition — Rδ_* applied to the tensor unit — built from functors the first ledger already names plus the coherent derived-tensor root (HasCoherentDerivedTensor).
• geometricUnitIso, the statement that its transform is the identity, is derived from four inputs: the right-slot projection formula at δ (an existing class, consumed here at a second site), the coherent left unitor, and the two retraction classes below.
• geometricUnitKernelData assembles a genuine UnitKernelData (geometricCorrespondence X X Z p q) from exactly those inputs and no others.

Where the diagonal geometry lives

Classically every input below is a theorem about the diagonal of a product: δ ≫ p = 𝟙 = δ ≫ q are the defining triangle identities, pullback and pushforward along a retraction compose to the identity by functoriality, and − ⊗ 𝒪 is the identity because 𝒪 is the monoidal unit. The tensor unit and unitor now come from one structure whose triangle law is explicit. The two retraction classes carry their triangle identity as a comm guard — deliberately not consumed by the derivation, which uses iso alone; the guard is what makes iso the right thing to ask for.

What this file does not assert

• Nothing constructs an instance of any class here, and no scheme is shown to admit one. Inhabitant-free, like both kernel ledgers.

• Nothing identifies Z with X ×_S X or δ with an actual diagonal; the classes are stated at arbitrary morphisms with the guards making the intended instantiation precise.

• No DualKernel. The classical dual kernel is P^∨ ⊗ p^* ω_X [dim X], which needs derived duals and a dualizing complex — machinery with no substrate in this repository when this file was written.

  Half of that reason has since lapsed and the sentence is corrected rather than left standing: KernelAdjunction.lean now ledgers the three constituent adjunctions, and they are consumed — by FourierMukai.ConstituentRightAdjoints, and through it by KernelAutoequivalence.DualKernel.ofRightAdjointKernel. What remains true is the other half: nothing discharges those classes. A DualKernel is now reachable — KernelSwap.geometricDualKernel assembles one — but only from that whole uninhabited ledger plus a supplied equivalence, so this file's own inputs still do not produce one.

• This file alone does not prove the kernel is a unit for convolution; KernelUnitConvolution.lean derives those laws from additional section and base-change geometry.

class AlgebraicGeometry.DerivedCategory.FourierMukai.HasTensorUnit {S : Scheme} (T : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [HasDerivedTensor T] : Type (u + 1)

Compatibility record for a raw tensor bifunctor with a chosen left unit.

New stable unit and convolution APIs require HasCoherentDerivedTensor, where this unit and both unitors belong to the same monoidal structure as the associator, pentagon, and triangle.

• unit : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left T)

  The unit object, playing 𝒪_T.

• iso : (derivedTensor T).obj unit ≅ CategoryTheory.Functor.id (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left T))

  Twisting by the unit is the identity.

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.DerivedCategory.FourierMukai.hasTensorUnitOfCoherent {S : Scheme} (T : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [HasCoherentDerivedTensor T] : HasTensorUnit T

Forget the coherent root to the old selected-unit capability.

This supports raw intermediate callers without allowing a selected unit to synthesize monoidal coherence.

Equations

• One or more equations did not get rendered due to their size.

class AlgebraicGeometry.DerivedCategory.FourierMukai.HasPullbackRetraction {S : Scheme} {X Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left X)] [IsLocallyNoetherian (CategoryTheory.Over.left Z)] (δ : X ⟶ Z) (p : Z ⟶ X) [Families.SchemeBaseChange.HasCoherentPullback δ] [Families.SchemeBaseChange.HasCoherentPullback p] : Type (u + 1)

Derived pullback along a section collapses, supplied.

For a section-retraction pair δ ≫ p = 𝟙, the composite of the two derived pullbacks is the identity. The equation is a guard: the derivation consumes iso alone, and comm is what makes it the right isomorphism to ask for.

• comm : CategoryTheory.CategoryStruct.comp δ p = CategoryTheory.CategoryStruct.id X

  The triangle identity. A guard, not consumed.

• iso : (Families.SchemeBaseChange.boundedCoherentDerivedPullback p).comp (Families.SchemeBaseChange.boundedCoherentDerivedPullback δ) ≅ CategoryTheory.Functor.id (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X))

  Pullback along the retraction then the section is the identity.

class AlgebraicGeometry.DerivedCategory.FourierMukai.HasPushforwardRetraction {S : Scheme} {X Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left X)] [IsLocallyNoetherian (CategoryTheory.Over.left Z)] (δ : X ⟶ Z) (q : Z ⟶ X) [HasDerivedPushforward δ] [HasDerivedPushforward q] : Type (u + 1)

Derived pushforward along a section collapses, supplied.

The pushforward companion: for δ ≫ q = 𝟙, pushing forward along the section and then the retraction is the identity. Guard as above.

• comm : CategoryTheory.CategoryStruct.comp δ q = CategoryTheory.CategoryStruct.id X

  The triangle identity. A guard, not consumed.

• iso : (derivedPushforward δ).comp (derivedPushforward q) ≅ CategoryTheory.Functor.id (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X))

  Pushforward along the section then the retraction is the identity.

noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.diagonalKernel {S : Scheme} {X Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left X)] [IsLocallyNoetherian (CategoryTheory.Over.left Z)] (δ : X ⟶ Z) [HasDerivedPushforward δ] [HasCoherentDerivedTensor X] : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)

The unit kernel, 𝒪_Δ — a definition, not supplied data.

Rδ_* applied to the tensor unit. The classical 𝒪_Δ, built from functors the ledgers already name.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.geometricUnitIso {S : Scheme} {X Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left X)] [IsLocallyNoetherian (CategoryTheory.Over.left Z)] (p q : Z ⟶ X) (δ : X ⟶ Z) [Families.SchemeBaseChange.HasCoherentPullback p] [Families.SchemeBaseChange.HasCoherentPullback δ] [HasDerivedTensor Z] [HasCoherentDerivedTensor X] [HasDerivedPushforward q] [HasDerivedPushforward δ] [HasProjectionFormulaRight δ] [HasPullbackRetraction δ p] [HasPushforwardRetraction δ q] : CategoryTheory.Functor.id (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left X)) ≅ (geometricCorrespondence X X Z p q).transform (diagonalKernel δ)

The transform of the unit kernel is the identity — derived.

The chain is the classical argument, four steps, each naming its input:

step	rewrites	input
1	(⊗ 𝒪_Δ) → δ^* ⋙ (⊗𝒪) ⋙ δ_*	HasProjectionFormulaRight at δ
2	(⊗𝒪) deleted	HasCoherentDerivedTensor left unitor
3	δ_* ⋙ q_* deleted	HasPushforwardRetraction
4	p^* ⋙ δ^* → 𝟭	HasPullbackRetraction

Written in the same style as geometricCompIso: every intermediate functor and every step is let-bound with a fully ascribed type.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.geometricUnitKernelData {S : Scheme} {X Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left X)] [IsLocallyNoetherian (CategoryTheory.Over.left Z)] (p q : Z ⟶ X) (δ : X ⟶ Z) [Families.SchemeBaseChange.HasCoherentPullback p] [Families.SchemeBaseChange.HasCoherentPullback δ] [HasDerivedTensor Z] [HasCoherentDerivedTensor X] [HasDerivedPushforward q] [HasDerivedPushforward δ] [HasProjectionFormulaRight δ] [HasPullbackRetraction δ p] [HasPushforwardRetraction δ q] : CategoryTheory.Triangulated.FourierMukai.UnitKernelData (geometricCorrespondence X X Z p q)

The geometric unit kernel data, assembled — with no supplied fields.

A UnitKernelData for the geometric correspondence of X with itself, with unitKernel the constructed diagonalKernel and unitIso the derived geometricUnitIso. Together with KernelAutoequivalence.id this makes the identity a kernel autoequivalence, geometrically, conditional on the four named inputs.

Equations

• One or more equations did not get rendered due to their size.

What the three ledgers together leave

The unit side of the autoequivalence story is now: a caller who discharges the first ledger's contracts at p, q, δ plus HasProjectionFormulaRight at δ, HasCoherentDerivedTensor, and the two retraction classes gets KernelAutoequivalence.id with a geometric kernel. Still absent, and named absences rather than ledgers: DualKernel (needs derived duals and a dualizing complex) and the unit's compatibility with convolution (needs ConvolutionData for the self-correspondence and a comparison of convKernel with diagonalKernel).