Blueprint for the Adjunction Formula

1.10 Auslander-Buchsbaum Formula

Lemma 1.10.1
#

BH 1.3.4

Proof ▼

Uses

* def of associated primes

* a fact about associated primes giving and embedding

* some facts about commutative squares (maybe already in lean?)

* tensor products of modules

* Nakayama (a corollary, like Atiyah-MacDonald 2.8 but uses maps, might just follow from AM 2.8)

Lemma 1.10.2
#

BH 1.3.5

Proof ▼

This uses

* BH 1.1.5

* The "tor" characterization of projective dimension

Theorem 1.10.3
#

depth + projdim = depth

Proof ▼