go from relation to polynomial

Stream: general

[Jack J Garzella]

Say I have a linear relation on the finset 1, α, α^2, ..., α^n (e.g. from the lemma exists_nontrivial_relation_of_dim_lt_card), which on paper I might write as c_0 * 1 + c_1 * α +, ..., c_n * α^n = 0. I want to reinterpret this equation as the statement "the polynomial c_0 * 1 + c_1 * x +, ..., c_n * x^n has α as a root. It's unclear to me how to even get the polynomial in the first place, and then one would need to assert that it has the proper root.

This seems like a good example of a statement that is "mathematically obvious" but very subtle in Lean. How should one go about this?

This step is key in the proof of the following lemma

lemma degree_le_findim (x : L) {hx : is_integral F x} :
degree (minimal_polynomial hx) ≤ findim F L := sorry

[Alex J. Best]

(in mathlib) A polynomial over K is a function \N \to K with finite support, so the slickest way is probably to define the function as a composition \N \to V \to K where V \to K is from exists_nontrivial_relation_of_dim_lt_card and \N \to V is the map \lambda n, \alpha^n, then prove this has finite support. What I wrote doesn't quite make sense as really you want \N \to K to send any m bigger than the original degree to 0, so there should be an if in there or something too.

[Scott Morrison]

(This is an excellent question, and I would love to see progress here! I've already wanted this for the second half of Schur's lemma.)

[Johan Commelin]

@Jack J Garzella In what form do you have the linear relation?

[Johan Commelin]

As some sort of finset.sum or as something being an element of the span of other elements?

[Johan Commelin]

Or maybe something else?

[Johan Commelin]

Whatever the shape you have it in, I agree that it makes sense to add a new constructor for polynomials.
Something like this

def polynomial.of_relation := sorry -- figuring out the correct generality here might be non-trivial...

lemma polynomial.of_relation_is_root :
  eval\2 _ _ (polynomial.of_relation _ _ _ _) x = 0

[Anne Baanen]

Did you already check the proof that a Noetherian (i.e. finite-dimensional) field extension is integral? It has a relatively explicit construction, although I don't understand all the details from reading it.