Flat modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A module M over a commutative ring R is flat if for all finitely generated ideals I of R, the canonical map I ⊗ M →ₗ M is injective.

This is equivalent to the claim that for all injective R-linear maps f : M₁ → M₂ the induced map M₁ ⊗ M → M₂ ⊗ M is injective. See https://stacks.math.columbia.edu/tag/00HD. This result is not yet formalised.

Main declaration #

• module.flat: the predicate asserting that an R-module M is flat.

TODO #

• Show that tensoring with a flat module preserves injective morphisms. Show that this is equivalent to be flat. See https://stacks.math.columbia.edu/tag/00HD. To do this, it is probably a good idea to think about a suitable categorical induction principle that should be applied to the category of R-modules, and that will take care of the administrative side of the proof.
• Define flat R-algebras
• Define flat ring homomorphisms
  • Show that the identity is flat
  • Show that composition of flat morphisms is flat
• Show that flatness is stable under base change (aka extension of scalars) For base change, it will be very useful to have a "characteristic predicate" instead of relying on the construction A ⊗ B. Indeed, such a predicate should allow us to treat both A[X] and A ⊗ R[X] as the base change of R[X] to A. (Similar examples exist with fin n → R, R × R, ℤ[i] ⊗ ℝ, etc...)
• Generalize flatness to noncommutative rings.