The fibrewise criterion for flatness of finitely presented modules

Let R → B be a ring homomorphism and M a finitely presented B-module which is flat over R. If for every prime p of R the base change of M to the fibre ring B ⊗[R] κ(p) is flat over B ⊗[R] κ(p), then M is flat over B (Module.Flat.of_flat_fiber). Geometrically: a finite and finitely presented morphism X ⟶ Y of schemes over S, with X flat over S, is flat as soon as its restriction to every fibre over S is flat. This deduces flatness of a finite morphism between two families over S from flatness over fields, as is needed for multiplication by an integer on an elliptic curve over an arbitrary base.

The local statement is Module.Free.of_flat_fiber: if B is local and p is the inverse image of its maximal ideal in R, flatness of M over R and of its fibre (B ⊗[R] κ(p)) ⊗[B] M over B ⊗[R] κ(p) make M free over B. Choose a presentation 0 → K → Bⁿ → M → 0. As M is flat over R, the sequence stays exact after κ(p) ⊗[R] -, which is base change along B → B ⊗[R] κ(p); as the fibre of M is flat, it stays exact after a further base change to the residue field of B. So κ(B) ⊗[B] K → κ(B)ⁿ is injective, and Mathlib's Module.free_of_lTensor_residueField_injective shows that M is free. No Noetherian hypothesis is needed: finite presentation makes K finitely generated, which is what Nakayama's lemma uses.

The global statement localizes at the maximal ideals q of B. The localization B_q ⊗[B] M is still flat over R (Module.Flat.tensorProduct_of_flat), and its fibre over the prime of R below q is a base change of the fibre of M.

Main results

• Module.Free.of_flat_fiber: the criterion over a local ring, with freeness as conclusion.
• Module.Flat.of_flat_fiber: the criterion over an arbitrary ring.

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.
• The Stacks Project, Lemma 10.99.15 (Tag 00MP), the Noetherian version.

theorem Module.Free.of_flat_fiber {R : Type u_1} {B : Type u_2} {M : Type u_3} [CommRing R] [CommRing B] [Algebra R B] [AddCommGroup M] [Module R M] [Module B M] [IsScalarTower R B M] [IsLocalRing B] [FinitePresentation B M] [Flat R M] (h : Flat (TensorProduct R B (Ideal.comap (algebraMap R B) (IsLocalRing.maximalIdeal B)).ResidueField) (TensorProduct B (TensorProduct R B (Ideal.comap (algebraMap R B) (IsLocalRing.maximalIdeal B)).ResidueField) M)) : Free B M

The fibrewise criterion for flatness, local form. Let B be a local R-algebra and p the inverse image in R of the maximal ideal of B. A finitely presented B-module M which is flat over R, and whose fibre (B ⊗[R] κ(p)) ⊗[B] M is flat over B ⊗[R] κ(p), is free over B.

theorem Module.Flat.of_flat_fiber {R : Type u_1} {B : Type u_2} {M : Type u_3} [CommRing R] [CommRing B] [Algebra R B] [AddCommGroup M] [Module R M] [Module B M] [IsScalarTower R B M] [FinitePresentation B M] [Flat R M] (h : ∀ (p : Ideal R) [inst : p.IsPrime], Flat (TensorProduct R B p.ResidueField) (TensorProduct B (TensorProduct R B p.ResidueField) M)) : Flat B M

The fibrewise criterion for flatness. Let M be a finitely presented B-module which is flat over R. If for every prime p of R the fibre (B ⊗[R] κ(p)) ⊗[B] M is flat over the fibre ring B ⊗[R] κ(p), then M is flat over B.