Pushforward of quasicoherent modules along isomorphisms and morphisms of spectra

Let φ : R ⟶ S be a morphism of commutative rings. Pushforward along the induced morphism Spec S ⟶ Spec R preserves quasicoherent modules. Indeed, Mathlib identifies quasicoherence on a spectrum with invertibility of the canonical map from the sheaf associated to global sections, and proves that this map remains invertible after pushforward along Spec φ.

The resulting functor QuasicoherentSheaf.pushforwardSpecMap is the pushforward operation along a morphism of spectra. It is compatible with identities and composition of ring maps. This calculation is the affine-local input for constructing the quasicoherent coordinate algebra p_* 𝒪_V of an affine morphism p : V ⟶ X.

Pushforward along a scheme isomorphism also preserves quasicoherence, via the comparison with restriction along its inverse.

Main declarations

• AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pushforward_specMap: pushforward along a morphism of spectra preserves quasicoherence;
• TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMap: the induced functor on quasicoherent sheaves;
• TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMapId, TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMapComp: its compatibility with identities and composition.

References

• The Stacks Project, Tag 01LC: pushforward along a quasi-compact and quasi-separated morphism preserves quasi-coherence. The case of a morphism of spectra is the one formalized here.

instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pushforward_specMap {R S : CommRingCat} (f : R ⟶ S) (M : (Spec S).Modules) [SheafOfModules.IsQuasicoherent M] : SheafOfModules.IsQuasicoherent ((pushforward (Spec.map f)).obj M)

Pushforward of a quasicoherent module along Spec S ⟶ Spec R is quasicoherent.

theorem TauCeti.AlgebraicGeometry.isQuasicoherent_pushforward_of_iso {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (M : X.Modules) [SheafOfModules.IsQuasicoherent M] : SheafOfModules.IsQuasicoherent ((AlgebraicGeometry.Scheme.Modules.pushforward e.hom).obj M)

Pushforward along a scheme isomorphism preserves quasicoherence.

noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMap {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Functor (QuasicoherentSheaf (AlgebraicGeometry.Spec S)) (QuasicoherentSheaf (AlgebraicGeometry.Spec R))

Pushforward of quasicoherent sheaves along the morphism of spectra induced by a ring homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMap_obj_obj {R S : CommRingCat} (f : R ⟶ S) (M : QuasicoherentSheaf (AlgebraicGeometry.Spec S)) : ((pushforwardSpecMap f).obj M).obj = (AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map f)).obj M.obj

The underlying module of affine quasicoherent pushforward is ordinary module pushforward.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMap_map_hom {R S : CommRingCat} (f : R ⟶ S) {M N : QuasicoherentSheaf (AlgebraicGeometry.Spec S)} (g : M ⟶ N) : ((pushforwardSpecMap f).map g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map f)).map g.hom) (CategoryTheory.eqToHom ⋯))

Affine quasicoherent pushforward acts on morphisms by ordinary module pushforward.

noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMapId (R : CommRingCat) : pushforwardSpecMap (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (QuasicoherentSheaf (AlgebraicGeometry.Spec R))

Affine quasicoherent pushforward along the identity ring map is naturally the identity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMapId_hom_app_hom (R : CommRingCat) (M : QuasicoherentSheaf (AlgebraicGeometry.Spec R)) : ((pushforwardSpecMapId R).hom.app M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforwardCongr ⋯).hom.app M.obj) ((AlgebraicGeometry.Scheme.Modules.pushforwardId (AlgebraicGeometry.Spec R)).hom.app M.obj))

The identity comparison is Mathlib's comparison on underlying modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMapId_inv_app_hom (R : CommRingCat) (M : QuasicoherentSheaf (AlgebraicGeometry.Spec R)) : ((pushforwardSpecMapId R).inv.app M).hom = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforwardId (AlgebraicGeometry.Spec R)).inv.app M.obj) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforwardCongr ⋯).inv.app M.obj) (CategoryTheory.eqToHom ⋯))

The inverse identity comparison is Mathlib's inverse on underlying modules.

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMapComp_obj_obj {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (M : QuasicoherentSheaf (AlgebraicGeometry.Spec T)) : (((pushforwardSpecMap g).comp (pushforwardSpecMap f)).obj M).obj = ((AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map g)).comp (AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map f))).obj M.obj

The underlying module of a composite affine quasicoherent pushforward is the composite module pushforward.

noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMapComp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : (pushforwardSpecMap g).comp (pushforwardSpecMap f) ≅ pushforwardSpecMap (CategoryTheory.CategoryStruct.comp f g)

Affine quasicoherent pushforward respects composition of ring maps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMapComp_hom_app_hom {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (M : QuasicoherentSheaf (AlgebraicGeometry.Spec T)) : ((pushforwardSpecMapComp f g).hom.app M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforwardComp (AlgebraicGeometry.Spec.map g) (AlgebraicGeometry.Spec.map f)).hom.app M.obj) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforwardCongr ⋯).hom.app M.obj) (CategoryTheory.eqToHom ⋯)))

The composition comparison is Mathlib's comparison on underlying modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pushforwardSpecMapComp_inv_app_hom {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (M : QuasicoherentSheaf (AlgebraicGeometry.Spec T)) : ((pushforwardSpecMapComp f g).inv.app M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforwardCongr ⋯).inv.app M.obj) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforwardComp (AlgebraicGeometry.Spec.map g) (AlgebraicGeometry.Spec.map f)).inv.app M.obj) (CategoryTheory.eqToHom ⋯)))

The inverse composition comparison is Mathlib's inverse on underlying modules.