Symmetric powers commute with pullback of quasicoherent sheaves

For every morphism of schemes f : X ⟶ Y and every quasicoherent 𝒪_Y-module M, the canonical comparison f^* (Symⁿ M) ⟶ Symⁿ (f^* M) (Scheme.Modules.pullbackSymmetricPowerComparison) is an isomorphism. There are no flatness, finiteness or characteristic hypotheses.

The three inputs of the local criterion TauCeti.AlgebraicGeometry.isIso_pullbackComparison_app_of_isQuasicoherent are the composition coherence TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_comp, invertibility along open immersions for every sheaf of modules (TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app_of_isOpenImmersion, in TauCeti.AlgebraicGeometry.Modules.SymmetricPower.Restriction), and invertibility on quasicoherent modules between affine spectra, where the comparison is the scalar-extension isomorphism (TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_of_spec).

Main declaration

• TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app: the comparison along an arbitrary morphism is invertible on every quasicoherent sheaf.

References

• R. Hartshorne, Algebraic Geometry, Exercise II.5.16.

instance TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (n : ℕ) (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] : CategoryTheory.IsIso ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison f n).app M)

Symmetric powers commute with pullback of quasicoherent sheaves: for every morphism of schemes f : X ⟶ Y and every quasicoherent 𝒪_Y-module M, the canonical comparison f^* (Symⁿ M) ⟶ Symⁿ (f^* M) is an isomorphism.