Pushforward and restriction of modules on schemes

Pushforward along a scheme isomorphism agrees with restriction along its inverse. This identification transports local properties of module sheaves through affine normalizations. Restriction of a pushforward to an open of the base agrees with pushforward of the restriction to its preimage. Both comparisons have formulas on sections.

These comparisons use Mathlib's module pushforward and restriction API.

theorem TauCeti.AlgebraicGeometry.pushforward_comp_toSheaf {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : (AlgebraicGeometry.Scheme.Modules.pushforward f).comp (SheafOfModules.toSheaf Y.ringCatSheaf) = (SheafOfModules.toSheaf X.ringCatSheaf).comp (TopCat.Sheaf.pushforward AddCommGrpCat f.base)

Forgetting the module structure commutes with direct image.

noncomputable def TauCeti.AlgebraicGeometry.pushforwardCompToPresheafIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : (AlgebraicGeometry.Scheme.Modules.pushforward f).comp (AlgebraicGeometry.Scheme.Modules.toPresheaf Y) ≅ (AlgebraicGeometry.Scheme.Modules.toPresheaf X).comp (TopCat.Presheaf.pushforward AddCommGrpCat f.base)

Forgetting the module structure commutes with direct image, on underlying presheaves: the abelian presheaf of f_* M is the abelian presheaf of M precomposed with inverse image of opens.

theorem TauCeti.AlgebraicGeometry.pushforward_obj_smul {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (M : X.Modules) {U : Y.Opens} (r : ↑(Y.presheaf.obj (Opposite.op U))) (x : ↑(((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M).presheaf.obj (Opposite.op U))) : r • x = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r • have this := x; this

A function r on an open U of Y acts on sections of f_* M over U through f.app U r, as a section of M over f ⁻¹ᵁ U.

noncomputable def TauCeti.AlgebraicGeometry.pushforwardIsoRestrictFunctor {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) : AlgebraicGeometry.Scheme.Modules.pushforward e.hom ≅ AlgebraicGeometry.Scheme.Modules.restrictFunctor e.inv

Pushforward along an isomorphism agrees with restriction along its inverse.

@[simp]

theorem TauCeti.AlgebraicGeometry.pushforwardIsoRestrictFunctor_hom_app_val_app_apply {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (M : X.Modules) (V : Y.Opens) (x : ↑(((AlgebraicGeometry.Scheme.Modules.pushforward e.hom).obj M).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (((pushforwardIsoRestrictFunctor e).hom.app M).val.app (Opposite.op V))) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (CategoryTheory.eqToHom ⋯).op)) x

On sections, pushforward along an isomorphism is restriction along the equality between the image under its inverse and the preimage under the forward map.

@[simp]

theorem TauCeti.AlgebraicGeometry.pushforwardIsoRestrictFunctor_inv_app_val_app_apply {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (M : X.Modules) (V : Y.Opens) (x : ↑((M.restrict e.inv).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (((pushforwardIsoRestrictFunctor e).inv.app M).val.app (Opposite.op V))) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (CategoryTheory.eqToHom ⋯).op)) x

The inverse pushforward--restriction comparison uses the inverse equality of opens.

noncomputable def TauCeti.AlgebraicGeometry.restrictPushforwardIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) : (AlgebraicGeometry.Scheme.Modules.pushforward f).comp (AlgebraicGeometry.Scheme.Modules.restrictFunctor U.ι) ≅ (AlgebraicGeometry.Scheme.Modules.restrictFunctor ((TopologicalSpace.Opens.map f.base).obj U).ι).comp (AlgebraicGeometry.Scheme.Modules.pushforward (f ∣_ U))

Restricting a pushforward to an open of the base agrees with pushing forward the restriction to its preimage, naturally in the module sheaf.

@[simp]

theorem TauCeti.AlgebraicGeometry.restrictPushforwardIso_hom_app_val_app_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (M : X.Modules) (V : (↑U).Opens) (x : ↑((((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M).restrict U.ι).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (((restrictPushforwardIso f U).hom.app M).val.app (Opposite.op V))) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (CategoryTheory.eqToHom ⋯).op)) x

On sections, open restriction of pushforward is the restriction along the equality of the two inverse-image opens.

@[simp]

theorem TauCeti.AlgebraicGeometry.restrictPushforwardIso_inv_app_val_app_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (M : X.Modules) (V : (↑U).Opens) (x : ↑(((AlgebraicGeometry.Scheme.Modules.pushforward (f ∣_ U)).obj (M.restrict ((TopologicalSpace.Opens.map f.base).obj U).ι)).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (((restrictPushforwardIso f U).inv.app M).val.app (Opposite.op V))) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (CategoryTheory.eqToHom ⋯).op)) x

The inverse comparison restricts along the inverse equality of inverse-image opens.