The local criterion for flatness

Let R be a Noetherian ring, S a Noetherian R-algebra, M a finite S-module and I an ideal of R whose extension I S lies in the Jacobson radical of S. If I ⊗[R] M → M is injective, that is Tor₁ᴿ(R ⧸ I, M) = 0, and M ⧸ I M is flat over R ⧸ I, then M is flat over R (Module.Flat.of_subtype_rTensor_injective). This is the local criterion for flatness (Stacks, Tag 00MK), stated with the Jacobson radical in place of a local homomorphism of local rings. For a local homomorphism R → S and I the maximal ideal of R, the quotient M ⧸ I M is a vector space over the residue field, so flatness of M reduces to the vanishing of Tor₁ᴿ(κ, M). In its infinitesimal form the criterion needs no Tor₁ hypothesis: M is flat over R as soon as M ⧸ Iⁿ M is flat over R ⧸ Iⁿ for every n (Module.Flat.of_forall_flat_quotient_pow), and conversely these quotients are flat when M is (Module.Flat.quotient_smul_top). This form applies when M is only known modulo powers of I, as for the completion of a ring that is flat over R but not yet known to be Noetherian.

Two special cases are derived.

• A regular element (Stacks, Tag 00ML, for the ideal (x)). If x ∈ R is M-regular, then Tor₁ᴿ(R ⧸ (x), M) = 0 (IsSMulRegular.span_singleton_subtype_rTensor_injective), so M is flat over R as soon as M ⧸ x M is flat over R ⧸ (x) (Module.Flat.of_flat_quotSMulTop). Conversely M ⧸ x M is flat over R ⧸ (x) whenever M is flat over R, so for an M-regular x the two conditions are equivalent (Module.flat_quotSMulTop_iff_flat), the flat counterpart of Mathlib's Module.free_quotSMulTop_iff_free. This is the inductive step of miracle flatness (Stacks, Tag 00R4).
• Flatness over the fibres (Stacks, Tag 00MP). Let R → S → T be ring maps with S and T Noetherian, M a finite T-module flat over R, and J an ideal of R with J T in the Jacobson radical of T. Flatness over R already gives Tor₁ˢ(S ⧸ J S, M) = 0 (Module.Flat.map_subtype_rTensor_injective, in TauCeti.RingTheory.Ideal.TensorProduct), so M is flat over S as soon as M ⧸ J M is flat over S ⧸ J S (Module.Flat.of_flat_quotient_map). For local rings and J the maximal ideal of R, the fibre condition holds automatically when J S is the maximal ideal of S; in ring homomorphism form, f : S → T is flat as soon as f ∘ g is, for some g : R → S with 𝔪_R S = 𝔪_S (RingHom.Flat.of_comp_of_map_maximalIdeal_eq). The typical g is the map to the completion of a Noetherian local ring, which transports flatness of an endomorphism such as Frobenius to the completion.

Iterating the criterion along a sequence gives a flatness test for a local homomorphism R → S of Noetherian local rings: if r₁, …, rₙ generate the maximal ideal of R and their images form a weakly S-regular sequence, then S is flat over R (Module.Flat.of_isWeaklyRegular_map_algebraMap). Dividing by r₁ on both sides preserves the hypotheses, and for n = 0 the ring R is a field. The test needs no regularity of R or Cohen–Macaulayness of S; these are only ways of producing the regular sequence. For instance, the Frobenius endomorphism of a regular local ring of characteristic p sends a regular system of parameters to their p-th powers, again a regular sequence, which proves Kunz's theorem (TauCeti.IsRegularLocalRing.flat_frobenius). The ring homomorphism form RingHom.Flat.of_isWeaklyRegular_map applies to such endomorphisms without an algebra structure of a ring over itself.

A related criterion runs along a regular element of the algebra rather than of the base (compare Matsumura, Commutative Ring Theory, §22, for local homomorphisms of Noetherian local rings). If S is Noetherian, M is a finite S-module, x ∈ S lies in the Jacobson radical of S and is M-regular, and M ⧸ x M is flat over R, then M is flat over R (Module.Flat.of_flat_quotSMulTop_of_isSMulRegular). No Noetherian hypothesis on R is needed: the kernel of M ⊗[R] I → M ⊗[R] R is a finite S-module equal to x times itself, so it vanishes by Nakayama's lemma.

Implementation notes

By Mathlib's ideal criterion it suffices that J ⊗[R] M → M is injective for every ideal J.

Steps 1–3 hold without Noetherian hypotheses and live in TauCeti.RingTheory.Flat.TensorProduct.

1. Tensoring with M preserves injectivity of maps between modules killed by I: over R ⧸ I this is flatness of M ⧸ I M (Ideal.rTensor_injective_of_isTorsionBySet).
2. If L ⧸ N is killed by I, then N ⊗[R] M → L ⊗[R] M is injective, by a chase along a free module covering L (Ideal.subtype_rTensor_injective_of_smul_top_le).
3. By induction, the same holds when L ⧸ N is killed by Iⁿ (Ideal.subtype_rTensor_injective_of_pow_smul_top_le). Applied to J ⧸ (J ⊓ Iⁿ) inside R ⧸ Iⁿ, it shows that the kernel of J ⊗[R] M → M comes from (J ⊓ Iⁿ) ⊗[R] M (Ideal.mem_range_rTensor_inclusion_inf_pow).
4. By the Artin–Rees lemma J ⊓ Iⁿ ⊆ I^(n - c) J, so an element t of the kernel lies in I^(n - c) (J ⊗[R] M) for all n. Its image in M ⊗[R] J, a finite S-module (Module.Finite.tensor), therefore vanishes by Krull's intersection theorem over S.

For the infinitesimal form, step 3 is replaced by flatness of M ⧸ Iⁿ M over R ⧸ Iⁿ (Ideal.mem_range_rTensor_inclusion_inf_of_flat), and step 4 is unchanged.

Main results

• Module.Flat.of_subtype_rTensor_injective: the local criterion for flatness.
• Module.Flat.of_forall_flat_quotient_pow: the infinitesimal form of the local criterion; Module.flat_iff_forall_flat_quotient_pow is the equivalence.
• Module.Flat.quotient_smul_top: M ⧸ I M is flat over R ⧸ I when M is flat over R.
• Module.Flat.of_flat_quotient_map: the criterion for flatness over the fibres.
• RingHom.Flat.of_comp_of_map_maximalIdeal_eq: f is flat if f ∘ g is flat and g maps the maximal ideal onto the maximal ideal.
• Module.Flat.of_flat_quotSMulTop: the criterion along a regular element.
• Module.Flat.quotSMulTop: M ⧸ x M is flat over R ⧸ (x) when M is flat over R.
• Module.flat_quotSMulTop_iff_flat: for an M-regular x as above, M ⧸ x M is flat over R ⧸ (x) if and only if M is flat over R.
• Module.Flat.of_flat_quotSMulTop_of_isSMulRegular: the criterion along a regular element of the algebra S.
• Module.Flat.of_isWeaklyRegular_map_algebraMap: a local homomorphism R → S of Noetherian local rings is flat if generators of the maximal ideal of R map to a weakly S-regular sequence; RingHom.Flat.of_isWeaklyRegular_map is the same for a ring homomorphism.

References

• The Stacks Project, Tag 00MK, the local criterion for flatness, and Tag 00ML, its variant along a regular element.
• The Stacks Project, Tag 00MP, flatness over the fibres.
• The Stacks Project, Tag 00R4, miracle flatness, whose proof uses the criterion along a regular element.
• H. Matsumura, Commutative Ring Theory, Theorems 22.3 and 22.5.

instance Module.Flat.quotSMulTop {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] (x : R) : Flat (R ⧸ Ideal.span {x}) (QuotSMulTop x M)

If M is flat over R, then M ⧸ x M is flat over R ⧸ (x).

instance Module.Flat.quotient_smul_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] (I : Ideal R) : Flat (R ⧸ I) (M ⧸ I • ⊤)

If M is flat over R, then M ⧸ I M is flat over R ⧸ I.

The local criterion

theorem Module.Flat.of_forall_flat_quotient_pow {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] {S : Type u_3} [CommRing S] [IsNoetherianRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Module.Finite S M] {I : Ideal R} (hIS : Ideal.map (algebraMap R S) I ≤ ⊥.jacobson) (hflat : ∀ (n : ℕ), Flat (R ⧸ I ^ n) (M ⧸ I ^ n • ⊤)) : Flat R M

Local criterion for flatness, infinitesimal form (Matsumura, Theorem 22.3, (4) ⇒ (1)). Let R and S be Noetherian, M a finite S-module and I an ideal of R with I S in the Jacobson radical of S. If M ⧸ I ^ n M is flat over R ⧸ I ^ n for every n, then M is flat over R.

theorem Module.flat_iff_forall_flat_quotient_pow {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] {S : Type u_3} [CommRing S] [IsNoetherianRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Module.Finite S M] {I : Ideal R} (hIS : Ideal.map (algebraMap R S) I ≤ ⊥.jacobson) : Flat R M ↔ ∀ (n : ℕ), Flat (R ⧸ I ^ n) (M ⧸ I ^ n • ⊤)

Under the hypotheses of Module.Flat.of_forall_flat_quotient_pow, M is flat over R if and only if M ⧸ I ^ n M is flat over R ⧸ I ^ n for every n.

theorem Module.Flat.of_subtype_rTensor_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} [Flat (R ⧸ I) (M ⧸ I • ⊤)] [IsNoetherianRing R] {S : Type u_3} [CommRing S] [IsNoetherianRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Module.Finite S M] (hIS : Ideal.map (algebraMap R S) I ≤ ⊥.jacobson) (hI : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))) : Flat R M

Local criterion for flatness (Stacks, Tag 00MK). Let R and S be Noetherian, M a finite S-module and I an ideal of R with I S in the Jacobson radical of S. If I ⊗[R] M → M is injective, that is Tor₁ᴿ(R ⧸ I, M) = 0, and M ⧸ I M is flat over R ⧸ I, then M is flat over R.

theorem Module.Flat.of_flat_quotient_map {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u_3} {T : Type u_4} [CommRing S] [IsNoetherianRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [CommRing T] [IsNoetherianRing T] [Algebra S T] [Module T M] [IsScalarTower S T M] [Module.Finite T M] [Flat R M] {J : Ideal R} (hJ : Ideal.map (algebraMap S T) (Ideal.map (algebraMap R S) J) ≤ ⊥.jacobson) [Flat (S ⧸ Ideal.map (algebraMap R S) J) (M ⧸ Ideal.map (algebraMap R S) J • ⊤)] : Flat S M

Flatness over the fibres (Stacks, Tag 00MP). Let R → S → T be ring maps with S and T Noetherian, let M be a finite T-module which is flat over R, and let J be an ideal of R with J T in the Jacobson radical of T. If M ⧸ J M is flat over S ⧸ J S, then M is flat over S.

Along a regular element

theorem Module.Flat.of_flat_quotSMulTop {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : R} [IsNoetherianRing R] {S : Type u_3} [CommRing S] [IsNoetherianRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Module.Finite S M] (hx : (algebraMap R S) x ∈ ⊥.jacobson) (reg : IsSMulRegular M x) [Flat (R ⧸ Ideal.span {x}) (QuotSMulTop x M)] : Flat R M

Local criterion for flatness along a regular element (Stacks, Tag 00ML, for the ideal (x)). Let R and S be Noetherian, M a finite S-module and x ∈ R with image in the Jacobson radical of S. If x is M-regular and M ⧸ x M is flat over R ⧸ (x), then M is flat over R.

theorem Module.Flat.of_flat_quotSMulTop_of_isLocalHom {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : R} [IsLocalRing R] [IsNoetherianRing R] {S : Type u_3} [CommRing S] [IsLocalRing S] [IsNoetherianRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [Module S M] [IsScalarTower R S M] [Module.Finite S M] (hx : x ∈ IsLocalRing.maximalIdeal R) (reg : IsSMulRegular M x) [Flat (R ⧸ Ideal.span {x}) (QuotSMulTop x M)] : Flat R M

Local criterion for flatness along a regular element, for a local homomorphism R → S of Noetherian local rings (Stacks, Lemma 10.99.10 (00ML), for the ideal (x)): if x lies in the maximal ideal of R, is M-regular, and M ⧸ x M is flat over R ⧸ (x), then the finite S-module M is flat over R.

theorem Module.flat_quotSMulTop_iff_flat {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : R} [IsNoetherianRing R] {S : Type u_3} [CommRing S] [IsNoetherianRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Module.Finite S M] (hx : (algebraMap R S) x ∈ ⊥.jacobson) (reg : IsSMulRegular M x) : Flat (R ⧸ Ideal.span {x}) (QuotSMulTop x M) ↔ Flat R M

For an M-regular element x as in Module.Flat.of_flat_quotSMulTop, M ⧸ x M is flat over R ⧸ (x) if and only if M is flat over R.

Along a regular element of the algebra

theorem Module.Flat.of_flat_quotSMulTop_of_isSMulRegular {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u_3} [CommRing S] [IsNoetherianRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Module.Finite S M] {x : S} (hx : x ∈ ⊥.jacobson) (reg : IsSMulRegular M x) [Flat R (QuotSMulTop x M)] : Flat R M

Flatness along a regular element of the algebra. Let S be a Noetherian R-algebra, M a finite S-module and x an M-regular element of the Jacobson radical of S. If M ⧸ x M is flat over R, then so is M. Unlike Module.Flat.of_flat_quotSMulTop, the element x need not come from R, and R need not be Noetherian.

theorem RingHom.Flat.of_comp_of_map_maximalIdeal_eq {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [IsNoetherianRing S] [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (g : R →+* S) (f : S →+* T) [IsLocalHom f] (hfg : (f.comp g).Flat) (hg : Ideal.map g (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S) : f.Flat

Let g : R → S and f : S → T be ring homomorphisms of local rings, with S and T Noetherian and f local. If f ∘ g is flat and g maps the maximal ideal of R onto a generating set of the maximal ideal of S, then f is flat. This is flatness over the fibres (Module.Flat.of_flat_quotient_map), whose fibre condition holds because S ⧸ 𝔪_R S is a field. Unlike the module version, it applies to endomorphisms such as Frobenius.

theorem Module.Flat.of_isWeaklyRegular_map_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [CommRing S] [IsLocalRing S] [IsNoetherianRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {rs : List R} (hrs : Ideal.ofList rs = IsLocalRing.maximalIdeal R) (hreg : RingTheory.Sequence.IsWeaklyRegular S (List.map (⇑(algebraMap R S)) rs)) : Flat R S

Flatness from a regular sequence. Let R → S be a local homomorphism of Noetherian local rings. If r₁, …, rₙ generate the maximal ideal of R and their images form a weakly S-regular sequence, then S is flat over R. This iterates the local criterion Module.Flat.of_flat_quotSMulTop_of_isLocalHom along the sequence.

theorem RingHom.Flat.of_isWeaklyRegular_map {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [CommRing S] [IsLocalRing S] [IsNoetherianRing S] (f : R →+* S) [IsLocalHom f] {rs : List R} (hrs : Ideal.ofList rs = IsLocalRing.maximalIdeal R) (hreg : RingTheory.Sequence.IsWeaklyRegular S (List.map (⇑f) rs)) : f.Flat

Flatness from a regular sequence, for a local homomorphism f : R →+* S of Noetherian local rings: if r₁, …, rₙ generate the maximal ideal of R and f r₁, …, f rₙ is a weakly S-regular sequence, then f is flat. Unlike Module.Flat.of_isWeaklyRegular_map_algebraMap, this applies to endomorphisms, such as Frobenius, without an algebra structure of R over itself.