The projection formula for finite locally free sheaves

Let f : X ⟶ Y be a morphism of schemes and E a finite locally free sheaf on Y. The projection formula identifies, naturally in the sheaf of modules N on X,

E ⊗ f_* N ≅ f_* (f^* E ⊗ N).

No hypothesis on f is needed. Both sides are right adjoint functors of N: tensoring with E is right adjoint to tensoring with its dual E^∨, and tensoring with f^* E is right adjoint to tensoring with f^* E^∨, the dual of f^* E (TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDualIso). Their left adjoints T ↦ f^* (E^∨ ⊗ T) and T ↦ f^* E^∨ ⊗ f^* T agree because pullback commutes with tensoring by the quasi-coherent sheaf E^∨ (AlgebraicGeometry.Scheme.Modules.pullbackTensorLeftIso), so the right adjoints agree too.

For the closed subscheme ι : Z ⟶ X cut out by an ideal sheaf, the case N = 𝒪_Z identifies E ⊗ ι_* 𝒪_Z, the restriction of E to Z seen on X, with the direct image of the pullback ι^* E (TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.tensorPushforwardUnitIso).

References

• R. Hartshorne, Algebraic Geometry, Exercise II.5.1(d) (the projection formula for a locally free sheaf of finite rank).

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pushforwardTensorLeftIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FiniteLocallyFreeSheaf Y) : (AlgebraicGeometry.Scheme.Modules.pushforward f).comp (CategoryTheory.MonoidalCategory.tensorLeft E.obj) ≅ (CategoryTheory.MonoidalCategory.tensorLeft ((pullback f).obj E).obj).comp (AlgebraicGeometry.Scheme.Modules.pushforward f)

The projection formula. For a finite locally free sheaf E on Y and any morphism f : X ⟶ Y, tensoring a direct image with E is the direct image of the tensor product with f^* E: E ⊗ f_* N ≅ f_* (f^* E ⊗ N), naturally in the sheaf of modules N on X.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.tensorPushforwardUnitIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FiniteLocallyFreeSheaf Y) : CategoryTheory.MonoidalCategoryStruct.tensorObj E.obj ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)) ≅ (AlgebraicGeometry.Scheme.Modules.pushforward f).obj ((pullback f).obj E).obj

The projection formula for the direct image of the structure sheaf: E ⊗ f_* 𝒪_X ≅ f_* (f^* E). For a closed immersion f this identifies the restriction of E to the closed subscheme, seen on Y, with the direct image of the pullback of E.