mv_polynomial.vars

Stream: maths

[Chris Hughes]

I'm really struggling with mv_polynomial.vars. I'm looking for some lemma that I can use to reason about it without having to think about polynomials as finsupp. Something like the fact that p is in the image of the canonical map from mv_polynomial p.vars R, or the fact that for any set s, algebra.adjoin (X '' s) = {p | ↑p.vars ⊆ s}. Does someone who knows this part of the library have a good idea about how to do this?

[Adam Topaz]

Is docs#mv_polynomial.eval₂ the preferred way to "change the variables type" (after composition with mv_polynomial.X of course)? The API search comes up with nothing when I look for mv_polynomial vars eval which is not very promising...

[Chris Hughes]

(deleted)

[Chris Hughes]

Adam Topaz said:

Is docs#mv_polynomial.eval₂ the preferred way to "change the variables type" (after composition with mv_polynomial.X of course)? The API search comes up with nothing when I look for mv_polynomial vars eval which is not very promising...

The preferred way is rename.

[Chris Hughes]

I guess maybe vars_rename is the key.

[Chris Hughes]

It's still not easy to work out how to use that.

[Adam Topaz]

( docs#mv_polynomial.vars_rename since I'm on mobile)

[Chris Hughes]

Let s be the smallest set such that p is in the image of rename (coe : s -> sigma). suppose rename coe q = p, then q.vars ⊆ s ⊆ p.vars by vars_rename. Therefore p is in the image of the map from mv_polynomial p.vars R. I'm tired, but I hope that's right.

[Chris Hughes]

This tells me vars is big enough which is what I struggling with. I already knew it was small enough.

[Chris Hughes]

Hang on, I know q.vars ⊆ s and q.vars ⊆ p.vars but not s ⊆ p.vars which is what I need.

[Johan Commelin]

@Chris Hughes I'm not a vars expert, but I've worked with it before. I need to take care of some bureaucrazy this morning. But please ping me later today, if you are still struggling with it then.

[Chris Hughes]

It seems like I managed it. The key lemma was eval₂_hom_congr'

lemma exists_rename_eq_of_vars_subset_range  (p : mv_polynomial σ R) (f : S → σ)
  (hfi : injective f) (hf : ↑p.vars ⊆ set.range f) :
  ∃ q : mv_polynomial S R, rename f q = p

[Johan Commelin]

I think I used eval\2_hom_congr' a tonne during the Witt project.

[Johan Commelin]

Do you need injectivity of f?

[Johan Commelin]

Ooh, I see. We used the version without ' quite a lot, and the version with ' was used twice.

[Eric Wieser]

(docs#mv_polynomial.eval₂_hom_congr')