Symmetric 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 Symⁿ Γ(M,U) to Symⁿ Γ(M,D(f)) is localization at the powers of f. The symmetric powers use the respective rings of regular functions, and the map is the actual restriction of PresheafOfModulesOfCommRing.symmetricPower.

This computes the sectionwise symmetric-power presheaf on an affine basis. It does not identify the symmetric power of sections with sections of the sheafified symmetric power on arbitrary opens. The computation supplies the localization compatibility used in that affine comparison.

References

• R. Hartshorne, Algebraic Geometry, Lemma II.5.3.

theorem AlgebraicGeometry.Scheme.Modules.isLocalizedModule_symmetricPower_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.symmetricPower n).obj M.val).map (CategoryTheory.homOfLE ⋯).op))

On the basic opens of an affine open, the restriction in the sectionwise symmetric-power presheaf of a quasicoherent module is localization at the defining function. This holds in every degree, without any freeness or finiteness assumption on the module.