Restriction of symmetric powers on schemes

Symmetric powers of module sheaves commute with restriction along every open immersion. The comparison is the canonical pushforward comparison for the functor sending an open to its image; its coefficient map is the inverse of the structure-sheaf isomorphism on that open. No quasicoherence hypothesis is required. The unit of the restriction--pushforward adjunction is compatible with this comparison and with the pushforward comparison (Scheme.Modules.restrictAdjunction_unit_app_symmetricPower).

Consequently, along an open immersion j the canonical pullback comparison j^* (Symⁿ M) ⟶ Symⁿ (j^* M) is the inverse of the restriction isomorphism, read through the identification of restriction with pullback (TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_app_of_isOpenImmersion), and so it is invertible for every sheaf of modules (TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app_of_isOpenImmersion).

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictSymmetricPowerIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (n : ℕ) : (restrictFunctor f).comp (SheafOfModules.symmetricPower X.sheaf n) ≅ (SheafOfModules.symmetricPower Y.sheaf n).comp (restrictFunctor f)

Symmetric powers commute with restriction along an open immersion, naturally in the module sheaf. The forward map is the canonical symmetric-power pushforward comparison.

theorem AlgebraicGeometry.Scheme.Modules.restrictSymmetricPowerIso_hom_app {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (n : ℕ) (M : Y.Modules) : (restrictSymmetricPowerIso f n).hom.app M = (TauCeti.SheafOfModules.pushforwardSymmetricPowerComparison (restrictRingCatSheafHom f) n).app M

The forward restriction isomorphism is the canonical pushforward comparison.

theorem AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_symmetricPower {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (n : ℕ) (M : Y.Modules) : (restrictAdjunction f).unit.app ((SheafOfModules.symmetricPower Y.sheaf n).obj M) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower Y.sheaf n).map ((restrictAdjunction f).unit.app M)) (CategoryTheory.CategoryStruct.comp ((TauCeti.SheafOfModules.pushforwardSymmetricPowerComparison (Hom.toRingCatSheafHom f) n).app (M.restrict f)) ((pushforward f).map ((restrictSymmetricPowerIso f n).hom.app M)))

The unit M ⟶ f_* (M|_X) of the restriction--pushforward adjunction along an open immersion is compatible with the symmetric-power comparisons of pushforward and restriction.

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_app_of_isOpenImmersion {U Y : AlgebraicGeometry.Scheme} (j : U ⟶ Y) [AlgebraicGeometry.IsOpenImmersion j] (n : ℕ) (M : Y.Modules) : (AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison j n).app M = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.restrictFunctorIsoPullback j).inv.app ((SheafOfModules.symmetricPower Y.sheaf n).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.restrictSymmetricPowerIso j n).inv.app M) ((SheafOfModules.symmetricPower U.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.restrictFunctorIsoPullback j).hom.app M)))

Along an open immersion j, the canonical comparison j^* (Symⁿ M) ⟶ Symⁿ (j^* M) is the inverse of the restriction isomorphism Symⁿ (M|_U) ≅ (Symⁿ M)|_U, read through the identification Scheme.Modules.restrictFunctorIsoPullback of restriction with pullback.

instance TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app_of_isOpenImmersion {U Y : AlgebraicGeometry.Scheme} (j : U ⟶ Y) [AlgebraicGeometry.IsOpenImmersion j] (n : ℕ) (M : Y.Modules) : CategoryTheory.IsIso ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison j n).app M)

Along an open immersion the canonical symmetric-power comparison is invertible for every sheaf of modules.