generic-freeness.txt

The goal of this subsection is to give a simple and constructive proof of
Grothendieck's generic freeness lemma. A basic rendition of it is as follows:

\begin{quote}\emph{Generic freeness, first formulation.}
Let~$A$ be an integral domain. Let~$M$ be a finitely
generated~$A$-module. Then there exists a nonzero element~$f \in A$ such
that~$M[f^{-1}]$ is a finite free~$A[f^{-1}]$-module.
\end{quote}

The following more general version can be found, for instance, in the Stacks
Project~\stacksproject{051Z}.

\begin{quote}\emph{Generic freeness, second formulation.}
Let~$A$ be a reduced ring. Let~$M$ be a finitely
generated~$A$-module. Then there exists a dense open subset~$U \subseteq
\Spec(A)$ such that for any point~$x \in U$ there is an element~$f \in A$ such
that~$x \in D(f) \subseteq U$ and that the module~$M[f^{-1}]$ is a
finite free~$A[f^{-1}]$-module.
\end{quote}


However, the following form of the lemma \emph{can} be proven
intuitionistically:

\begin{quote}\emph{Generic freeness, third formulation.}
Let~$A$ be a reduced ring. Let~$M$ be a finitely generated~$A$-module.
Assume that~$f = 0$ is the only element of~$A$ such that~$M[f^{-1}]$ is a finite
free~$A[f^{-1}]$-module. Then~$A = 0$.
\end{quote}