Lemma 10.77.5. (Warning: see Remark 10.77.4.) Suppose $R$ is a local ring, and $M$ is a finite flat $R$-module. Then $M$ is finite free.

Proof. Follows from the equational criterion of flatness, see Lemma 10.38.11. Namely, suppose that $x_1, \ldots , x_ r \in M$ map to a basis of $M/\mathfrak mM$. By Nakayama's Lemma 10.19.1 these elements generate $M$. We want to show there is no relation among the $x_ i$. Instead, we will show by induction on $n$ that if $x_1, \ldots , x_ n \in M$ are linearly independent in the vector space $M/\mathfrak mM$ then they are independent over $R$.

The base case of the induction is where we have $x \in M$, $x \not\in \mathfrak mM$ and a relation $fx = 0$. By the equational criterion there exist $y_ j \in M$ and $a_ j \in R$ such that $x = \sum a_ j y_ j$ and $fa_ j = 0$ for all $j$. Since $x \not\in \mathfrak mM$ we see that at least one $a_ j$ is a unit and hence $f = 0$.

Suppose that $\sum f_ i x_ i$ is a relation among $x_1, \ldots , x_ n$. By our choice of $x_ i$ we have $f_ i \in \mathfrak m$. According to the equational criterion of flatness there exist $a_{ij} \in R$ and $y_ j \in M$ such that $x_ i = \sum a_{ij} y_ j$ and $\sum f_ i a_{ij} = 0$. Since $x_ n \not\in \mathfrak mM$ we see that $a_{nj}\not\in \mathfrak m$ for at least one $j$. Since $\sum f_ i a_{ij} = 0$ we get $f_ n = \sum _{i = 1}^{n-1} (-a_{ij}/a_{nj}) f_ i$. The relation $\sum f_ i x_ i = 0$ now can be rewritten as $\sum _{i = 1}^{n-1} f_ i( x_ i + (-a_{ij}/a_{nj}) x_ n) = 0$. Note that the elements $x_ i + (-a_{ij}/a_{nj}) x_ n$ map to $n-1$ linearly independent elements of $M/\mathfrak mM$. By induction assumption we get that all the $f_ i$, $i \leq n-1$ have to be zero, and also $f_ n = \sum _{i = 1}^{n-1} (-a_{ij}/a_{nj}) f_ i$. This proves the induction step. $\square$

There are also:

• 2 comment(s) on Section 10.77: Finite projective modules

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).