Restriction of exterior powers on schemes

Exterior powers of module sheaves commute with restriction along every open immersion. The forward comparison sends a wedge of restricted sections to the restriction of their wedge. It is the canonical pushforward comparison for the functor sending an open to its image, with coefficient map the inverse structure-sheaf isomorphism. No quasicoherence, finiteness, or flatness hypothesis is required.

The natural isomorphism is TauCeti.AlgebraicGeometry.restrictExteriorPowerIso; TauCeti.AlgebraicGeometry.restrictExteriorPowerIso_hom_app identifies its forward map.

The unit of the restriction--pushforward adjunction is compatible with this comparison and with the pushforward comparison (TauCeti.AlgebraicGeometry.restrictAdjunction_unit_app_exteriorPower). Consequently, along an open immersion j the canonical pullback comparison j^* (⋀ⁿ M) ⟶ ⋀ⁿ (j^* M) is the inverse of the restriction isomorphism, read through the identification of restriction with pullback (TauCeti.AlgebraicGeometry.pullbackExteriorPowerComparison_app_of_isOpenImmersion), and so it is invertible for every sheaf of modules (TauCeti.AlgebraicGeometry.isIso_pullbackExteriorPowerComparison_app_of_isOpenImmersion).

References

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

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

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

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

The forward restriction isomorphism is the canonical pushforward comparison.

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

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

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

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

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

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