Nonzerodivisors of the structure sheaf and flat morphisms

A flat ring map sends nonzerodivisors to nonzerodivisors, so along a flat morphism of schemes f : X ⟶ Y the image under f.appLE of a nonzerodivisor on an affine open of Y is a nonzerodivisor on every affine open of X above it (Scheme.Hom.isSMulRegular_appLE).

A section that is a nonzerodivisor on every affine open inside U is one on every open subset of U, affine or not (Scheme.isSMulRegular_map_of_forall_affineOpens). Since restriction between affine opens is flat, a nonzerodivisor on an affine open U therefore remains a nonzerodivisor on every open subset of U (IsAffineOpen.isSMulRegular_map). Likewise, the pullback of a nonzerodivisor along a flat morphism to an affine scheme is a nonzerodivisor on every affine open of the source (Scheme.Hom.isSMulRegular_map_appTop); a nonzerodivisor of a ring R is one on Spec R by Scheme.isSMulRegular_ΓSpecIso_inv. Consequently the global sections of a scheme flat over Spec R form a torsion-free R-module (Scheme.Hom.isTorsionFree_appTop).

theorem AlgebraicGeometry.Scheme.isSMulRegular_map_of_forall_affineOpens {X : Scheme} {U V : X.Opens} (hVU : V ≤ U) {a : ↑(X.presheaf.obj (Opposite.op U))} (ha : ∀ (W : ↑X.affineOpens) (hWU : ↑W ≤ U), IsSMulRegular (↑(X.presheaf.obj (Opposite.op ↑W))) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hWU).op)) a)) : IsSMulRegular (↑(X.presheaf.obj (Opposite.op V))) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hVU).op)) a)

A section over U whose restriction to every affine open inside U is a nonzerodivisor restricts to a nonzerodivisor on every open subset V ⊆ U, affine or not.

theorem AlgebraicGeometry.Scheme.Hom.isSMulRegular_appLE {X Y : Scheme} (f : X ⟶ Y) [Flat f] {U : Y.Opens} (hU : IsAffineOpen U) {V : X.Opens} (hV : IsAffineOpen V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {b : ↑(Y.presheaf.obj (Opposite.op U))} (hb : IsSMulRegular (↑(Y.presheaf.obj (Opposite.op U))) b) : IsSMulRegular (↑(X.presheaf.obj (Opposite.op V))) ((CategoryTheory.ConcreteCategory.hom (appLE f U V e)) b)

Along a flat morphism f, the image under f.appLE of a nonzerodivisor on an affine open U of the target is a nonzerodivisor on every affine open V ⊆ f ⁻¹ᵁ U of the source.

theorem AlgebraicGeometry.IsAffineOpen.isSMulRegular_map {X : Scheme} {U V : X.Opens} (hU : IsAffineOpen U) (hVU : V ≤ U) {a : ↑(X.presheaf.obj (Opposite.op U))} (ha : IsSMulRegular (↑(X.presheaf.obj (Opposite.op U))) a) : IsSMulRegular (↑(X.presheaf.obj (Opposite.op V))) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hVU).op)) a)

A nonzerodivisor on an affine open U restricts to a nonzerodivisor on every open subset V ⊆ U, affine or not.

theorem AlgebraicGeometry.Scheme.Hom.isSMulRegular_map_appTop {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) [Flat f] {b : ↑(Y.presheaf.obj (Opposite.op ⊤))} (hb : IsSMulRegular (↑(Y.presheaf.obj (Opposite.op ⊤))) b) (U : ↑X.affineOpens) : IsSMulRegular (↑(X.presheaf.obj (Opposite.op ↑U))) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom (appTop f)) b))

Along a flat morphism to an affine scheme, the pullback of a nonzerodivisor restricts to a nonzerodivisor on every affine open of the source.

theorem AlgebraicGeometry.Scheme.isSMulRegular_ΓSpecIso_inv {R : Type u} [CommRing R] {π : R} (hπ : IsSMulRegular R π) : IsSMulRegular (↑((Spec ↧R).presheaf.obj (Opposite.op ⊤))) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso ↧R).inv) π)

A nonzerodivisor π of a ring R is a nonzerodivisor among the global functions on Spec R.

theorem AlgebraicGeometry.Scheme.Hom.isTorsionFree_appTop {X : Scheme} {R : Type u} [CommRing R] (f : X ⟶ Spec ↧R) [Flat f] : Module.IsTorsionFree R ↑(X.presheaf.obj (Opposite.op ⊤))

Along a flat morphism f : X ⟶ Spec R, the global sections of X form a torsion-free R-module, for the algebra structure induced by f.