Finite-length duality over a regular local base

Given: A regular Noetherian local ring $(R,\mathfrak{m})$ of dimension $d$, a module-finite local $R$-algebra $(B,\mathfrak{n})$, and finite-length $B$-modules $M$.

def-axiom-of-choice. The Axiom of Choice (AC) is the following statement. > Every family of nonempty sets has a choice function > (def-choice-function). Written out: for every set $\mathcal{F}$ all of whose members are nonempty, there exists a function $g$ with domain $\mathcal{F}$ satisfying $g(S)\in S$ for all $S\in \mathcal{F}$. (The Axiom of Choice)

def-dependent-choice. Let $X$ be a set and let $R\subseteq X\times X$ be a binary relation on $X$. Call $R$ entire on $X$ when $\text{for every }x\in X\text{ there is }y\in X\text{ with }xRy\mathrm{.}$ The Axiom of Dependent Choice, written $\mathrm{D}\mathrm{C}$, is the following statement. (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain)

cor-koszul-complex-resolves-a-regular-quotient. If $M$ is finite free and $\mathbf{x}$ is $M$-regular, then $K(\mathbf{x};M)$ is a finite free resolution of $M\mathrm{/}(\mathbf{x})M$. (Koszul Complex Resolves A Regular Quotient)

thm-regular-local-rings-are-domains-and-cohen-macaulay. Assume the Axiom of Choice (The Axiom of Choice). A regular local ring $R$ of dimension $d$ is a domain and Cohen–Macaulay. For every regular system $(x_1,\dots ,x_d)$, the tuple is $R$-regular and $R\mathrm{/}(x_1,\dots ,x_c)$ is regular local of dimension $d-c$ for all $0\le c\le d$. (regular local rings are domains and cohen macaulay)

thm-long-exact-ext-sequence-in-the-first-variable. Assume the Axiom of Dependent Choice. Let $\mathcal{A}$ be abelian with enough projectives and enough injectives, and fix supplied projective and injective resolution data on all its objects. (The long exact Ext sequence in the first variable)

lem-finite-regular-base-algebra-dualizing-biduality. Assume AC and DC. Let $R$ be a regular Noetherian ring of finite dimension $d$, and let $B\mathrm{\ne }0$ be a module-finite $R$-algebra. For any integer $s$, $D_B=R{\mathrm{Hom}}_R(B,R[s])$ is a dualizing complex over $B$. (Dualizing biduality for finite algebras over a regular base)