Exponential Fields & Transseries

Stream: Is there code for X?

[Antonio De Lucreziis]

It looks like there isn't anything from this branch of logic in mathlib:

https://en.wikipedia.org/wiki/Transseries

I was also looking for some docs on how one would start to formalize an object like this. More precisely, given a commutative ring $R$, i want to define the structure $(R, +, \times, <, \exp)$ in Lean. I tried writing an inductive type starting from a base ring $R$ and then adding exponential fields "operations" so $+$, $\times$ and $\exp$, but that only encodes "terms" of the structure and I loose all algebraic structure (i.e. I have to re-prove commutativity).

On the other hand, if I use the "type-class" approach I can easily define exponential fields in the axiomatic way, but then I lose the ability to match over term structure.

Is there an idiomatic way of doing this kind of things in Lean?

P.S. I don't know if this is the correct channel for this type of questions, in that case please tell me were I should move it

[Luigi Massacci]

What’s wrong with building on top of what is currently in mathlib’s model theory library?

[Luigi Massacci]

You can define that as a language expanding the language of rings (the latter being already there)

[Luigi Massacci]

There’s generic ordered structures but not ordered rings, but again you can combine the two (and add the appropriate compatibility axioms to the theory)

[Luigi Massacci]

see docs#FirstOrder.Language.ring

[Luigi Massacci]

The docs there also explain how to make this work alongside the standard Ring typeclass

[Luigi Massacci]

(the TLDR is: @Chris Hughes has already done the nasty part of setting this up for you, so you might as well reap the benefits instead of doing it from scratch)

[Chris Hughes]

I think the answer is different depending on what you want to do with this structure.

I think what it you actually want is to just define one particular type which is the type of formal transeries which is not a particularly easy type to define by the looks of it. You're best bet is to look at docs#HahnSeries and I suspect it's a special case of this by the looks of the wikipedia article (I don't know what a Transseries or a Hahn Series is so I'm not an expert here)

[Chris Hughes]

It's unlikely that anything to do with model theory is what you want. I wouldn't recommend using docs#FirstOrder.Language.ring

[Chris Hughes]

What you want is probably HahnSeries _ ℝ and I haven't quite figured out what goes in the placeholder for the _. It'll be some ordered abelian group, but I haven't quite worked out which one from the wikipedia article yet.

[Yaël Dillies]

Chris, I don't think this can be a Hahn series, since you can have a transseries as an exponent in another transseries

[Yaël Dillies]

You can however reuse docs#HahnSeries by following this construction: https://en.wikipedia.org/wiki/Transseries#Log-free_transseries

[Yaël Dillies]

The construction from surreal numbers might be the easiest one given the work we have on docs#Surreal: https://en.wikipedia.org/wiki/Transseries#Using_surreal_numbers

[Antonio De Lucreziis]

Thank you all. I already saw the Surreal numbers definition and I also think it is the one with the most similar construction. I'll let you know if me and my colleague make some progress on this!