linear maps of polynomials

Stream: Is there code for X?

[Heather Macbeth]

I would like to break the abstraction barrier between polynomials and finsupp ℕ briefly for the following purpose: I have a linear map from finsupp ℕ R to finsupp ℕ R and would like to interpret it as a linear map from polynomial R to polynomial R. Is there a good way to do this?

[Yaël Dillies]

This sounds like you need the "identity" equivalences between the type and its synonym, in the vein of docs#order_dual.to_dual, docs#order_dual.of_dual, docs#to_lex, docs#of_lex.

[Heather Macbeth]

That's so ugly, though! In my opinion what ought to exist is some kind of constructor for linear maps to/from polynomials, right before polynomial is marked irreducible. I haven't thought through the exact right form though, so I wondered if someone else had.

[Adam Topaz]

I'm surprised we don't have a finsupp version of docs#polynomial.coeff

[Adam Topaz]

Or a polynomial.of_finsupp.

[Adam Topaz]

Ah we do have docs#polynomial.to_finsupp (which is the field in the structure defining a polynomial)

[Heather Macbeth]

Even that, though, is not a linear map.

[Adam Topaz]

Right.

[Adam Topaz]

We do have docs#polynomial.basis_monomials so you could use that to obtain the linear iso.

[Heather Macbeth]

I wonder if @Gabriel Ebner has thought about this, he was behind the irreducible refactor I think.

[Adam Topaz]

import ring_theory.mv_polynomial.basic

variables (R : Type*) [comm_ring R]

noncomputable
example : polynomial R ≃ₗ[R] ℕ →₀ R :=
(polynomial.basis_monomials _).repr

[Heather Macbeth]

But it should also work to just define polynomial.to_finsupp.linear_map as linear_equiv.refl, before the irreducible attribute is introduced.

[Yaël Dillies]

... which is exactly what I proposed

[Eric Wieser]

polynomial isn't irreducible, it's a structure

[Adam Topaz]

Ah, we have docs#polynomial.to_finsupp_iso_alg

[Heather Macbeth]

Yaël Dillies said:

... which is exactly what I proposed

But what I'm saying is that I hate it :)

[Eric Wieser]

We do have polynomial.of_finsupp, it's the constructor of the src#polynomial structure

[Adam Topaz]

The docstring of to_finsupp_iso_alg is

Algebra isomorphism between polynomial R and add_monoid_algebra R ℕ. This is just an implementation detail, but it can be useful to transfer results from finsupp to polynomials.

[Heather Macbeth]

We have our general mathlib principle never to use an equiv if you can do it for a morphism ... it'd be great if there were a more functorial version here

[Heather Macbeth]

so "lift" rather than "transport"

[Eric Wieser]

It seems that doc-gen doesn't record constructor names which is why you couldn't find of_finsupp