feat(RingTheory/LaurentSeries): add notation

[Julian]

Refs: leanprover/vscode-lean4#523

---

I've only made use of the notation in the file in places that were already within the namespace, but happy to make further changes if preferred.

[github-actions]

PR summary 27c38d0421

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance : Algebra (RatFunc F) F⸨X⸩
+ instance : Coe R⟦X⟧ R⸨X⸩
+ instance : IsScalarTower F[X] (RatFunc F) F⸨X⸩
+ instance : Valued K⸨X⸩ ℤₘ₀ := Valued.mk' (PowerSeries.idealX K).valuation
+ instance [CommSemiring R] : Algebra R⟦X⟧ R⸨X⸩ := (HahnSeries.ofPowerSeries ℤ R).toAlgebra
+ instance {K : Type*} [Field K] : IsFractionRing K⟦X⟧ K⸨X⸩
+--+ coe_C
+--+ coe_neg
+--+ coe_smul
+--+ coe_sub
- instance : Algebra (RatFunc F) (LaurentSeries F)
- instance : Coe (PowerSeries R) (LaurentSeries R)
- instance : IsScalarTower F[X] (RatFunc F) (LaurentSeries F)
- instance : Valued (LaurentSeries K) ℤₘ₀ := Valued.mk' (PowerSeries.idealX K).valuation
- instance [CommSemiring R] : Algebra (PowerSeries R) (LaurentSeries R)
- instance {K : Type*} [Field K] : IsFractionRing (PowerSeries K) (LaurentSeries K)
-+-+ coe_X
-+-+ coe_add
-+-+ coe_mul
-+-+ coe_one
-+-+ coe_pow
-+-+ coe_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[kbuzzard]

I certainly like the look of this. The notation is standard, even to the extent that the brackets are written close together in LaTeX. Happy to hear another opinion but LGTM.

[faenuccio]

This is something that we discussed with @mariainesdff and we ended up wondering if this notation should be used for Laurent Series as HahnSeries of for the $$X$$-adic completion of $$K(X)$$. We prove they are isomorphic (the PR process is ongoing) but ultimately it is not clear to us what will be "the prototypical gadget" to play with, that will then most deserve a dedicated notation.

[Julian]

I don't know enough to have any opinion clearly so I'm happy to close if that's recommended!

[faenuccio]

After thinking carefully for a while, I am also in favour of the changes proposed by this PR. @Julian if you can update it, I will be happy to have a final look and suggest that it be merged.

[Julian]

@faenuccio I don't think there seem to be any merge conflicts -- are you asking me to rebase it anyways? (Happy to do whatever is helpful).

Also could you perhaps say anything about what changed your mind, just curious to learn!

[faenuccio]

@faenuccio I don't think there seem to be any merge conflicts -- are you asking me to rebase it anyways? (Happy to do whatever is helpful).

A couple of more PR included Laurent Series (in particular #16865, that is being merged) and it would be worthwhile to recheck for occurrences of LaurentSeries * in Mathlib to replace them with your notation.

Also could you perhaps say anything about what changed your mind, just curious to learn!

Ah sure, thanks for asking. Mainly three points:

1. Although it is true that power series are the completion of rational functions almost over "any" ring, the way these completions are constructed can be very different. So it makes perfect sense to have a basic set-up that works in the greatest generality and then, in special cases (like over fields) to state some isomorphisms; but then what really deserves a notation is the basic set-up, that is the most general;

2. The "explicit" definition with coefficients and bounded-below non-zero terms is most likely the one that one uses when considering terms of Laurent series, and having a notation that allows for writing down quickly "let f be a Laurent Series" is very useful; when stating abstract theorems, one is more likely to see the appearance of the type rather than the terms themselves, and having the full name in these cases seems OK;

3. It is very consistent with the rest of the library: we have a notation K[X] for polynomials seen as AddMonoidAlgebra R ℕ and this is very close to HahnSeries R ℤ.

I am sorry if these motivations were already perfectly clear in your mind, it just took me a while to convince myself 😢

[Julian]

A couple of more PR included Laurent Series (in particular #16865, that is being merged) and it would be worthwhile to recheck for occurrences of LaurentSeries * in Mathlib to replace them with your notation.

Aha! OK, happy to. Will ping you when I've done so (after your PR is merged).

I am sorry if these motivations were already perfectly clear in your mind, it just took me a while to convince myself 😢

Nothing is very clear in my mind :D, though thankfully I at least understood some of what you said! Thank you for elaborating!

[Julian]

OK this is ready for review I believe @faenuccio.

[faenuccio]

Thanks, having a look!

[faenuccio]

Thanks! I think that you can also replace the notation in the docstring (see line 282, for instance, in the dostring of def coeAlgHom (it also seems to me that there is a repetition three lines below). Also line 293 does not have this notation, can you check again the document? BTW, I think (please check) that we also have R(T) for rational functions, and it would be worth it to enforce also that notation in this file.

[Julian]

Thanks for the review! That section (from line 278 till 413) is not in the LaurentSeries namespace, it's in the RatFunc one, so the notation doesn't work in it, which was why I didn't make the change there -- obviously I can do it in the docstring anyways if that's preferred?

Or is there a way to be able to use it in the Lean code too? If I open LaurentSeries that will open everything, no, not just enable the notation?

I'll have a look for the rational function notation.

[faenuccio]

Thanks for the review! That section (from line 278 till 413) is not in the LaurentSeries namespace, it's in the RatFunc one, so the notation doesn't work in it, which was why I didn't make the change there -- obviously I can do it in the docstring anyways if that's preferred?

Or is there a way to be able to use it in the Lean code too? If I open LaurentSeries that will open everything, no, not just enable the notation?

I'll have a look for the rational function notation.

In order to only open notation you can write

open scoped LaurentSeries

(for instance right after the namespace RatFunc on line 280). This will allow the scoped (sic!) notation to fire, without carrying over all results in the namespace.

[Julian]

Thanks for that tip, I'm sure I've seen it before and forgot what it does. It seems to work perfectly.

I've made the changes, and also made the changes to use the PowerSeries notation in the file -- I'm still looking for the notation for rational functions, I don't see it immediately yet.

Right now the only places without the notation then are in the module docstring -- let me know if I should change it there too but I followed what the PowerSeries module did (which is to use it in the docstring).

[faenuccio]

Thanks for that tip, I'm sure I've seen it before and forgot what it does. It seems to work perfectly.

I've made the changes, and also made the changes to use the PowerSeries notation in the file -- I'm still looking for the notation for rational functions, I don't see it immediately yet.

Right now the only places without the notation then are in the module docstring -- let me know if I should change it there too but I followed what the PowerSeries module did (which is to use it in the docstring).

Concerning RatFun you're right, there is nothing. Forget about it - I am sorry. As for docstring, I would suggest that both in the module docstring (at the top) and in declarations docstring, you first use the full name, then you show what the notation is, and from that point on, you only use the notation. As several docstrings are duplicated in the module and along the files, this applies to both situations.

[Julian]

Concerning RatFun you're right, there is nothing.

There is one place that uses the notation in a docstring, that place is here (but yeah it seems not to exist, maybe due to those old Zulip threads about how safe it was to have notation with single parentheses? I can't find them via Zulip search).

I am happy to make the docstring notation change of course -- but do you want me to make it to the PowerSeries file as well in this same PR? It too doesn't mention the notation in the docstring. Or should I do that in a follow-up?

[Julian]

There are a bunch of places in the PowerSeries files that don't use the PowerSeries notation. To me it seems best to do it in a follow up along with fixing those. I'll proceed under that assumption unless you tell me otherwise!

[faenuccio]

There are a bunch of places in the PowerSeries files that don't use the PowerSeries notation. To me it seems best to do it in a follow up along with fixing those. I'll proceed under that assumption unless you tell me otherwise!

Both are OK, so go ahead as you see fit. Final question before sending this PR to merge: have you checked that LaurentSeries * does not appear anywhere else in the library?

[Julian]

OK I've added the notation to the module docstring and type docstring as you suggested, so I think this is ready now!

have you checked that LaurentSeries * does not appear anywhere else in the library?

Yes! At least via a grep, this is all of them.

[faenuccio]

Awesome, thanks so much for your work!

[faenuccio]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by faenuccio.