Flatness of scheme-theoretic images over a Bezout domain

Let R be a Bezout domain, for instance a discrete valuation ring, with an injective map to a field K, and let X be a scheme over R. If a quasi-compact morphism f : Y ⟶ X comes from a scheme Y over K, then the scheme-theoretic image of f is flat over R.

On an affine open U of X, the sections of the image over U form the quotient of Γ(X, U) by the kernel of Γ(X, U) → Γ(Y, f⁻¹ U), so they embed into a K-algebra. Nonzero elements of R are therefore nonzerodivisors on them, which over a Bezout domain is flatness (Module.Flat.flat_iff_algebraMap_mem_nonZeroDivisors_of_isBezout).

Over a discrete valuation ring this is the flatness of the scheme-theoretic closure of the generic fibre: closing up a subscheme of X_K inside X yields a flat model of it.

Main results

• AlgebraicGeometry.Scheme.Hom.flat_imageι_comp: the scheme-theoretic image of a quasi-compact morphism from a scheme over K to a scheme over R is flat over R.

References

• The Stacks Project, Tag 0539, flatness over valuation rings, generalized in Mathlib to Bezout domains.

theorem AlgebraicGeometry.Scheme.Hom.flat_imageι_comp {R K : Type u} [CommRing R] [IsDomain R] [IsBezout R] [Field K] [Algebra R K] [FaithfulSMul R K] {X Y : Scheme} (f : Y ⟶ X) [QuasiCompact f] (g : X ⟶ Spec ↧R) (toK : Y ⟶ Spec ↧K) (h : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp toK (Spec.map (CommRingCat.ofHom (algebraMap R K)))) : Flat (CategoryTheory.CategoryStruct.comp (imageι f) g)

Let R be a Bezout domain with an injective map to a field K, let g : X ⟶ Spec R, and let f : Y ⟶ X be quasi-compact with f ≫ g factoring through Spec K. Then the scheme-theoretic image of f is flat over R.