Flat base change for sections of the structure sheaf

Let X be a scheme over a commutative ring R, let R → R' be a ring map, and let Y = X ×_R R' be the base change, given as a pullback square H over Spec R' ⟶ Spec R, with projection g : Y ⟶ X. The sections of the structure sheaf over opens are algebras over the base ring through Scheme.baseRingToStructurePresheaf. This file records that pulling back sections along g is compatible with these base-ring maps, and packages it as an R-linear map Γ(X, W) → Γ(Y, W'), where R acts on Γ(Y, W') through R → R'.

When R → R' is flat and W is quasi-compact and quasi-separated, Mathlib's AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right says that Γ(Y, g⁻¹ W) = R' ⊗_R Γ(X, W). This file restates it in terms of the base-ring maps, as a pushout square of commutative rings and as IsBaseChange for the linear map above.

Main definitions and results

• TauCeti.AlgebraicGeometry.baseRingToStructurePresheaf_app_comp_appLE_of_isPullback: pulling back sections along g commutes with the base-ring maps.
• TauCeti.AlgebraicGeometry.appTop_baseRingToGlobalSections_of_isPullback: the same on global sections, for the base-ring maps to global functions.
• TauCeti.AlgebraicGeometry.isPushout_baseRingToStructurePresheaf_app_of_flat: flat base change for sections of the structure sheaf, as a pushout square of commutative rings.
• TauCeti.AlgebraicGeometry.sectionsBaseChange: pulling back sections along g, as an R-linear map.
• TauCeti.AlgebraicGeometry.isBaseChange_sectionsBaseChange: flat base change for sections of the structure sheaf, as IsBaseChange.

References

• The Stacks Project, Lemma 30.5.2, flat base change.

theorem TauCeti.AlgebraicGeometry.baseRingToStructurePresheaf_app_comp_appLE_of_isPullback {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] {R' : Type u} [CommRing R'] [Algebra R R'] {Y : AlgebraicGeometry.Scheme} [Y.Over (AlgebraicGeometry.Spec ↧R')] {g : Y ⟶ X} (H : CategoryTheory.IsPullback g (Y ↘ AlgebraicGeometry.Spec ↧R') (X ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R R')))) {W : X.Opens} {W' : Y.Opens} (hW : W' ≤ (TopologicalSpace.Opens.map g.base).obj W) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.baseRingToStructurePresheaf R X).app (Opposite.op W)) (AlgebraicGeometry.Scheme.Hom.appLE g W W' hW) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R R')) ((AlgebraicGeometry.Scheme.baseRingToStructurePresheaf R' Y).app (Opposite.op W'))

Pulling back sections along the base change g is compatible with the base-ring maps on both sides.

theorem TauCeti.AlgebraicGeometry.appTop_baseRingToGlobalSections_of_isPullback {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] {R' : Type u} [CommRing R'] [Algebra R R'] {Y : AlgebraicGeometry.Scheme} [Y.Over (AlgebraicGeometry.Spec ↧R')] {g : Y ⟶ X} (H : CategoryTheory.IsPullback g (Y ↘ AlgebraicGeometry.Spec ↧R') (X ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R R')))) (r : R) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop g)) ((AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections R X) r) = (AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections R' Y) ((algebraMap R R') r)

The base change g carries the action of the base ring R on global functions to the action of R', through algebraMap R R'.

theorem TauCeti.AlgebraicGeometry.isPushout_baseRingToStructurePresheaf_app_of_flat {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] {R' : Type u} [CommRing R'] [Algebra R R'] {Y : AlgebraicGeometry.Scheme} [Y.Over (AlgebraicGeometry.Spec ↧R')] {g : Y ⟶ X} (H : CategoryTheory.IsPullback g (Y ↘ AlgebraicGeometry.Spec ↧R') (X ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R R')))) [Module.Flat R R'] {W : X.Opens} (hW : IsCompact ↑W) (hW' : IsQuasiSeparated ↑W) {W' : Y.Opens} (hW'eq : W' = (TopologicalSpace.Opens.map g.base).obj W) : CategoryTheory.IsPushout ((AlgebraicGeometry.Scheme.baseRingToStructurePresheaf R X).app (Opposite.op W)) (CommRingCat.ofHom (algebraMap R R')) (AlgebraicGeometry.Scheme.Hom.appLE g W W' ⋯) ((AlgebraicGeometry.Scheme.baseRingToStructurePresheaf R' Y).app (Opposite.op W'))

Flat base change for sections of the structure sheaf, as a pushout square of commutative rings: for a flat ring map R → R' and a quasi-compact quasi-separated open W of X, Γ(Y, g⁻¹ W) = R' ⊗_R Γ(X, W).

def TauCeti.AlgebraicGeometry.sectionsBaseChange {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] {R' : Type u} [CommRing R'] [Algebra R R'] {Y : AlgebraicGeometry.Scheme} [Y.Over (AlgebraicGeometry.Spec ↧R')] {g : Y ⟶ X} (H : CategoryTheory.IsPullback g (Y ↘ AlgebraicGeometry.Spec ↧R') (X ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R R')))) {W : X.Opens} {W' : Y.Opens} (hW : W' ≤ (TopologicalSpace.Opens.map g.base).obj W) : ↑(X.presheaf.obj (Opposite.op W)) →ₗ[R] ↑(Y.presheaf.obj (Opposite.op W'))

Pulling back sections of the structure sheaf along the base change g, as an R-linear map. Here R and R' act on sections through Scheme.baseRingToStructurePresheaf, and R acts on the sections of Y through R → R'.

@[simp]

theorem TauCeti.AlgebraicGeometry.sectionsBaseChange_apply {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] {R' : Type u} [CommRing R'] [Algebra R R'] {Y : AlgebraicGeometry.Scheme} [Y.Over (AlgebraicGeometry.Spec ↧R')] {g : Y ⟶ X} (H : CategoryTheory.IsPullback g (Y ↘ AlgebraicGeometry.Spec ↧R') (X ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R R')))) {W : X.Opens} {W' : Y.Opens} (hW : W' ≤ (TopologicalSpace.Opens.map g.base).obj W) (s : ↑(X.presheaf.obj (Opposite.op W))) : (sectionsBaseChange H hW) s = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE g W W' hW)) s

sectionsBaseChange pulls back sections along g.

theorem TauCeti.AlgebraicGeometry.isBaseChange_sectionsBaseChange {R : Type u} [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] {R' : Type u} [CommRing R'] [Algebra R R'] {Y : AlgebraicGeometry.Scheme} [Y.Over (AlgebraicGeometry.Spec ↧R')] {g : Y ⟶ X} (H : CategoryTheory.IsPullback g (Y ↘ AlgebraicGeometry.Spec ↧R') (X ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R R')))) [Module.Flat R R'] {W : X.Opens} (hW : IsCompact ↑W) (hW' : IsQuasiSeparated ↑W) {W' : Y.Opens} (hW'eq : W' = (TopologicalSpace.Opens.map g.base).obj W) : IsBaseChange R' (sectionsBaseChange H ⋯)

Flat base change for sections of the structure sheaf: for a flat ring map R → R' and a quasi-compact quasi-separated open W of X, pulling back sections exhibits Γ(Y, g⁻¹ W) as the base change R' ⊗_R Γ(X, W).