Flatness is stable under composition and base change

We show that flatness is stable under composition and base change. The latter is not formalized yet.

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

TODO

• Show that flatness is stable under base change, i.e. if S is any R-algebra and M is a flat R-module, then M ⊗[R] S is a flat S-module.

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 the former is injective as a composition of injective maps (note that M ⊗[S] S → M is injective because M is S-flat).

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

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