Separable extension of valuationSubring

Stream: maths

[Junjie Bai]

Suppose we have two field with discrete valuation K, L, and there valuation ring O_K, O_L. if L/K is a separable field extension, and K is complete with respect to the valuation. Is the ring extension O_L/O_K separable?(i.e. **all of the element has a separable minimal polynomial).

[Andrew Yang]

What's your definition of a separable polynomial over non-fields? mathlib defines it as $(f, f') = 1$ in $R[X]$. In this sense, $\mathcal{O}_L/\mathcal{O}_K$ is hardly separable ever. For example $x^2+1$ is not a separable polynomial in $\mathbb{Z}_2[X]$ because $(x^2+1, 2x)$ is contained in the proper ideal $\{ p\mid p(1) \in 2\mathbb{Z}_2\}$. So $\mathbb{Q}_2(i)/\mathbb{Q}_2$ is a counterexample.

[Junjie Bai]

You're right! But if we have moreover the extension of residue field is also separable, is it true?

[Andrew Yang]

Because $2$ splits in $\mathbb{Q}(i)$, the extension of residue field is trivial in $\mathbb{Q}_2(i)/\mathbb{Q}_2$.

[Andrew Yang]

I'm guessing that $\mathcal{O}_L/\mathcal{O}_K$ is separable iff $L/K$ is unramified.

[Junjie Bai]

Yes, you are right. That condition is not enough. It seems that i have to add this as a condition in my code. Thanks a lot!