Exterior 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^* (⋀ⁿ M) ⟶ ⋀ⁿ (f^* M) (Scheme.Modules.pullbackExteriorPowerComparison) 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.pullbackExteriorPowerComparison_comp, invertibility along open immersions for every sheaf of modules (TauCeti.AlgebraicGeometry.isIso_pullbackExteriorPowerComparison_app_of_isOpenImmersion, in TauCeti.AlgebraicGeometry.Modules.ExteriorPower.Restriction), and invertibility on quasicoherent modules between affine spectra, where the comparison is the scalar-extension isomorphism (TauCeti.AlgebraicGeometry.isIso_pullbackExteriorPowerComparison_of_spec).

Main declaration

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

References

• R. Hartshorne, Algebraic Geometry, Exercise II.5.16.
• The Stacks Project, Lemma 10.13.6 (Tag 0C6F).

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

Exterior 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^* (⋀ⁿ M) ⟶ ⋀ⁿ (f^* M) is an isomorphism.