Flatness is stable under composition and base change

We show that flatness is stable under composition and base change.

Main theorems

• Module.Flat.comp: if S is a flat R-algebra and M is a flat S-module, then M is a flat R-module
• Module.Flat.baseChange: if M is a flat R-module and S is any R-algebra, then S ⊗[R] M is S-flat.
• Module.Flat.of_isLocalizedModule: if M is a flat R-module and S is a submonoid of R then the localization of M at S is flat as a module for the localization of R at S.

Composition

Let R be a ring, S a flat R-algebra and M a flat S-module. To show that M is flat as an R-module, we show that the inclusion of an R-submodule N into an R-module P tensored on the left with M is injective. For this consider the composition of natural maps

M ⊗[R] N ≃ M ⊗[S] (S ⊗[R] N) → M ⊗[S] (S ⊗[R] P) ≃ M ⊗[R] P;

S ⊗[R] N → S ⊗[R] P is injective by R-flatness of S, so the middle map is injective by S-flatness of M.

theorem Module.Flat.trans (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Flat R S] [Flat S M] : Flat R M

If S is a flat R-algebra, then any flat S-Module is also R-flat.

Base change

Let R be a ring, M a flat R-module and S an R-algebra, then S ⊗[R] M is a flat S-module. This is a special case of Module.Flat.instTensorProduct.

instance Module.Flat.baseChange (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Flat R M] : Flat S (TensorProduct R S M)

If M is a flat R-module and S is any R-algebra, S ⊗[R] M is S-flat.

theorem Module.Flat.isBaseChange (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Flat R M] (N : Type t) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) : Flat S N

A base change of a flat module is flat.

instance Module.Flat.localizedModule {R : Type u} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [Flat R M] (S : Submonoid R) : Flat (Localization S) (LocalizedModule S M)

theorem Module.Flat.of_isLocalizedModule {R : Type u} {M : Type u_1} {Mp : Type u_2} (Rp : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring Rp] [Algebra R Rp] [AddCommMonoid Mp] [Module R Mp] [Module Rp Mp] [IsScalarTower R Rp Mp] [Flat R M] (S : Submonoid R) [IsLocalization S Rp] (f : M →ₗ[R] Mp) [h : IsLocalizedModule S f] : Flat Rp Mp