The Stacks project

Proof. Choose a generator $g$ for $I_ i(M^\bullet , f)$. Since $f^{r_ i} \in I_ i(M^\bullet , f)$ we see that $g$ divides a power of $f$. In particular $g$ is a nonzerodivisor in $A$. The $r_ i \times r_ i$-minors of the map $(f, d^ i) : M^ i \to M^ i \oplus M^{i + 1}$ generate the ideal $I_ i(M^\bullet , f)$ and the $(r_ i + 1) \times (r_ i + 1)$-minors of $(f, d^ i)$ are zero: we may check this after localizing at $f$ where the rank of the map is equal to $r_ i$. Consider the surjection

By Lemma 15.8.9 the module $Q$ is finite locally free of rank $r_{i + 1}$. Hence $Q$ is $f$-torsion free and we conclude the cokernel of $(f, d^ i)$ modulo $f$-power torsion is $Q$ as well.

Consider the complex of finite free $A$-modules

which becomes split exact after localizing at $f$. The map $(1, d^ i) : f^{i + 1}M^ i \to f^ iM^ i \oplus f^{i + 1}M^{i + 1}$ is isomorphic to the map $(f, d^ i) : M^ i \to M^ i \oplus M^{i + 1}$ we studied above. Hence the image

is isomorphic to $Q$ in particular projective. On the other hand, by construction of $\eta _ f$ in Section 15.95 the image of the injective map $(1, d^ i) : (\eta _ fM)^ i \to f^ iM^ i \oplus f^{i + 1}M^{i + 1}$ is the kernel of $(d^ i, -1)$. We conclude that we obtain an isomorphism $(\eta _ fM)^ i \oplus Q' = f^ iM^ i \oplus f^{i + 1}M^{i + 1}$ and we see that indeed $\eta _ fM^ i$ is finite locally free of rank $r_ i$ and that $(1, d^ i)$ is the inclusion of a direct summand. $\square$