Pullback of exterior powers of modules on schemes

For a morphism of schemes f : X ⟶ Y, Scheme.Modules.pullbackExteriorPowerComparison f n is the canonical natural map f^* (⋀ⁿ M) ⟶ ⋀ⁿ (f^* M), the scheme case of TauCeti.SheafOfModules.pullbackExteriorPowerComparison. It is characterized by its transpose under the pullback--pushforward adjunction, and it is an isomorphism in degree one.

For a ring map φ : R ⟶ S, pullback along Spec φ commutes with exterior powers of the sheaf associated with any R-module. The comparison is natural in the module and does not require flatness, finite presentation, or local freeness. It combines the affine computation of exterior powers with the identification of pullback with extension of scalars.

This is the affine calculation used to descend exterior-power pullback comparisons on schemes. It includes finite projective modules and therefore the affine charts of finite locally free sheaves. The forward component is characterized as the composite of the existing affine comparisons and the scalar-extension map, whose value on a decomposable wedge is explicit in TauCeti.extendScalarsExteriorPowerIso_hom_tmul_mk.

References

• The Stacks Project, Lemma 10.13.6 (Tag 0C6F).
• R. Hartshorne, Algebraic Geometry, Proposition II.5.2 (e).

noncomputable def TauCeti.AlgebraicGeometry.tildePullbackExteriorPowerIso {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) : (AlgebraicGeometry.tilde.functor R).comp ((SheafOfModules.exteriorPower (AlgebraicGeometry.Spec R).sheaf n).comp (AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ))) ≅ (AlgebraicGeometry.tilde.functor R).comp ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).comp (SheafOfModules.exteriorPower (AlgebraicGeometry.Spec S).sheaf n))

Pullback along a morphism of affine spectra commutes with exterior powers of associated sheaves, naturally in the module, for any ring map.

@[simp]

theorem TauCeti.AlgebraicGeometry.tildePullbackExteriorPowerIso_hom_app {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : ModuleCat ↑R) : (tildePullbackExteriorPowerIso φ n).hom.app M = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).map (tildeExteriorPowerIso n M).inv) (CategoryTheory.CategoryStruct.comp ((tildeFunctorCompPullbackIso φ).hom.app (M.exteriorPower n)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map (extendScalarsExteriorPowerIso (CommRingCat.Hom.hom φ) n M).hom) (CategoryTheory.CategoryStruct.comp (tildeExteriorPowerIso n ((ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).obj M)).hom ((SheafOfModules.exteriorPower (AlgebraicGeometry.Spec S).sheaf n).map ((tildeFunctorCompPullbackIso φ).inv.app M)))))

The affine pullback comparison is the scalar-extension comparison transported through tildeExteriorPowerIso and tildeFunctorCompPullbackIso.

@[simp]

theorem TauCeti.AlgebraicGeometry.tildePullbackExteriorPowerIso_inv_app {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : ModuleCat ↑R) : (tildePullbackExteriorPowerIso φ n).inv.app M = CategoryTheory.CategoryStruct.comp ((SheafOfModules.exteriorPower (AlgebraicGeometry.Spec S).sheaf n).map ((tildeFunctorCompPullbackIso φ).hom.app M)) (CategoryTheory.CategoryStruct.comp (tildeExteriorPowerIso n ((ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).obj M)).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map (extendScalarsExteriorPowerIso (CommRingCat.Hom.hom φ) n M).inv) (CategoryTheory.CategoryStruct.comp ((tildeFunctorCompPullbackIso φ).inv.app (M.exteriorPower n)) ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).map (tildeExteriorPowerIso n M).hom))))

The inverse affine pullback comparison reverses the affine and scalar-extension comparisons.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison {X Y : Scheme} (f : X ⟶ Y) (n : ℕ) : (SheafOfModules.exteriorPower Y.sheaf n).comp (pullback f) ⟶ (pullback f).comp (SheafOfModules.exteriorPower X.sheaf n)

The canonical comparison f^* (⋀ⁿ M) ⟶ ⋀ⁿ (f^* M) for modules on schemes: TauCeti.SheafOfModules.pullbackExteriorPowerComparison along f.toRingCatSheafHom.

theorem AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison_eq {X Y : Scheme} (f : X ⟶ Y) (n : ℕ) : pullbackExteriorPowerComparison f n = TauCeti.SheafOfModules.pullbackExteriorPowerComparison (pullbackPushforwardAdjunction f) n

The scheme comparison is the sheaf comparison for the scheme pullback adjunction.

theorem AlgebraicGeometry.Scheme.Modules.mateEquiv_pullbackExteriorPowerComparison {X Y : Scheme} (f : X ⟶ Y) (n : ℕ) : (CategoryTheory.mateEquiv (pullbackPushforwardAdjunction f) (pullbackPushforwardAdjunction f)) (pullbackExteriorPowerComparison f n) = TauCeti.SheafOfModules.pushforwardExteriorPowerComparison (Hom.toRingCatSheafHom f) n

The mate of the scheme comparison under the pullback--pushforward adjunction is the pushforward comparison along f.toRingCatSheafHom.

theorem AlgebraicGeometry.Scheme.Modules.unit_comp_pushforward_map_pullbackExteriorPowerComparison_app {X Y : Scheme} (f : X ⟶ Y) (n : ℕ) (M : Y.Modules) : CategoryTheory.CategoryStruct.comp ((pullbackPushforwardAdjunction f).unit.app ((SheafOfModules.exteriorPower Y.sheaf n).obj M)) ((pushforward f).map ((pullbackExteriorPowerComparison f n).app M)) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.exteriorPower Y.sheaf n).map ((pullbackPushforwardAdjunction f).unit.app M)) ((TauCeti.SheafOfModules.pushforwardExteriorPowerComparison (Hom.toRingCatSheafHom f) n).app ((pullback f).obj M))

The adjunction equation characterizing the pullback comparison for modules on schemes: its transpose is the exterior power of the unit M ⟶ f_* f^* M followed by the exterior-power comparison of pushforward.

theorem AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison_app_comp_exteriorPowerOneIso {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) : CategoryTheory.CategoryStruct.comp ((pullbackExteriorPowerComparison f 1).app M) ((SheafOfModules.exteriorPowerOneIso X.sheaf).hom.app ((pullback f).obj M)) = (pullback f).map ((SheafOfModules.exteriorPowerOneIso Y.sheaf).hom.app M)

In degree one, the pullback comparison for modules on schemes is the identity of f^* M, read through the identifications ⋀¹ M ≅ M.

instance AlgebraicGeometry.Scheme.Modules.isIso_pullbackExteriorPowerComparison_one {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.IsIso (pullbackExteriorPowerComparison f 1)

The pullback comparison for modules on schemes is an isomorphism in degree one.