Local criterion for injectivity over a Noetherian ring (source code)

= Local criterion for injectivity over a Noetherian ring
{title2=$M\text{ injective}\iff M_P\text{ injective for every prime }P$}

For a <Noetherian ring>, injectivity of a <module> can be tested at all prime localizations. By the <Baer criterion>, test $\operatorname{Ext}^1_R(R/J,M)$ for every <ideal> $J$. <Localization of Ext over a Noetherian ring> identifies its localization with the corresponding <ideal> test over $R_P$. Every <ideal> of $R_P$ is extended from its contraction, and <localization detects zero elements> applies to the resulting Ext <module> even when it is not finitely generated. These observations prove both directions.