1 Auslander-Buchsbaum-Serre Theorem

adfe develop some homological and element-wise machinery from Commutative Algebra, culminating in the proof of the Auslander-Buchsbaum-Serre theorem, and the corollary that the condition of being a regular ring localizes. This corollary is crucial for our proof of adjunction.

We follow Bruns-Herzog almost exclusively.

The current version of this blueprint is incomplete–this reflects the fact that we have not yet chosen which proof of Auslander-Buchsbaum-Serre to formalize.

In particular, there are two detailed by Bruns-Herzog: one uses a fact about Cohen-Macaulay rings for the forward direction, and a theorem of Ferrand-Vasconcelos for the reverse direction. The other uses Koszul homology and some facts about Tor for the forward direction, and a statement of Serre on DG-algebras for the reverse direction. We can basically pick and choose which proof we want to use for each direction.