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-ideal I into R tensored on the left with M is injective. For this consider the composition of natural maps

M ⊗[R] I ≃ M ⊗[S] (S ⊗[R] I) ≃ M ⊗[S] J → M ⊗[S] S ≃ M ≃ M ⊗[R] R

where J is the image of S ⊗[R] I under the (by flatness of S) injective map S ⊗[R] I → S. One checks that this composition is precisely I → R tensored on the left with M and it is injective as a composition of injective maps (note that M ⊗[S] J → M ⊗[S] S is injective because M is S-flat).

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

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

@[deprecated Module.Flat.trans]

theorem Module.Flat.comp (R : Type u) (S : Type v) (M : Type w) [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Flat R S] [Module.Flat S M] : Module.Flat R M

Alias of Module.Flat.trans.

---

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. To show that S ⊗[R] M is S-flat, we consider for an ideal I in S the composition of natural maps

I ⊗[S] (S ⊗[R] M) ≃ I ⊗[R] M → S ⊗[R] M ≃ S ⊗[S] (S ⊗[R] M).

One checks that this composition is precisely the inclusion I → S tensored on the right with S ⊗[R] M and that the former is injective (note that I ⊗[R] M → S ⊗[R] M is injective, since M is R-flat).

instance Module.Flat.baseChange (R : Type u) (S : Type v) (M : Type w) [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] [Module.Flat R M] : Module.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) [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] [Module.Flat R M] (N : Type t) [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) : Module.Flat S N

A base change of a flat module is flat.

instance Module.Flat.localizedModule {R : Type u} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] (S : Submonoid R) : Module.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) [CommRing R] [AddCommGroup M] [Module R M] [CommRing Rp] [Algebra R Rp] [AddCommGroup Mp] [Module R Mp] [Module Rp Mp] [IsScalarTower R Rp Mp] [Module.Flat R M] (S : Submonoid R) [IsLocalization S Rp] (f : M →ₗ[R] Mp) [h : IsLocalizedModule S f] : Module.Flat Rp Mp