Structures · Algebra

Module.Flat

An R-module M is flat if for every finitely generated submodule N of every finitely generated R-module P in the same universe as R, the canonical map N ⊗ M → P ⊗ M is injective. This implies the same is true for arbitrary R-modules N and P and injective linear maps N →ₗ[R] P, see Flat.rTensor_preserves_injective_linearMap. To show a module over a ring R is flat, it suffices to consider the case P = R, see Flat.iff_rTensor_injective.

Defined in

Mathlib.RingTheory.Flat.Basic

Shape

2 explicit arguments · adds out