Lemma 10.78.5. (Warning: see Remark 10.78.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.39.11. Namely, suppose that $x_1, \ldots , x_ r \in M$ map to a basis of $M/\mathfrak mM$. By Nakayama's Lemma 10.20.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$
Post a comment
Your email address will not be published. Required fields are marked.
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).
All contributions are licensed under the GNU Free Documentation License.
Comments (0)
There are also: