Laurent polynomials

Stream: maths

[Damiano Testa]

Dear All,

I'm starting to define Laurent polynomials. This is still in its very early stages, but I have a branch adomani_laurent_polynomials joining the CI building challenge of these past days.

Any comments are greatly appreciated!

I am planning to define monomial and probably weaken typeclass assumptions on the ring. However, I wanted to get the final lemmas exists_X_pow and proprop. (Naming is also on my TODO list.)

[Damiano Testa]

I'd be very happy to hear your opinions, as the day is coming to a close for me!

[Damiano Testa]

The branch only creates a new file data.polynomial.laurent_polynomials

[Yaël Dillies]

What about renaming it to data.polynomial.laurent to avoid redundancy?

[Damiano Testa]

Sure, I'll do that, likely tomorrow morning! Thanks for the input!

[Eric Wieser]

branch#adomani_laurent_polynomials?

[Eric Wieser]

I'm surprised we don't have what you call add_full_lift there, as an extension of docs#finsupp.lmap_domain

[Damiano Testa]

It might be there, I just could not find it...

[Eric Wieser]

It probably isn't, I don't remember seeing it either

[Damiano Testa]

I wanted to get the map as an R-linear ring map, but went for algebra, assuming commutativity on the semiring instead. I'll try to weaken that as well.

[Eric Wieser]

Looks like a great start, I look forward to the PR!

[Damiano Testa]

Thanks, Eric! You are the motivation behind it!

[Eric Wieser]

I would imagine you can get it as an R algebra map between polynomials over A, as the general case

[Eric Wieser]

(and you should probably build it for add_monoid_algebra before polynomials)

[Damiano Testa]

Also, I plan to add that R[T;T⁻¹] is the localization of R[X], hence the lemma about exists...

[Damiano Testa]

Yes, the branch was trying to get quickly somewhere, but the PRs will be more leisurely and with hopefully better and more stable development.

[Damiano Testa]

Also, a lot of this may not need ℕ and ℤ either, bit general monoids with a monoid map between them.

[Eric Wieser]

I found your use of regular N and Z to that end amusing

[Damiano Testa]

#13382 contains the stuff that goes into algebra/monoid_algebra/basic.

[Damiano Testa]

After the recent discussions, I decided to label PR #13415 as awaiting-review. Given the the monoid_algebra stuff has been merged, this is probably a good time!

[Damiano Testa]

Here is an update on the status of the PR.

• #13784 is the initial part of the PR, introducing Laurent polynomials and proving some basic lemmas about them;
• #13783 proves an auxiliary result, bundling comap_domain into an add_monoid_hom, when the implied map is an injection;
• #13415 is the rest of the Laurent polynomials PR, that will soon use comap_domain.add_monoid_hom to truncate to something more usual.

[Damiano Testa]

Further update: #13784 has been merged!

• #13783 is still waiting, with lemmas about comap_domain,
• #14005 is a new PR containing some induction lemmas for Laurent polynomials,
• #13415 is the "reference PR", where I added the localization result.