The card of roots is equal to natDegree of separable polynom

Stream: new members

[Junjie Bai]

If we have the extension of ring S / R is separable, x is an element of S, and f is it's minimal polynomial over R , can we proof the card of roots of f is equal to the natDegree of f? here is a #mwe:

import Mathlib

open Algebra Polynomial
variable {R S : Type*} [CommRing R] [IsDomain R] [Ring S] [IsDomain S] [Algebra R S]
variable [Algebra.IsSeparable R S]
variable {x : S}

example : Multiset.card (minpoly R x).roots = (minpoly R x).natDegree := by sorry

[Kevin Buzzard]

I doubt that what you've formalised is true in general -- isn't that the roots in R? But it's not true for roots in S either even for fields, if S/R isn't normal

[Junjie Bai]

Yes, I think you are right. The problem I'm dealing is this :
Suppose L/K is a valued field extension, separable and normal. and O_K, O_L is the valuation ring, suppose the ring extension O_L/O_K is also separable. can we have this conclusion? Here is the #mwe:

import Mathlib

open Valuation Valued

variable {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] [Normal K L]
variable [LinearOrderedCommGroupWithZero ℤₘ₀] [vK : Valued K ℤₘ₀] [vL : Valued L ℤₘ₀]
variable [Algebra 𝒪[K] 𝒪[L]] [Algebra.IsSeparable 𝒪[K] 𝒪[L]]

example (x : 𝒪[L]) : Multiset.card (minpoly 𝒪[K] x).roots = (minpoly 𝒪[K] x).natDegree := by sorry

Do you think these condition is enough? Or what should I add to get the result? Thanks a lot!

[Kevin Buzzard]

I think those conditions are too much: the algebra OK OL assumption means "assume OL is an OK-algebra in an arbitrary way"

[Junjie Bai]

Yes, it can inferred by other condition, but I don't remember what should I open to infer this. How can I proof this under the assumptions? I don't find a theorem related to this, most of them require the minimal polynomial is over a field. Should I proof a lemma first? Or which theorem can solve this? Any suggestion is appreciated.

[Riccardo Brasca]

The first thing you have to do is to write down a very precise pen and paper proof.

[Riccardo Brasca]

Then check what is in mathlib and what is not. For integrally closed rings we should have a more or less robust theory of minimal polynomials.

[Junjie Bai]

OK, I'll try to do it! Thanks a lot!