Lemma 15.90.4. Let $R$ be a ring, let $f \in R$, and let $R \to R'$ be a ring map which induces isomorphisms $R/f^ nR \to R'/f^ nR'$ for $n > 0$. An $R$-module $M$ is finitely generated if and only if the ($R' \oplus R_ f$)-module $M \otimes _ R (R' \oplus R_ f)$ is finitely generated. For example, if $M \otimes _ R (R^\wedge \oplus R_ f)$ is finitely generated as a module over $R^\wedge \oplus R_ f$, then $M$ is a finitely generated $R$-module.
Slight generalization of [Lemme 2(a), Beauville-Laszlo].
Proof. The ‘only if' is clear, so we assume that $M \otimes _ R (R' \oplus R_ f)$ is finitely generated. In this case, by writing each generator as a sum of simple tensors, $M \otimes _ R (R' \oplus R_ f)$ admits a finite generating set consisting of elements of $M$. That is, there exists a morphism from a finite free $R$-module to $M$ whose cokernel is killed by tensoring with $R' \oplus R_ f$; we may thus deduce $M$ is finite generated by applying Lemma 15.90.2 to this cokernel. The last statement is a special case of the first statement by Lemma 15.90.1. $\square$
Comments (2)
Comment #3823 by Kestutis Cesnavicius on
Comment #3926 by Johan on
There are also: