Documentation

Mathlib.RingTheory.Flat

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) [] [] [Module R M] :
• out : ∀ ⦃I : ⦄,

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

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