Let be a Noetherian local ring, and let be a finite -module. When has finite projective dimension over , we have the remarkable equality

This is the famous *Auslander-Buchsbaum formula*, and is one of my favorite tools in commutative algebra. In this post I want to record the following innocent application of Auslander-Buchsbaum, which I found in September 2011 but didn’t have any use for until recently.

**Proposition. ***Let be a Noetherian local ring, an ideal of , and a finite -module. Then*

*whenever both number on the right-hand side are finite.*

*Proof.* Supposing , a direct construction with complexes yields a finite resolution of by finite free -modules, so as well.

Now, a sequence is -regular if and only if is -regular, so the -depth and the -depth of are equal. Equating the Auslander-Buchsbaum formulas for over and then yields the equality

Rearranging, we compute

where the second line follows from the equality , and the third line follows from another application of the Auslander-Buchsbaum formula, which is allowed by our assumption that .

**Theorem.*** Let be a regular local ring, and let be a finite -module of projective dimension . Then the following are equivalent:*

**i. **,

**ii. ***,*

**iii. *** is a regular local ring of dimension , and is free over .*

*Proof. *It’s trivial to check that iii. implies ii. implies i. We prove that i. implies iii. By hypothesis, we may choose elements of whose reductions modulo are linearly independent over ; set . By e.g. Theorem 14.2 of Matsumura, the elements form a subset of a regular system of parameters for , and so the ring is regular of dimension . Furthermore, we have . To see this, note that since regular local rings are Cohen-Macaulay, Theorem 17.4 of Matsumura implies that is an -regular sequence, so the Koszul complex yields a minimal projective resolution of length . Now, the -module structure of naturally factors through the map , and applying the previous Proposition, we find

so is projective and hence free over . Since is also a faithful module over , the natural surjection is necessarily an isomorphism.