Projective coherent duality over a regular local base

Given: A regular Noetherian local ring $R$ of dimension $d$, a projective $R$-scheme $X$ with a fixed closed immersion $i\text{\hspace{0.17em}⁣}:X\hookrightarrow P={\mathbb{P}}_R^N$, the complex $D_X=i^{!}({\mathcal{O}}_P(-N-1)[N+d])$, and a bounded coherent complex $K$ on $X$.

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-dualizing-complex-on-projective-cm-scheme. A dualizing complex on a Noetherian scheme $X$ is an object $D_X\in D_{\mathrm{C}\mathrm{o}\mathrm{h}}^b(X)$ such that, locally on affine open neighborhoods $U=\mathrm{Spec}B$, its corresponding complex has finite injective dimension over $B$ and the homothety map $B\to R{\mathrm{Hom}}_B(D_X{\mathrm{\mid }}_U,D_X{\mathrm{\mid }}_U)$ is an isomorphism. (Dualizing complexes and the normalized dualizing sheaf on a projective CM scheme)

lem-relative-projective-space-derived-duality-regular-local-base. Assume AC and DC. Let $R$ be regular Noetherian local of finite dimension and $P={\mathbb{P}}_R^N$. Write $W={\mathcal{O}}_P(-N-1)$. Laurent residue gives $t:R\mathrm{\Gamma }(P,W[N])\to R$. For every $K\in D_{\mathrm{C}\mathrm{o}\mathrm{h}}^b(P)$, evaluation followed by $t$ gives a natural quasi-isomorphism $R\mathrm{\Gamma }(P,\mathcal{R}\text{\hspace{0.17em}⁣}Ho{m}_P(K,W[N]))\cong R{\mathrm{Hom}}_R(R\mathrm{\Gamma }(P,K),R)$. (Relative derived duality on projective space over a regular local ring)

lem-finite-closed-immersion-derived-coinduction-adjunction. Assume AC. For a finite homomorphism $A\to B$ of Noetherian rings and $G\in D^{+}(A)$, the complex $f^{!}G=R{\mathrm{Hom}}_A(B,G)$ has its natural $B$-action and is right adjoint to restriction of scalars. (Derived adjunction for finite rings and closed immersions)

lem-regular-quotient-dualizing-complex-and-biduality. Assume AC. Let $A$ be a regular Noetherian ring of finite dimension $n$, let $L$ be an invertible $A$-module, and let $B=A\mathrm{/}I$ be nonzero. For any integer $s$, $D_B=R{\mathrm{Hom}}_A(B,L[s])$ is a dualizing complex over $B$. (Dualizing complexes and coherent biduality for regular-ring quotients)

thm-localisation-and-polynomial-extension-of-regular-rings. Assume the Axiom of Choice (The Axiom of Choice). Localizations and finite polynomial extensions of a commutative regular Noetherian ring are regular. Regularity can equivalently be tested at maximal ideals. For every nonzero such ring, $\mathrm{gldim}R=\dim R$, allowing infinity. (localisation and polynomial extension of regular rings)

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)