Proof explanation) Finite injective dimension of the residue field of a Noetherian local ring implies regularity

Question

I am trying to prove:

Let $(R,\mathfrak m,k)$ be a Noetherian local ring. If $\operatorname{inj dim}_R k$ is finite, then $R$ is regular.

In this link: Finite injective dimension of the residue field implies that the ring is regular, there is a proof using induction on $\dim R$, and there is a point which I can't understand. Since the answer given in the link is quite old, I've made a new post.

My question is:

1. The answer says that use Theorem 3.1.17 to deduce $\operatorname{inj dim} \mathfrak{m}=0$. But to use Theorem 3.1.17 we need that $\mathfrak{m}$ has finite injective dimension. How do we know that $\mathfrak{m}$ has finite injective dimension?

2. How does the result that $\mathfrak{m}$ is a direct summand of $R$ imply that $\mathfrak{m}=0$?

3. As given in the answer, I am able to show that $\operatorname{inj dim}\mathfrak{m}/(x)<\infty$. But how should we apply this result to use the induction hypothesis?

Answer 1

While I cannot speak for a different user's intent, I have some suggestions for how to fill in the details.

1 and 2. We want to show that $\mathfrak m=0$ in case $\dim R=0$ and $k$ has finite injective dimension. Note that $k$ is an injective module over $R$, by Theorem 3.1.17. Applying the exact functor $\hom_R(-,k)$ to the short exact sequence $0\to \mathfrak m\to R \to k \to 0$, the following is an exact sequence $$0\to\hom_R(k,k)\to\hom_R(R,k)\to\hom_R(\mathfrak m,k)\to 0$$ The map $\hom_R(k,k)\to\hom_R(R,k)$ is nonzero. Also, both $\hom_R(k,k)$ and $\hom_R(R,k)$ are isomorphic to $k$. It follows that $$\hom_R(\mathfrak m/\mathfrak m^2,k)\cong\hom_R(\mathfrak m,k)=0$$Applying Nakayama's lemma, we deduce $\mathfrak m=0$.

(Note that one can prove $\mathfrak m$ is injective by taking an injective hull and using Theorem 3.2.8, then $\mathfrak m=0$ follows from the fact that $0\to \mathfrak m\to R \to k\to 0$ is split exact.)

${}$3. This follows a suggestion in the comments as it seems to be clearer than the approach in the linked answer. Let $d=\dim R$ and $x\in\mathfrak m/\mathfrak m^2$ a non-zero divisor. Applying Lemma 3.1.16 (and its proof), we have isomorphisms$$\operatorname{Ext}_{R/xR}^i(k,\mathfrak m/xR)\cong \operatorname{Ext}_R^{i+1}(k,\mathfrak m)\quad\text{and}\quad \operatorname{Ext}_{R/xR}^i(k,R/xR)\cong\operatorname{Ext}_R^{i+1}(k,R)$$for all $i\ge 0$. Moreover, Proposition 3.1.14 and the fact that $\operatorname{inj dim}_Rk<\infty$ implies $$\operatorname{Ext}_R^i(k,\mathfrak m)\cong\operatorname{Ext}_R^i(k,R)\qquad(i\gg 0)$$Thus, in the long exact sequence associated to $0\to \mathfrak m/xR\to R/xR\to k\to 0$ we have isomorphisms$$\operatorname{Ext}_{R/xR}^i(k,\mathfrak m/xR)\xrightarrow{\sim}\operatorname{Ext}_{R/xR}^i(k,R/xR)\qquad(i\gg 0)$$and this forces $$\operatorname{Ext}_{R/xR}^i(k,k)=0\qquad(i\gg0)$$which means $k$ has a finite injective dimension over $R/xR$. The induction hypothesis implies $R/xR$ is regular. Hence, there exist $x_1,\dots,x_{d-1}\in\mathfrak m$ such that their images $\overline x_1,\dots,\overline x_{d-1}$ in $\mathfrak m/xR$ comprise a system of generators for $\mathfrak m/xR$. So, $\mathfrak m$ is generated by $x_1,\dots,x_{d-1},x$ and thus $R$ is regular.