Hahn Series

Stream: maths

[Aaron Anderson]

I currently have a stack of PRs forming on Hahn series, so I’m starting a thread.

[Aaron Anderson]

#6208 is needed to define multiplication, and #6226 is needed to show the product is an actual Hahn series.

[Aaron Anderson]

These are put to work in branch#hahn_series.

[Aaron Anderson]

I’m interested in any thoughts as to whether Laurent series should actually be defined as hahn_series Z _, or if I should just give an iso when both are done.

[Aaron Anderson]

@Kevin Buzzard

[Kevin Buzzard]

My plan was to define Laurent series as Hahn series with coefficients in Z and to prove that that were a localisation of power series in one variable at the variable. Thanks so much for doing this!

[Aaron Anderson]

Ok, #6237 gets up to the comm_ring structure.

[Johan Commelin]

Cool! You are moving fast!

[Xavier Xarles]

How nice! You did a really nice job, I am learning a lot reading what you did.

[Aaron Anderson]

Let me know if you have any further questions about it, it'd help the documentation.

[Aaron Anderson]

Other than the order theory, creating a new type of series with a convolution product is a bit boilerplate, except for a few small things that can go wrong in the distributivity/associativity proofs, which go wrong differently in each different context it seems...

[Filippo A. E. Nuccio]

While @Aaron Anderson was developing the more powerful theory of Hahn Series, I've amused myself defining Laurent series (in one variable), and PR it in #6258. There are still some sorrys left concerning associativity, but the basics of it being a comm_ring (when the coefficients are) is there. I've also defined coefficients (as a function from $\mathbb{Z}$ to the base ring). Being much less experienced then @Aaron Anderson , my code is by far less efficient and I wonder if anything of what I've done should be kept or if the approach through Hahn series makes everything obsolete. Before going further, I'd appreciate if anyone can have a look and tell me if it is worth spending more time on my approach, or not.

[Aaron Anderson]

I think the biggest issue is that working with quotients is difficult.

[Aaron Anderson]

Personally I think it's much easier to define Laurent series as a subtype of a type of functions like how I defined Hahn series, or if you want to use ordered pairs, make the pair representation unique, like perhaps by representing it as a pair of a coefficient function with a rank, where the rank lives in with_top Z, with the rule that the rank is the largest possible rank such that all coefficients below that rank are 0.

[Aaron Anderson]

The benefit of your sort of pair representation is in defining the embedding of power series into Laurent series, and I'll admit I haven't gotten there yet, but I think it should still not be too bad with Hahn series

[Aaron Anderson]

The actual Hahn series PR #6237 is now unblocked. I've started developing the valuation at branch#hahn_series2, but won't be able to get around to it again for at least a week.

[Aaron Anderson]

An update on the Hahn series project if anyone wants it:

[Aaron Anderson]

I'm inching closer towards being able to define the field structure. The critical step that remains is proving Higman's Lemma.

[Aaron Anderson]

To do that, I started expanding the API on partial well-orderings, and in the process of looking into all of this, found that with partial well-orderings, we can drop the linearity assumption on the monomial group, which means that things like multivariable Laurent series should be possible. This is what #7131 is for.

[Aaron Anderson]

I've delayed defining Laurent series until I have the field structure, so I can define the localization map as a localization map, but if anyone has any requests for Laurent series API, I'd be happy to discuss it.

[Johan Commelin]

@Aaron Anderson This is becoming a pretty huge project, but I'm really happy you are doing it. I don't have a pressing need for Laurent series right now. But probably in a couple of months, yes.
And it's just great to know that by that time there will be a solid API in place!

[Kevin Buzzard]

Yes this is a much overdue API. Many thanks!

[Aaron Anderson]

Yes, this is rather more complicated than just defining Laurent series, but we should also be able to get Puiseux series for cheap, and Hahn series themselves are nice.

[Aaron Anderson]

Aaron Anderson said:

I'm inching closer towards being able to define the field structure. The critical step that remains is proving Higman's Lemma.

Apparently Higman's Lemma was already done in lean by @Minchao Wu in the Kruskal's Tree Theorem project

[Minchao Wu]

@Aaron Anderson Higman’s Lemma was done in a very early version of Lean 3 and has not yet been ported to the current mathlib. I can modernize it and make a PR if people want it.

[Aaron Anderson]

I am already working on it, taking inspiration from your strategy. It would need to be connected to my definitions about well-quasi orders anyway.

[Aaron Anderson]

branch#higmans_lemma

[Aaron Anderson]

Starting this at #7165

[Minchao Wu]

I have been trapped by other tasks last week and just came back to this. It seems that the formalization is almost done (and looks very nice), but I’ll try to see if there’s anything I can do.

[Aaron Anderson]

It occurs to me that finsum can probably cut a lot of the nasty proofs way down

[Aaron Anderson]

Hrmm... I'm not so sure. I've started at branch#hahn_finsum, and I'd like some input as to whether this is better.