Need help defining an instance

Stream: new members

[Egor Morozov]

I would like to consider R[x_1,...,x_n] as an R[x_1]-module. I guess that what I need is an instance of Module (Polynomial R) (MvPolynomial (Fin (n + 1)) R) but I'm stuck on how to define it. Could someone give a hint please?

[Aaron Liu]

docs#PolynomialModule

[Egor Morozov]

Aaron Liu said:

docs#PolynomialModule

I am aware of this but I don't see how it helps. Of course, I have a module structure on PolynomialModule R (MvPolynomial (Fin n) R), which is mathematically the same but isn't an instance I'm looking for.

[Jakub Nowak]

Isn't PolynomialModule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) what you want?

[Egor Morozov]

I'm not sure... In fact, what I really need is to define some complicated linear map on R[x_1,...,x_n] in the following way: first define it on the elements of the form x_1 ^ s * g, where g is in R[x_2,...,x_n], and then extend by linearity (the map depends on s but is linear in g so it is possible). I just realized that probably this module structure is not what I really need here but I still don't see a good way to formalize this idea.

[Jakub Nowak]

Maybe this will be helpful?
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/MvPolynomial/Equiv.html#MvPolynomial.finSuccEquiv

[Jakub Nowak]

Ah, wait, nvm, that's different. It's n-valued polynomial with singled-valued polynomials as coefficients.
nvm, nvm, it's single-valued polynomial with n-valued polynomials as coefficients, so I think what you want?

[Egor Morozov]

Yes, I can use this isomorphism but then I have to jump between MvPolynomial (Fin (n + 1)) R and Polynomial (MvPolynomial (Fin n) R) all the time, which is very annoying. I believe there should be a more elegant way to do this.

[Jakub Nowak]

I've got the instance you wanted

import Mathlib

variable {R : Type*} [CommRing R]

noncomputable instance instPUnit : Module (Polynomial R) (MvPolynomial PUnit R) :=
  AddEquiv.module (β := Polynomial R) (Polynomial R) (MvPolynomial.pUnitAlgEquiv R)

noncomputable instance instFin (n : ℕ) : Module (Polynomial R) (MvPolynomial (Fin (n + 1)) R) :=
  match n with
  | 0 =>
    let : Fin (0 + 1) ≃ Unit := (Fintype.equivFinOfCardEq (by simp)).symm
    let : MvPolynomial (Fin (0 + 1)) R ≃+ MvPolynomial PUnit R := MvPolynomial.renameEquiv R this
    AddEquiv.module (Polynomial R) this
  | n + 1 =>
    let inst' := instFin n
    let : MvPolynomial (Fin (n + 1 + 1)) R ≃+ Polynomial (MvPolynomial (Fin (n + 1)) R) := MvPolynomial.finSuccEquiv R (n + 1)
    AddEquiv.module (Polynomial R) this

[Egor Morozov]

@MrQubo, wow, great job! Altgough I realized eventually that I don't need this for my initial problem, it is a very instructive piece of code for me, so thank you!

[Kevin Buzzard]

You could just define the ring homomorphism R[x_1]->R[x_1,...,x_n] and then turn the target into an algebra (and hence a module) over the source.