Affine base change of global sections

For a ring map φ : R ⟶ S, the canonical map S ⊗_R Γ(Spec R, M) ⟶ Γ(Spec S, (Spec φ)^* M) is natural in the sheaf of modules M. It is an isomorphism when M is quasicoherent, with no flatness or finiteness hypothesis. The comparison sends 1 ⊗ m to the pullback of the section m.

This is the affine section calculation underlying cohomology and base change. The map is defined for arbitrary coefficient sheaves; quasicoherence is used only for its invertibility. It also supplies the section-module comparison used to transport invariants of modules, such as Fitting ideals, under scheme pullback.

The construction uses tildeFunctorCompPullbackIso, the tilde/global-sections adjunction, and the extension/restriction-of-scalars adjunction. The characteristic equation identifies it with the map adjoint to pulling back global sections.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.2(e).
• The Stacks Project, Tag 01I9 (pullback of quasicoherent sheaves on affine schemes).

noncomputable def CommRingCat.Hom.moduleSpecΓPullback {R S : CommRingCat} (φ : R ⟶ S) : AlgebraicGeometry.moduleSpecΓFunctor.comp (ModuleCat.extendScalars (hom φ)) ⟶ (AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).comp AlgebraicGeometry.moduleSpecΓFunctor

The natural affine base-change map from scalar extension of global sections to global sections of the pulled-back module sheaf.

theorem CommRingCat.Hom.moduleSpecΓPullback_app {R S : CommRingCat} (φ : R ⟶ S) (M : (AlgebraicGeometry.Spec R).Modules) : (moduleSpecΓPullback φ).app M = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toTildeΓNatIso.hom.app ((ModuleCat.extendScalars (hom φ)).obj (AlgebraicGeometry.moduleSpecΓFunctor.obj M))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.moduleSpecΓFunctor.map ((TauCeti.AlgebraicGeometry.tildeFunctorCompPullbackIso φ).inv.app (AlgebraicGeometry.moduleSpecΓFunctor.obj M))) (AlgebraicGeometry.moduleSpecΓFunctor.map ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).map (AlgebraicGeometry.tilde.adjunction.counit.app M))))

The affine comparison is obtained by sheafifying the extended section module and then pulling back the tilde/global-sections counit.

theorem CommRingCat.Hom.unit_moduleSpecΓPullback_app {R S : CommRingCat} (φ : R ⟶ S) (M : (AlgebraicGeometry.Spec R).Modules) : CategoryTheory.CategoryStruct.comp ((ModuleCat.extendRestrictScalarsAdj (hom φ)).unit.app (AlgebraicGeometry.moduleSpecΓFunctor.obj M)) ((ModuleCat.restrictScalars (hom φ)).map ((moduleSpecΓPullback φ).app M)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.moduleSpecΓFunctor.map ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction (AlgebraicGeometry.Spec.map φ)).unit.app M)) ((TauCeti.AlgebraicGeometry.pushforwardCompModuleSpecΓFunctorIso φ).hom.app ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).obj M))

The affine comparison is adjoint to pulling back sections along Spec φ.

theorem CommRingCat.Hom.unit_moduleSpecΓPullback_app_assoc {R S : CommRingCat} (φ : R ⟶ S) (M : (AlgebraicGeometry.Spec R).Modules) {Z : ModuleCat ↑R} (h : (ModuleCat.restrictScalars (hom φ)).obj (AlgebraicGeometry.moduleSpecΓFunctor.obj ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).obj M)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((ModuleCat.extendRestrictScalarsAdj (hom φ)).unit.app (AlgebraicGeometry.moduleSpecΓFunctor.obj M)) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (hom φ)).map ((moduleSpecΓPullback φ).app M)) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.moduleSpecΓFunctor.map ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction (AlgebraicGeometry.Spec.map φ)).unit.app M)) (CategoryTheory.CategoryStruct.comp ((TauCeti.AlgebraicGeometry.pushforwardCompModuleSpecΓFunctorIso φ).hom.app ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).obj M)) h)

The affine comparison is adjoint to pulling back sections along Spec φ.

@[simp]

theorem CommRingCat.Hom.moduleSpecΓPullback_app_one_tmul {R S : CommRingCat} (φ : R ⟶ S) (M : (AlgebraicGeometry.Spec R).Modules) (m : ↑(AlgebraicGeometry.moduleSpecΓFunctor.obj M)) : (CategoryTheory.ConcreteCategory.hom ((moduleSpecΓPullback φ).app M)) (1 ⊗ₜ[↑R] m) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.moduleSpecΓFunctor.map ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction (AlgebraicGeometry.Spec.map φ)).unit.app M))) m

The affine base-change map sends 1 ⊗ m to the pullback of the global section m.

theorem CommRingCat.Hom.isIso_moduleSpecΓPullback_app {R S : CommRingCat} (φ : R ⟶ S) (M : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent M] : CategoryTheory.IsIso ((moduleSpecΓPullback φ).app M)

Affine base change of global sections is invertible for quasicoherent coefficients. The ring map need not be flat.

noncomputable def CommRingCat.Hom.moduleSpecΓPullbackIso {R S : CommRingCat} (φ : R ⟶ S) (M : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent M] : (ModuleCat.extendScalars (hom φ)).obj (AlgebraicGeometry.moduleSpecΓFunctor.obj M) ≅ AlgebraicGeometry.moduleSpecΓFunctor.obj ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).obj M)

Scalar extension of the global sections of a quasicoherent sheaf agrees with the global sections of its pullback. The forward map is moduleSpecΓPullback.

@[simp]

theorem CommRingCat.Hom.moduleSpecΓPullbackIso_hom {R S : CommRingCat} (φ : R ⟶ S) (M : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent M] : (moduleSpecΓPullbackIso φ M).hom = (moduleSpecΓPullback φ).app M

The forward affine section isomorphism is the canonical base-change map.