Degree of span of polynomials

Stream: Is there code for X?

[Lukas Miaskiwskyi]

To get back into the Lean world, I've been going into a rabbit hole on how to possibly prove the Jordan normal form (which we don't have yet, right?). This has lead me to proving the following three theorems which I couldn't immediately find:

import Mathlib.Data.Polynomial.Module

universe u

open Polynomial Module

variable {K : Type u} [Semiring K]

/-- For every polynomial `p` in the `K`-span of a set `s : K[X]`, there exists a polynomial of `p' ∈ s`
  whose degree dominates  `degree p`. See also `degree_span'` -/
theorem degree_span (s : Set K[X]) (hs : s.Nonempty) (p : K[X]) (hp : p ∈ Submodule.span K s) :
  ∃ p' ∈ s, degree p ≤ degree p' := sorry

/-- A stronger version of `degree_span` under the assumption that the set `s : K[X]` is finite.
  There exists a polynomial `p' ∈ s` whose degree dominates the degree of every element of
  `p ∈ span K s`-/
theorem degree_span' (s : Set K[X]) (h_fin : s.Finite) (hs : s.Nonempty) :
  ∃ p' ∈ s, ∀ (p : K[X]), p ∈ Submodule.span K s → degree p ≤ degree p' := sorry

variable {R : Type u} [Semiring R] [Nontrivial R] [NoZeroDivisors R]

/-- If `R` is a nontrivial ring without zero divisors, the polynomials `R[X]` are not finite as an
 `R`-module. When `R` is a field, this is equal to `R[X]` being an infinite-dimensional vector
 space over `R`.  -/
theorem polynomials_not_finite_module : ¬ (Module.Finite R R[X]) := sorry

Now as I proved them I've started to realize that I have no idea how to decide whether a theorem is a useful addition to mathlib. I wasn't able to find any theorems on how the span of polynomials interacts with degree, at least, so they're likely not completely redundant? In any case, looking at these theorems, is there any additional design philosophy you think I should be aware of?

[Ruben Van de Velde]

If you found them useful, probably there's a good chance they'll be accepted (new theorems about existing definitions much more easily than new definitions)

[Lukas Miaskiwskyi]

Okay, I suppose there's no harm to just PRing and learning with the accompanying reviews! At this point then we're not too concerned about bloating mathlib with theorems that e.g. may not see much use?

[Riccardo Brasca]

Did you use docs#Polynomial.degreeLT ?

[Riccardo Brasca]

With it the proof should be very short (but we want the results anyway!)

[Lukas Miaskiwskyi]

Hm, I saw those definitions but I didn't directly see how to quickly relate it to the span of an arbitrary set. For the first theorem I used docs#Submodule.span_induction, for the second one I combined the first theorem with docs#Set.Finite.exists_maximal_wrt, and for the last one I used the second theorem to show that the span of any finite subset only contains polynomials with finitely high degree. I probably did it like a lean-pedestrian, but I imagine when I PR the theorems someone will show me how to make them all one-liners :smiling_face_with_tear:

[Lukas Miaskiwskyi]

(but most importantly I still had fun!)

[Riccardo Brasca]

You can prove that if all elements of s are of degree less than n then the span is included in Polynomial.degreeLT (this should be immediate using docs#Submodule.span_le) and the proceed by contradiction

[Riccardo Brasca]

But also using induction is provably easy

[Riccardo Brasca]

I am talking about the first one

[Riccardo Brasca]

The second one is true in general, isn't it?

[Kevin Buzzard]

The last one certainly doesn't need no zero divisors and follows easily from the fact that any finite set of polynomials will be contained in the submodule of polynomials of degree at most N for some sufficiently large N and hence won't contain X^(N+1)

[Kevin Buzzard]

Riccardo Brasca said:

The second one is true in general, isn't it?

What do you mean by this?

[Riccardo Brasca]

Without assuming s finite

[Kevin Buzzard]

So what is your p' if s={1,X,X^2,X^3,...}?

[Riccardo Brasca]

Sorry sorry

[Lukas Miaskiwskyi]

Kevin Buzzard said:

The last one certainly doesn't need no zero divisors and follows easily from the fact that any finite set of polynomials will be contained in the submodule of polynomials of degree at most N for some sufficiently large N and hence won't contain X^(N+1)

True, thanks, I'll see if I can refine my proof there :)

[Kevin Buzzard]

IIRC we have this submodule in mathlib. It makes the first and third proof easy.

[Kevin Buzzard]

For the first one, by contradiction: if all elements of s had degree < degree p then the span is also contained in the polys of degree < degree p, an immediate contradiction.

[Riccardo Brasca]

Yes, it is docs#Polynomial.degreeLT

[Kevin Buzzard]

Oh yeah I just clicked on your link :-) Nice! So indeed we're suggesting the same proofs for 1 and 3.

[Lukas Miaskiwskyi]

Aaah, that's really nice, and indeed, that does likely make it very short. Thank you both! With some more experience & creativity I'll probably be better able to use the already existing resources

[Kevin Buzzard]

Yeah that's the trick. I remember well when I was in your situation -- I could think of a random proof and then bash it out and indeed I found it a lot of fun. But somehow there's an art to finding the most painless proof, and Riccardo and I both independently immediately focused on the submodule because we've seen it before as a useful construction. It's a cofinal system of finitely generated sub-R-modules: every fg R-submodule of R[X] is contained in one of these modules so often questions involving submodules can be reduced to questions about these particular submodules and hence to statements about degrees.

[Riccardo Brasca]

Yeah, it is important to believe in the library! We have really a lot of stuff about polynomials, I thought it is unlikely this submodule never showed up

[Ruben Van de Velde]

And then sometimes it turns out that your result is just the combination of two existing lemmas and it's actually easier to use them directly in your proof