Base change of quasicoherent sections #
For a morphism of schemes, if an open and its inverse image are affine, sections of the
pullback of a quasicoherent sheaf are obtained by extending scalars along the coordinate-ring
map. The isomorphism is characterized by sending 1 ⊗ s to the pullback of s. In particular,
if a single section generates the sections over the affine open, its pullback generates the
sections of the pullback over the inverse image.
For a cartesian square over Spec S ⟶ Spec R, the same section map exhibits sections on the
inverse image as the base change from R to S. This is the affine-cover input for cohomology
and base change. The module structures remain caller parameters, including at the top open.
Use pullbackSectionsEquiv for extension of scalars along the coordinate-ring map, and
isBaseChange_pullbackSections for extension along the original base-ring map R ⟶ S.
When R → S is flat, the same holds over every quasi-compact quasi-separated open U, which is
flat base change for the sections of a quasicoherent sheaf
(isBaseChange_pullbackSections_of_isQuasiSeparated). Cover U by finitely many affine opens
V i. Sections over U are the kernel of the differences of restrictions
∏ Γ(V i, M) → ∏ Γ(V i ∩ V j, M), before and after base change, and tensoring with the flat
algebra S preserves this kernel. The comparison is a base change on each V i, and it is
injective on each quasi-compact V i ∩ V j (liftBaseChange_pullbackSectionsBaseLinear_injective),
by the same argument with only the restrictions to the cover. This follows the proof of
Mathlib's AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right for the
structure sheaf.
The same holds over affine opens of the bases of an arbitrary cartesian square
g' ≫ f = f' ≫ g: for affine opens W of S and W' ⊆ g⁻¹ W of S', an open UX ⊆ f⁻¹ W and
UY = g'⁻¹ UX ∩ f'⁻¹ W', pulling back sections exhibits Γ(UY, g'^* M) as
Γ(S', W') ⊗[Γ(S, W)] Γ(UX, M), for affine UX (isBaseChange_pullbackSectionsLEBaseLinear)
or for quasi-compact quasi-separated UX and flat g
(isBaseChange_pullbackSectionsLEBaseLinear_of_isQuasiSeparated). The square
restricts to a cartesian square UY ⟶ UX over W' ⟶ W ≅ Spec Γ(S, W)
(Mathlib's AlgebraicGeometry.Scheme.Hom.isPullback_resLE), which reduces these to the global
statements.
Main results #
AlgebraicGeometry.Scheme.Hom.span_singleton_pullbackSections_eq_top: over affine opens, the pullback of a generator of the sections generates the sections of the pullback.AlgebraicGeometry.Scheme.Hom.isBaseChange_pullbackSections: base change of sections over an affine open, along any base-ring map.AlgebraicGeometry.Scheme.Hom.flat_sectionsBase_pullback: flatness of the sections over an affine open survives every base change.AlgebraicGeometry.Scheme.Hom.liftBaseChange_pullbackSectionsBaseLinear_injective: for flatR → S, the comparisonS ⊗[R] Γ(U, M) → Γ(g⁻¹ U, g^* M)is injective over a quasi-compact openU.AlgebraicGeometry.Scheme.Hom.isBaseChange_pullbackSections_of_isQuasiSeparated: for flatR → S, it is bijective over a quasi-compact quasi-separated openU.AlgebraicGeometry.Scheme.Hom.pullbackSectionsLEBaseLinear: in a commutative square, pullback of sections from an open overW ⊆ Sto an open overW' ⊆ g⁻¹ W, linear overΓ(S, W).AlgebraicGeometry.Scheme.Hom.isBaseChange_pullbackSectionsLEBaseLinearandAlgebraicGeometry.Scheme.Hom.isBaseChange_pullbackSectionsLEBaseLinear_of_isQuasiSeparated: in a cartesian square, it is a base change fromΓ(S, W)toΓ(S', W')for affineW,W', when the open ofXis affine, or quasi-compact quasi-separated andgis flat.
References #
- R. Hartshorne, Algebraic Geometry, Proposition II.5.2(e) and Proposition III.9.3.
- The Stacks Project, Tag 01I9 (pullback of quasicoherent sheaves) and Tag 02KH (flat base change of cohomology).
If an open and its inverse image are affine, sections of a quasicoherent pullback are the extension of the original section module along the map of coordinate rings. No flatness or finiteness hypothesis is required.
Instances For
The affine section comparison sends 1 ⊗ s to the pullback of s.
The inverse affine comparison takes a pulled-back section to 1 ⊗ s.
If a single section m₀ generates Γ(U, M) over Γ(X, U), then its pullback generates
Γ(g⁻¹ U, g^* M) over Γ(Y, g⁻¹ U), when U and g⁻¹ U are affine.
Pullback of sections is linear over the original base in a commuting square over
Spec S ⟶ Spec R. The module structures and scalar towers are caller parameters, so this
also preserves the usual actions on global sections when U = ⊤.
Instances For
The base-linear pullback has the same values as the canonical semilinear section map.
Affine base change of quasicoherent sections over the original base ring. No flatness, finiteness, or Noetherian hypothesis is needed. Caller-supplied module structures are retained.
Flat sections stay flat after base change. If the sections of a quasi-coherent sheaf M
over an affine open U of X form a flat R-module, then for every base change Y = X ×_R S
along a ring map R → S, the sections of the pullback g^* M over g⁻¹ U form a flat
S-module, being the base change S ⊗_R Γ(M, U).
Flat base change of sections over a quasi-compact open is injective. Let X be a scheme
over R, let R → S be flat and let Y = X ×_R S with projection g : Y ⟶ X. For a
quasi-coherent sheaf M on X and a quasi-compact open U of X, the map
S ⊗[R] Γ(U, M) → Γ(g⁻¹ U, g^* M), s ⊗ m ↦ s • g^* m, is injective.
Flat base change of sections over a quasi-compact quasi-separated open. Let X be a scheme
over R, let R → S be flat and let Y = X ×_R S with projection g : Y ⟶ X. For a
quasi-coherent sheaf M on X and a quasi-compact quasi-separated open U of X, pulling back
sections exhibits Γ(g⁻¹ U, g^* M) as the base change S ⊗[R] Γ(U, M).
Pulling back sections along g' in a commutative square
g' ≫ f = f' ≫ g (with g' : X' ⟶ X, f : X ⟶ S, f' : X' ⟶ S', g : S' ⟶ S), from an open
UX lying over an open W of S to an open UY ⊆ g'⁻¹ UX lying over an open W' ⊆ g⁻¹ W of
S', as a map linear over Γ(S, W). Here Γ(S, W) acts on Γ(S', W'), Γ(X, UX) and
Γ(X', UY) through g.appLE, f.appLE and f'.appLE; the module structures on the sections are
caller parameters compatible with these.
Instances For
The base-linear pullback of sections has the values of Scheme.Hom.pullbackSectionsLE.
Flat base change of sections over affine opens of the bases. Let
g' ≫ f = f' ≫ g be a cartesian square with g : S' ⟶ S flat, and M a quasi-coherent sheaf on
X. For affine opens W of S and W' ⊆ g⁻¹ W of S', a quasi-compact quasi-separated open
UX ⊆ f⁻¹ W of X and UY = g'⁻¹ UX ∩ f'⁻¹ W', pulling back sections exhibits Γ(UY, g'^* M) as
the base change Γ(S', W') ⊗[Γ(S, W)] Γ(UX, M).
Base change of sections over affine opens. Let g' ≫ f = f' ≫ g be a cartesian square
and M a quasi-coherent sheaf on X. For affine opens W of S, W' ⊆ g⁻¹ W of S' and
UX ⊆ f⁻¹ W of X, and UY = g'⁻¹ UX ∩ f'⁻¹ W', pulling back sections exhibits Γ(UY, g'^* M)
as the base change Γ(S', W') ⊗[Γ(S, W)] Γ(UX, M). No flatness is needed.