The Stacks project

It might be better to add a citation for the sentence "Then clearly $R$ is a discrete valuation ring." I think it's regular+dimension 1 (Tag 00PD (3)). (At least this was not clear to me at first glance, I wondered quite a while around noetherianness.)

Thanks for catching this! No you can't get this immediately from Lemma 10.119.7 because indeed you don't know that it is Noetherian (a priori). And indeed right now I don't see why $\bigcap p^nR = 0$ (with $R$ as in the proof). I fixed it by completing first. Unfortunately now the proof is rather long and I feel it doesn't do justice to what's really going on. Anway, the changes can be viewed here.

The original version (as far as I know) of Lemma 03C3 [EGA, ($\mathbf{0}_{III}$.10.3.1)] applies only to Noetherian base rings but shows that the extension is then also Noetherian. (That the Noether property is preserved in (the full version of) 03C3 is also embedded in [Bourbaki, Algèbre Commutative, Ch. X, Appendice].)

This gives immediately that R in the proof is a DVR (using also Lemma 031E). But of course the preservation of Noetherian property needs to go somewhere (in EGA it also goes via completion).

Should have checked before posting #7784 above: the preservation of the Noetherian property (as well as being a DVR) is in [EGA I 2nd ed., ($\mathbf{0}_{I}$.6.8.3)]. The proof is a quick lemma ((6.8.3.1), loc.cit.).

Dear Juhani, thank you for mentioning this.

Why is $R\to \Lambda$ flat (in the fifth sentence of the proof)？It seems like Tag 00MB (Lemma 10.97.2, as of 2025-10-18) only works when $R$ is Noetherian. However, as you discussed above, we don't know until the very end whether P is Noetherian, do we？ Am I misunderstanding how to apply Lemma 00MB here?

Sorry, I made a typo. The P in the third sentence of the comment above stands for $R$.

I apologize for posting multiple times. I thought we could prove that $\dim \Lambda \geq 1$ without knowing that $R\to \Lambda$ is flat. Since $\mathbb{Z}_{p}\to R$ is flat, for any $k$, $\mathbb{Z}/p^k\mathbb{Z} \to R/p^kR$ is injective. By Tag 05GG, for any $k$, it holds that $R/p^kR \cong \Lambda/p^k\Lambda$. In particular, for any $k$, it holds that $\mathbb{Z}/p^k\mathbb{Z} \subset R/p^kR \cong \Lambda/p^k\Lambda$. By passing to the limit, we conclude that $\mathbb{Z}_{p}\to\Lambda$ is injective. Thus $\Lambda\otimes_{\mathbb{Z}_p}\mathbb{Q}_p\neq 0$. Since $\Lambda/p\Lambda$ is a field, and $\mathrm{Spec} \Lambda$ is connected (since $\Lambda$ is local), we conclude that $\Lambda$ is a DVR. Alternatively, since $\mathbb{Z}/p^k\mathbb{Z}\to \Lambda/p^k\Lambda\cong R/p^kR$ is flat, we may also deduce the flattness of $\mathbb{Z}_p\to \Lambda$ directly from Tag 0523.

Thanks! I chose the last suggestion you made. See this commit.