polynomial op_C

Stream: new members

[Damiano Testa]

Dear All,

I am trying to work with mul_opposite and polynomial. As far as I can see, there is little more in mathlib, besides the equivalence

op_ring_equiv R : R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X]

I can get by with the two lemmas below: if my understanding is correct, they should be true. Can someone either provide a proof, or give a hint as to how to use op_ring_equiv to prove them?

Thanks!

import ring_theory.polynomial.basic

open_locale polynomial
open polynomial mul_opposite

variables {R : Type*} [semiring R]

@[simp] lemma mul_opposite.op_C (a : R) :
  (op_ring_equiv R) (op (C a)) = C (op a) :=
begin
  sorry
end

@[simp] lemma mul_opposite.op_X :
  (op_ring_equiv R) (op (X : R[X])) = X :=
begin
  sorry,
end

[Eric Wieser]

docs#polynomial.op_ring_equiv

[Eric Wieser]

docs#add_monoid_algebra.op_ring_equiv_single is basically the proof you want

[Eric Wieser]

You just need to do the appropriate unfolding to turn polynomial into add_monoid_algebra

[Damiano Testa]

I spent quite some time trying various combinations of

unfold polynomial
unfold op_ring_equiv,
unfold add_monoid_algebra.op_ring_equiv,
unfold C,
unfold monomial,
unfold monomial_fun,
ext,
simp,
congr,
exact add_monoid_algebra.op_ring_equiv_single a 0,
convert add_monoid_algebra.op_ring_equiv_single a 0,
exact add_monoid_algebra.op_ring_equiv_single 0 a,
convert add_monoid_algebra.op_ring_equiv_single 0 a,

but (I can say with almost certainly) none of these commands in any order actually works.

I imagine that the proof is just a few characters, but I am having a really hard time figuring out which ones...

[Kevin Buzzard]

Eric Wieser said:

docs#polynomial.op_ring_equiv

#13132 :-)

[Kevin Buzzard]

This is harder to do now polynomial is a structure with one field.

[Damiano Testa]

I feel very silly, but... this does not answer the question, right?

I had not realized the typo in the doc-string, since I had only read the lean code. :face_palm:

[Kevin Buzzard]

Yes, I can't answer the question in just a few characters. I could imagine proving it using ext and checking coefficients but I think Eric has something much smarter in mind. The issue is that we can no longer unfold polynomial into add_monoid_algebra because they're no longer defeq.

[Damiano Testa]

Ok, for the moment, I am happy with working assuming that the two lemmas that I wrote above are provable. I can always leave sorrys and go back to them later.

[Damiano Testa]

Ideally, I would like to know that nat_degree, support, leading_coeff convert "the obvious way" from a polynomial to its op. I think that I may be able to do the conversion, once those two pieces are in place.

[Damiano Testa]

(that is, once that bridgegap is closed, then I can make everything fit through the equivalence, or so I hope)

[Eric Wieser]

I made a start on this, but needed #13139 first

[Eric Wieser]

It should be possible to just do something like (docs#to_finsupp_iso)

apply to_finsupp_iso.injective,
clean_up_the_mess,
exact the_lemma_i_mentioned_earlier

[Eric Wieser]

But I can't work out what the intended spelling of clean_up_the_mess is

[Damiano Testa]

Ok, thanks for the suggestion! I'm probably not going to look at this today, but I have full proofs of the fact that supports, natdegrees, coeffs, leading coeffs... are what they should be, modulo these two lemmas.

[Damiano Testa]

Besides failing at proving X = X, this question exposed two typos in doc-strings: the one Kevin opened above and #13144.

[Damiano Testa]

As is often the case, once you find a solution to a problem, the problem suddenly appears much easier! What is below works:

@[simp] lemma op_monomial (n : ℕ) (r : R) :
  (op_ring_equiv R) (op (monomial n r : R[X])) = monomial n (op r) :=
by simp [op_ring_equiv]

@[simp] lemma op_C (a : R) :
  (op_ring_equiv R) (op (C a)) = C (op a) :=
op_monomial 0 a

@[simp] lemma op_X :
  (op_ring_equiv R) (op (X : R[X])) = X :=
op_monomial 1 1

[Damiano Testa]

The first by simp [op_ring_equiv] squeezes to

simp only [op_ring_equiv, ring_equiv.trans_apply, ring_equiv.op_apply_apply,
  ring_equiv.to_add_equiv_eq_coe, add_equiv.mul_op_apply, add_equiv.to_fun_eq_coe,
  add_equiv.coe_trans, op_add_equiv_apply, ring_equiv.coe_to_add_equiv, op_add_equiv_symm_apply,
  function.comp_app, unop_op, to_finsupp_iso_monomial, add_monoid_algebra.op_ring_equiv_single,
  to_finsupp_iso_symm_single]

No wonder there were lots of wring turns that I was taking!

[Damiano Testa]

I am thinking of making a PR with the lemmas above and also

 @[simp] lemma coeff_op (p : R[X]) (n : ℕ) :
  (op_ring_equiv R (mul_opposite.op p)).coeff n = mul_opposite.op (p.coeff n) := sorry

 @[simp] lemma support_op (p : R[X]) :
  (op_ring_equiv R (op p)).support = p.support := sorry

 @[simp] lemma nat_degree_op (p : R[X]) :
  (op_ring_equiv R (op p)).nat_degree = p.nat_degree := sorry

 @[simp] lemma leading_coeff_op (p : R[X]) :
  (op_ring_equiv R (op p)).leading_coeff = op p.leading_coeff :=

Assuming this seems like a good idea, what should the namespaces for these lemmas be? polynomial for dot-notation? Should mul_opposite or op_ring_equiv appear somewhere?

Thanks!

[Johan Commelin]

Those look useful. And yes, I would go for namespace polynomial.

[Damiano Testa]

Thanks! I'm preparing a PR. I am thinking of starting a new file ring_theory.polynomial.opposites. The polynomial files tend to be big and slow, and probably not often people need opposites, when working with polynomials.

Does this sound reasonable?

[Eric Wieser]

I think they should be called coeff_op_ring_equiv, and be stated without the op on the LHS by changing the type of p

[Eric Wieser]

But those lemmas look good to me

[Damiano Testa]

Also, in the context of this PR, op (a * b) converts to op b * op a. However, it would make more sense to have op (C a * X ^ n) convert to (C (op a) * X ^ n. Is there a way to instruct simp to use a different lemma than the "obvious" one?

[Eric Wieser]

If you do that, I think op_ring_equiv should move to that file

[Eric Wieser]

We could add a simp lemma that sends X ^ n * C to C * X ^ n?

[Eric Wieser]

We already have docs#polynomial.X_pow_mul, but that's not safe as a simp lemma

[Damiano Testa]

The lemma already exists.

[Eric Wieser]

Not specialized to C, does it?

[Damiano Testa]

Ah, I see your point!

[Damiano Testa]

I will also add this lemma, then. Though to a more basic file.

[Eric Wieser]

The idea with specializing to C is that it becomes a valid simp lemma that doesn't loop on X ^ n * X ^ n

[Eric Wieser]

Note that I just finished off my polynomial refactor in #13139, which will likely upset some calls to simp in your code if it gets merged

[Damiano Testa]

Thanks for the heads up! However, having learned that monomial is a much more stable spelling of C a * X ^ n, I am confident that it will be easy to fix the first lemma and all the other ones follow from it.

[Damiano Testa]

Eric Wieser said:

I think they should be called coeff_op_ring_equiv, and be stated without the op on the LHS by changing the type of p

I thought that I understood this comment, but is what is below what you had in mind?

@[simp] lemma coeff_op_ring_equiv (p : R[X]ᵐᵒᵖ) (n : ℕ) :
  (op_ring_equiv R p).coeff n = op ((unop p).coeff n) :=

[Damiano Testa]

#13162

It seems that no file used polynomial.op_ring_equiv, so I simply moved the definition to a new file and placed there also the lemmas above.

I will see if CI finds a hidden use of op_ring_equiv somewhere.

[Damiano Testa]

I also PRed the simp version of X_mul and X_pow_mul: #13163.