# 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.

- 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.