This aim of this question is to determine whether there exists a proof (or some counterexample) to the following statement : "If $R$ is a subring of Dedekind domain $S$, such that $S$ has a power basis as an $R$-module, then $R$ is itself a Dedekind domain".


The context is the following: I have recently been working on formalizing (using Lean) the Dedekind-Kummer theorem, which can be stated as follows [Proposition 8.3, *Algebraic number theory*, Neukirch] :


Let $\mathcal{O}$ be a Dedekind domain with field of fractions $K$ and $L$ a finite separable extension of $K$, and set $\mathcal{O'}$ to be the integral closure of $\mathcal{O}$ in $L$. If we pick a prime ideal $\mathfrak{p}$ of $\mathcal{O}$ and $\theta \in \mathcal{O}'$ such that the conductor ideal $\mathcal{C}$ of $\mathcal{O}[\theta]$ is coprime with $\mathfrak{p}$ and $L=K(\theta)$, then the prime factorisations of $\mathfrak{p} \mathcal{O'}$ and $\overline{f}$ have the same shape (in other words, there is a bijection between the sets of prime factors of $\mathfrak{p} \mathcal{O'}$ and $\overline{f}$ that preserves multiplicities), where $f$ is the minimal polynomial of $\theta$ over $K$ and $\overline{f}$ is the reduction mod $\mathfrak{p}$ of $f$.
**​​​​​​**


So far the case when $\mathcal{O'} = \mathcal{O}[\theta]$ has been fully formalized, but the formalization does not use the assumption that $\mathcal{O}$ is a Dedekind domain. The aim of this question is thus to determine whether or not this is actually a generalization of the original statement (at least for this particular case).**​​​​​​**



Can a Dedekind domain have a power basis over a ring that isn't a Dedekind domain?
If $R\subseteq S$ with $S$ Dedekind and free as an $R$-module, then $R$ is Dedekind because every $R$-ideal $I$ is projective (hence invertible, if non-zero). For $I\otimes\_RS$ $\cong$ $IS$ is projective over $S$, hence over $R$. But $I\otimes\_RS$ $\cong$ $I^{\oplus n}$ - or, more generally, $I\otimes\_RS$ $\cong$ $\bigoplus\_{\alpha\in A}I$ when $S$ $\cong$ $\bigoplus\_{\alpha\in A}R$. So $I$, a direct summand of $I\otimes\_RS$, is also projective over $R$.


**Edit** In fact, if $S$ is integral over $R$ (for example, finitely generated as a module), it suffices that $S$ is flat over $R$. For then we have $I\otimes\_RS$ $\cong$ $IS$, which is flat over $S$. But $S/R$ has lying-over, so that $\mathfrak{m}S$ $\ne$ $S$ for every maximal ideal $\mathfrak{m}$ of $R$. Thus $S$ is faithfully flat over $R$. This implies that $I$ is flat over $R$. So $R$ is Prüfer (finitely generated ideals are flat), and hence all non-zero finitely generated ideals are invertible. And $R$ must be Noetherian (if $I\_1\subseteq I\_2\subseteq\cdots$ are ideals of $R$, we have $I\_nS$ $=$ $I\_{n+1}S$ for some $n$; but $I\_nS\cap R$ $=$ $I\_n$ by faithful flatness, and likewise for $I\_{n+1}$).


