Exterior powers of sections on basic affine opens

For a quasicoherent module M, an affine open U, and a regular function f on U, the restriction from ⋀ⁿ Γ(M,U) to ⋀ⁿ Γ(M,D(f)) is localization at the powers of f. Here the two exterior powers use the respective rings of regular functions. The restriction is the actual map of PresheafOfModulesOfCommRing.exteriorPower, which sends each wedge of sections to the wedge of their restrictions.

This is an affine-local computation of the sectionwise exterior-power presheaf. It does not identify sections of the sheafification with exterior powers of sections on arbitrary opens. The section localization Scheme.Modules.isLocalizedModule_basicOpenRestrict induces this comparison via LinearMap.isLocalizedModule_exteriorPower.

References

• The Stacks Project, Lemma 10.13.6.
• R. Hartshorne, Algebraic Geometry, Lemma II.5.3.

theorem AlgebraicGeometry.Scheme.Modules.isLocalizedModule_exteriorPower_map_basicOpen {X : Scheme} (M : X.Modules) {U : X.Opens} [SheafOfModules.IsQuasicoherent M] (hU : IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) (n : ℕ) : IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom (((PresheafOfModulesOfCommRing.exteriorPower n).obj M.val).map (CategoryTheory.homOfLE ⋯).op))

The actual sectionwise exterior-power restriction to a basic open of an affine open is localization at the powers of the defining function. No finiteness assumption on the quasicoherent module or flatness assumption on its sections is needed.