Existence of W(k) and a ramified quadratic extension W(k)[√ p]

Let $p$ be a prime and let $k$ be an algebraically closed field of characteristic $p$ (lying in the lowest universe). The assertion is that one can find: a commutative ring $O^{\mathrm{nr}}$ which is a domain, a discrete valuation ring of characteristic zero, equipped with a $\mathbb{Z}_p$-algebra structure such that the ideal generated by the image of $p$ in $O^{\mathrm{nr}}$ is maximal and $O^{\mathrm{nr}}$ is complete (and separated) for the adic topology of that ideal, together with a ring isomorphism $e$ from the residue field of $O^{\mathrm{nr}}$ onto $k$; and, over it, a second commutative ring $O'$ which is again a domain, a discrete valuation ring of characteristic zero, carries an $O^{\mathrm{nr}}$-algebra structure, is complete for the adic topology of its maximal ideal, and contains an element $\varpi'$ of the maximal ideal with $\varpi'^2$ equal to the image of the natural number $p$ under $O^{\mathrm{nr}} \to O'$; finally a surjective ring homomorphism $\varphi' : O' \to k$ whose composite with the structure map $O^{\mathrm{nr}} \to O'$ equals the reduction map $O^{\mathrm{nr}} \to O^{\mathrm{nr}}/\mathfrak{m}$ followed by $e$.

This packages the ring of $p$-typical Witt vectors $W(k)$ of an algebraically closed field of characteristic $p$, which is an absolutely unramified complete discrete valuation ring of characteristic zero with residue field $k$, together with the totally ramified quadratic extension $W(k)[X]/(X^2-p)$ and its reduction map to $k$. It supplies the coefficient rings used by IsArtinianRing.exists_faithfullyFlat_isLocalHom_isAlgClosed_residueField_of_finite_residueField.