Flat modules

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.

class Module.Flat (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Prop

• out : ∀ ⦃I : Ideal R⦄, Ideal.FG I → Function.Injective ↑(TensorProduct.lift (LinearMap.comp (LinearMap.lsmul R M) (Submodule.subtype I)))

An R-module M is flat if for all finitely generated ideals I of R, the canonical map I ⊗ M →ₗ M is injective.

instance Module.Flat.self (R : Type u) [CommRing R] : Module.Flat R R