The canonical symmetric-power comparison on affine spectra

For an arbitrary ring map φ : R ⟶ S, the canonical comparison (Spec φ)^* (Symⁿ M) ⟶ Symⁿ ((Spec φ)^* M) is invertible for every quasicoherent module sheaf M on Spec R. There are no flatness, finite-presentation or local-freeness hypotheses, and no assumption on the characteristic.

The comparison is the mate of the pushforward map on sheafified symmetric tensors, not a separately chosen isomorphism. Under the affine identifications tildeSymmetricPowerIso and tildeFunctorCompPullbackIso it becomes the scalar-extension isomorphism S ⊗_R Symⁿ M ≅ Symⁿ (S ⊗_R M) of RingHom.extendScalarsSymmetricPowerIso (pullback_tildeSymmetricPowerIso_hom). The identification is checked on monomials, through the pullback and tilde adjunctions. This is the affine computation needed to check invertibility of the canonical comparison locally on schemes.

Main declarations

• TauCeti.AlgebraicGeometry.pullback_tildeSymmetricPowerIso_hom: the canonical comparison on an associated sheaf is the scalar-extension isomorphism, and TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_tilde solves for it;
• TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_of_spec: it is invertible on every quasicoherent sheaf on Spec R.

References

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

theorem TauCeti.AlgebraicGeometry.pullback_tildeSymmetricPowerIso_hom {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : ModuleCat ↑R) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).map (tildeSymmetricPowerIso n M).hom) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison (AlgebraicGeometry.Spec.map φ) n).app (AlgebraicGeometry.tilde M)) ((SheafOfModules.symmetricPower (AlgebraicGeometry.Spec S).sheaf n).map ((tildeFunctorCompPullbackIso φ).hom.app M))) = CategoryTheory.CategoryStruct.comp ((tildeFunctorCompPullbackIso φ).hom.app (M.symmetricPower n)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map ((CommRingCat.Hom.hom φ).extendScalarsSymmetricPowerIso n M).hom) (tildeSymmetricPowerIso n ((ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).obj M)).hom)

Under the affine identifications tildeSymmetricPowerIso and tildeFunctorCompPullbackIso, the canonical symmetric-power pullback comparison along Spec φ is the scalar-extension isomorphism S ⊗_R Symⁿ M ≅ Symⁿ (S ⊗_R M).

theorem TauCeti.AlgebraicGeometry.pullback_tildeSymmetricPowerIso_hom_assoc {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : ModuleCat ↑R) {Z : (AlgebraicGeometry.Spec S).Modules} (h : (SheafOfModules.symmetricPower (AlgebraicGeometry.Spec S).sheaf n).obj ((AlgebraicGeometry.tilde.functor S).obj ((ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).obj M)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).map (tildeSymmetricPowerIso n M).hom) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison (AlgebraicGeometry.Spec.map φ) n).app (AlgebraicGeometry.tilde M)) ((SheafOfModules.symmetricPower (AlgebraicGeometry.Spec S).sheaf n).map ((tildeFunctorCompPullbackIso φ).hom.app M)))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((tildeFunctorCompPullbackIso φ).hom.app (M.symmetricPower n)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map ((CommRingCat.Hom.hom φ).extendScalarsSymmetricPowerIso n M).hom) (tildeSymmetricPowerIso n ((ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).obj M)).hom)) h

Under the affine identifications tildeSymmetricPowerIso and tildeFunctorCompPullbackIso, the canonical symmetric-power pullback comparison along Spec φ is the scalar-extension isomorphism S ⊗_R Symⁿ M ≅ Symⁿ (S ⊗_R M).

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_tilde {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : ModuleCat ↑R) : (AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison (AlgebraicGeometry.Spec.map φ) n).app (AlgebraicGeometry.tilde M) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).map (tildeSymmetricPowerIso n M).inv) (CategoryTheory.CategoryStruct.comp ((tildeFunctorCompPullbackIso φ).hom.app (M.symmetricPower n)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map ((CommRingCat.Hom.hom φ).extendScalarsSymmetricPowerIso n M).hom) (CategoryTheory.CategoryStruct.comp (tildeSymmetricPowerIso n ((ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).obj M)).hom ((SheafOfModules.symmetricPower (AlgebraicGeometry.Spec S).sheaf n).map ((tildeFunctorCompPullbackIso φ).inv.app M)))))

The canonical symmetric-power pullback map on an associated sheaf is the composite of the affine comparisons with the scalar-extension isomorphism.

instance TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_of_spec {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent M] : CategoryTheory.IsIso ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison (AlgebraicGeometry.Spec.map φ) n).app M)

The canonical symmetric-power pullback comparison is invertible for every quasicoherent sheaf on an affine spectrum and every ring map, including nonflat maps.