Pullback of exterior powers in a locally constant degree

Let f : X ⟶ Y be a morphism of schemes and r : Y → ℕ a locally constant function. The exterior power ⋀^r M of an 𝒪_Y-module is the n-th exterior power over each open set r⁻¹{n} (TauCeti.AlgebraicGeometry.locallyConstantExteriorPower). Its pullback is compared with the exterior power of f^* M in the locally constant degree r ∘ f:

f^* (⋀^r M) ⟶ ⋀^{r ∘ f} (f^* M).

Since ⋀^{r ∘ f} is the product of the pushforwards of its restrictions to the open sets (r ∘ f)⁻¹{n} = f⁻¹ (r⁻¹{n}), the comparison is determined by its restrictions to these sets. There it is the n-th exterior power comparison f^* (⋀ⁿ M) ⟶ ⋀ⁿ (f^* M), read through the identifications of ⋀^r and ⋀^{r ∘ f} with ⋀ⁿ over r⁻¹{n} and f⁻¹ (r⁻¹{n}) and through the commutation of pullback with restriction to opens (restrictFunctor_map_pullbackLocallyConstantExteriorPowerComparison_app_comp). The open sets f⁻¹ (r⁻¹{n}) cover X, so the comparison is an isomorphism whenever all the n-th comparisons are (isIso_pullbackLocallyConstantExteriorPowerComparison_app_of_isIso), in particular for quasicoherent M (isIso_pullbackLocallyConstantExteriorPowerComparison_app).

Main declarations

• TauCeti.AlgebraicGeometry.pullbackLocallyConstantExteriorPowerComparison f r: the natural comparison f^* (⋀^r M) ⟶ ⋀^{r ∘ f} (f^* M);
• restrictFunctor_map_pullbackLocallyConstantExteriorPowerComparison_app_comp: over f⁻¹ (r⁻¹{n}) it is the n-th exterior power comparison;
• TauCeti.AlgebraicGeometry.isIso_pullbackLocallyConstantExteriorPowerComparison_app_of_isIso and TauCeti.AlgebraicGeometry.isIso_pullbackLocallyConstantExteriorPowerComparison_app: it is an isomorphism when every n-th exterior power comparison is, in particular on quasicoherent modules.

References

• [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter II, Exercise 5.16

noncomputable def TauCeti.AlgebraicGeometry.pullbackLocallyConstantExteriorPowerComparison {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (r : LocallyConstant ↥Y ℕ) : (locallyConstantExteriorPower r).comp (AlgebraicGeometry.Scheme.Modules.pullback f) ⟶ (AlgebraicGeometry.Scheme.Modules.pullback f).comp (locallyConstantExteriorPower (LocallyConstant.comap (TopCat.Hom.hom f.base) r))

The pullback comparison for exterior powers in a locally constant degree. For a morphism of schemes f : X ⟶ Y and a locally constant r : Y → ℕ, the natural map f^* (⋀^r M) ⟶ ⋀^{r ∘ f} (f^* M) which over each open set f⁻¹ (r⁻¹{n}) is the n-th exterior power comparison f^* (⋀ⁿ M) ⟶ ⋀ⁿ (f^* M) (restrictFunctor_map_pullbackLocallyConstantExteriorPowerComparison_app_comp).

theorem TauCeti.AlgebraicGeometry.restrictFunctor_map_pullbackLocallyConstantExteriorPowerComparison_app_comp {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (r : LocallyConstant ↥Y ℕ) (n : ℕ) (M : Y.Modules) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.restrictFunctor (AlgebraicGeometry.Scheme.Opens.ι ((LocallyConstant.comap (TopCat.Hom.hom f.base) r).fiberClopens n).toOpens)).map ((pullbackLocallyConstantExteriorPowerComparison f r).app M)) ((restrictLocallyConstantExteriorPowerIso (LocallyConstant.comap (TopCat.Hom.hom f.base) r) ((LocallyConstant.comap (TopCat.Hom.hom f.base) r).fiberClopens n).toOpens ⋯).hom.app ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M)) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.restrictPullbackIso f (r.fiberClopens n).toOpens ((LocallyConstant.comap (TopCat.Hom.hom f.base) r).fiberClopens n).toOpens ⋯).hom.app ((locallyConstantExteriorPower r).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Scheme.Hom.resLE f (r.fiberClopens n).toOpens ((LocallyConstant.comap (TopCat.Hom.hom f.base) r).fiberClopens n).toOpens ⋯)).map ((restrictLocallyConstantExteriorPowerIso r (r.fiberClopens n).toOpens ⋯).hom.app M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.restrictPullbackIso f (r.fiberClopens n).toOpens ((LocallyConstant.comap (TopCat.Hom.hom f.base) r).fiberClopens n).toOpens ⋯).inv.app ((SheafOfModules.exteriorPower Y.sheaf n).obj M)) ((AlgebraicGeometry.Scheme.Modules.restrictFunctor (AlgebraicGeometry.Scheme.Opens.ι ((LocallyConstant.comap (TopCat.Hom.hom f.base) r).fiberClopens n).toOpens)).map ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison f n).app M))))

The comparison over a fiber. Over the open set f⁻¹ (r⁻¹{n}), on which r ∘ f is constantly n, the comparison f^* (⋀^r M) ⟶ ⋀^{r ∘ f} (f^* M), followed by the identification of ⋀^{r ∘ f} with ⋀ⁿ there, is the n-th exterior power comparison f^* (⋀ⁿ M) ⟶ ⋀ⁿ (f^* M), read through the commutation of pullback with restriction (Scheme.Modules.restrictPullbackIso) and the identification of ⋀^r with ⋀ⁿ over r⁻¹{n}.

theorem TauCeti.AlgebraicGeometry.isIso_pullbackLocallyConstantExteriorPowerComparison_app_of_isIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (r : LocallyConstant ↥Y ℕ) (M : Y.Modules) (h : ∀ (n : ℕ), CategoryTheory.IsIso ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison f n).app M)) : CategoryTheory.IsIso ((pullbackLocallyConstantExteriorPowerComparison f r).app M)

The comparison f^* (⋀^r M) ⟶ ⋀^{r ∘ f} (f^* M) is an isomorphism as soon as every exterior power comparison f^* (⋀ⁿ M) ⟶ ⋀ⁿ (f^* M) is.

instance TauCeti.AlgebraicGeometry.isIso_pullbackLocallyConstantExteriorPowerComparison_app {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (r : LocallyConstant ↥Y ℕ) (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] : CategoryTheory.IsIso ((pullbackLocallyConstantExteriorPowerComparison f r).app M)

Exterior powers in a locally constant degree commute with pullback of quasicoherent sheaves: for every morphism of schemes f : X ⟶ Y, every locally constant r : Y → ℕ and every quasicoherent 𝒪_Y-module M, the comparison f^* (⋀^r M) ⟶ ⋀^{r ∘ f} (f^* M) is an isomorphism.