The fibrewise criterion for flatness of finite morphisms

Let f : X ⟶ Y and g : Y ⟶ S be morphisms of schemes, with f finite and locally of finite presentation and X flat over S. If for every point s of S the base change of f to the fibre Y_s = g.fiber s, that is X ×_Y Y_s ⟶ Y_s, is flat, then f is flat (AlgebraicGeometry.Scheme.Hom.flat_of_flat_pullback_fiberι). No Noetherian hypothesis is needed.

This turns flatness over fields into flatness over an arbitrary base: for a finite morphism between two families over S (for instance multiplication by a nonzero integer on an elliptic curve over S), flatness of f reduces to flatness of its restrictions to the fibres, which are morphisms of schemes over fields.

The proof reduces to S, Y and X affine and then applies the algebraic criterion Module.Flat.of_flat_fiber to the finitely presented Γ(Y)-module Γ(X). Along the way the hypothesis is used in the equivalent form that the base change of f along Y ×_S Spec K ⟶ Y is flat for every field K and every morphism Spec K ⟶ S; every such morphism factors through the residue field of its image point.

Main results

• AlgebraicGeometry.Scheme.Hom.flat_of_flat_pullback_fiberι: the fibrewise criterion for flatness of a finite, locally finitely presented morphism.

References

• A. Grothendieck, Éléments de géométrie algébrique IV, troisième partie, Théorème 11.3.10, the critère de platitude par fibres.

theorem AlgebraicGeometry.Scheme.Hom.flat_of_flat_pullback_fiberι {X Y S : Scheme} (f : X ⟶ Y) (g : Y ⟶ S) [IsFinite f] [LocallyOfFinitePresentation f] [Flat (CategoryTheory.CategoryStruct.comp f g)] (h : ∀ (s : ↥S), Flat (CategoryTheory.Limits.pullback.snd f (fiberι g s))) : Flat f

The fibrewise criterion for flatness of a finite morphism. Let f : X ⟶ Y be finite and locally of finite presentation, and g : Y ⟶ S such that X is flat over S. If for every point s of S the base change X ×_Y Y_s ⟶ Y_s of f to the fibre Y_s of g is flat, then f is flat.