laurent series

Stream: condensed mathematics

[Kevin Buzzard]

This sounds like a worthwhile project whether or not we need it for LTE. What is the scope? I could even do it for my class I'm teaching this term. Is there a multivariable theory? Right now we have power series in an arbitrary collection of variables $\sigma$ over a semiring $R$ defined as (σ →₀ ℕ) → R (so in particular $X_1+X_2+X_3+\cdots$ is allowed if all the $X_i$ are variables). If $R$ is furthermore commutative, Laurent series could just be defined by localising at the submonoid generated by $\sigma$. Is that even a useful definition? Or are we sticking to the one-variable case?

[Peter Scholze]

I think the needs for LTE are somewhat orthogonal to any standard approach, as these archimedean convergence bounds are fundamental to LTE.

[Peter Scholze]

And I don't think there's any reasonable multivariable theory

[Kevin Buzzard]

I think there's a well-defined map from the localisation to the $R$-module (σ →₀ ℤ) → Ralthough I don't see how to define it automatically because this isn't a ring so you can't use the universal property. But that's how to get coeff working I guess (it can be defined by hand).

[Peter Scholze]

Localization also has a universal property on $R$-modules

[Peter Scholze]

By the way @Kevin Buzzard , I remember that at some point you were annoyed that to check that the structure presheaf is a sheaf on affine schemes, you could not use the universal property of localizations rings, as some map is a difference

[Kevin Buzzard]

Aah, as an $R$-module the localisation $R[1/S]$ is the initial object for $R$-modules such that elements of $S$ act invertibly.

[Peter Scholze]

The trick there would have been to use (truncated) simplicial objects

[Kevin Buzzard]

Yes, but this is just a gimmick

[Kevin Buzzard]

Aah! I thought the trick was to talk about equalizers and not take the difference

[Peter Scholze]

OK, that's the same

[Peter Scholze]

Just came to mind as I was in the simplicial mindset ;-)

[Kevin Buzzard]

I just flag it because in the Stacks project they take the difference, when doing the basic theory.

[Johan Commelin]

Note that in LTE I also define the $(\_)^{T^{-1}}$ as an equalizer instead of a kernel. It's just a bit more natural, and makes a lot of things easier that you want to do afterwards.

[Peter Scholze]

Sounds good to me! Equalizers are just uglier to draw

[Peter Scholze]

I actually wanted to scream "but I did define it as an equalizer" before realizing I didn't

[Peter Scholze]

Actually, in my paper with Thomas Nikolaus, John Rognes complained a lot when we were just formally replacing equalizers by fibres of the difference, for maps of spectra (in the sense of algebraic topology). Somehow in his mental model for spectra, you can't meaningfully take the difference of two maps.

[Kevin Buzzard]

So to give an $A[1/S]$-module is to give an $A$-module on which the elements of $S$ act as bijections -- thanks Peter! Now if $R$ is a commutative ring (or probably even a commutative semiring) then $M:=$(σ →₀ ℤ) → R is a module for the ring $A = R[[\sigma]]:=$(σ →₀ ℕ) → Rin which the elements of $\sigma$ act as bijections, so it's a module for $A[1/\sigma]$, and now you can define a map $A[1/\sigma]\to M$ by sending 1 to 1 and there's your coeff. Then you can specialise to the case $\sigma=\{*\}$ and show e.g. that it's an ID if $R$ is an ID, a field if $R$ is a field etc. Is there any particular goal that you want Johan? I could definitely do this with my students. I promised them a possible walk through the foothills of Clausen-Scholze!

[Peter Scholze]

A fun theorem is that $\mathbb Z((T))$ is a principal ideal domain. That would actually go in a direction that's helpful for LTE (see Lecture 7)

[Peter Scholze]

But it's almost certainly too hard to do in the course

[Kevin Buzzard]

If $R$ is a PID is $R((T))$ a PID?

[Kevin Buzzard]

I have students looking for projects.

[Kevin Buzzard]

If $R$ is a UFD then $R[[T]]$ is a UFD, I believe.

[Kevin Buzzard]

but I'm always a bit scared about dimension-counting in this context.

[Peter Scholze]

I'd have to think about it, there are certainly some statements like this

[Johan Commelin]

@Kevin Buzzard Sorry, I haven't studied those sections enough to know what we'll need.

[Peter Scholze]

Yes, basic intuition about dimensions gets pretty safely fucked up

[Kevin Buzzard]

(it was Judith Ludwig who taught me this)

[Filippo A. E. Nuccio]

I think that R[[T]] is not a UFD in general if R is a UFD, there is a paper by Samuel on this
https://www.math.lsu.edu/~madden/M7210fall2012/Samuel-UFDs.pdf

[Filippo A. E. Nuccio]

But if R is a regular UFD, then R[[T]] is a (regular) UFD as well

[Kevin Buzzard]

oh wow it's amazing to see papers like this. "For example the fact that every regular local ring is a UFD has been conjectured in the early 40s...but the general case has been settled only in 1959 by Auslander and Buchsbaum". It's funny to imagine a time when this result wasn't "well-known and in all the standard textbooks"

[Kevin Buzzard]

Apparently $R:=\mathbb{F}_2[x,y,z]/(z^2-x^3-y^7)$ is a counterexample!

[Xavier Xarles]

There is another notion of something related to Laurent series, but much more abstract, that could be defined in Lean, is that of Hahn series:
https://en.wikipedia.org/wiki/Hahn_series
It could be defined as the series formed by the elements f in (σ →₀ G) → R , where R is a semiring, G an ordered_comm_monoid, whose support (to be defined) is well-ordered (i.e. any non-empty subset of the support of f has a least element), and in principle σ is finite (I did not check if it could work for any σ). If G= ℕ, all the subsets are well-ordered, hence there is no condition, and you recover the formal_power_series. If G=ℤ, the well-ordered subsets are the ones bounded below, and you get the laurent_power_series when σ=unit.
The key point is the definition of the multiplication, and this can be done wiht the usual formulae using that {(e,e')S×S' | e*e'=g} for any g in G and any S, S' well ordered subsets of G is finite.
I know this goes far away of what it is need for condensed mathematics, but my impression is that most the machinery to define this is already done in the mathlib.

[Xavier Xarles]

Of course, I meant G is a linear_ordered_comm_monoid, not just ordered.

[Peter Scholze]

I like these rings! It might be fun proving that, if $R$ is a field, one gets a spherically complete field this way

[Kevin Buzzard]

I had initially ruled out the approach of going via formal infinite series $\sum_{n\in\Z}a_nT^n$ because these formal infinite series are not a ring, but I see now that you can just put a multiplication on the subtype. Meh, so now we have some implementation decision. I've seen these Hahn series before within the context of higher rank valuations. The Wikipedia page you link to only sets up the one-variable theory. I convinced myself that Laurent series would work even for infinitely many variables -- there are many topologies (even in the two-variable case there are at least three choices), but the algebra is unambiguous.

Maybe I'll leave Laurent series for now and try one of the other things Johan suggested.

[Aaron Anderson]

Xavier Xarles said:

There is another notion of something related to Laurent series, but much more abstract, that could be defined in Lean, is that of Hahn series:
https://en.wikipedia.org/wiki/Hahn_series
It could be defined as the series formed by the elements f in (σ →₀ G) → R , where R is a semiring, G an ordered_comm_monoid, whose support (to be defined) is well-ordered (i.e. any non-empty subset of the support of f has a least element), and in principle σ is finite (I did not check if it could work for any σ). If G= ℕ, all the subsets are well-ordered, hence there is no condition, and you recover the formal_power_series. If G=ℤ, the well-ordered subsets are the ones bounded below, and you get the laurent_power_series when σ=unit.
The key point is the definition of the multiplication, and this can be done wiht the usual formulae using that {(e,e')S×S' | e*e'=g} for any g in G and any S, S' well ordered subsets of G is finite.
I know this goes far away of what it is need for condensed mathematics, but my impression is that most the machinery to define this is already done in the mathlib.

I've wanted to do Hahn series for ages, but every time I try, I get disappointed with how hard it is to work with well-founded subsets, rather than well-founded types. That API should still get built, and I still intend to get around to it if no one else does first.

[Kevin Buzzard]

Do you know if there's a multivariable version?

[Adam Topaz]

@Kevin Buzzard what do you mean by multivariable?

[Adam Topaz]

One natural thing you can do when you have two ordered groups $\Gamma_1$ and $\Gamma_2$ Is take their product $\Gamma := \Gamma_1 \times \Gamma_2$ with the lexicographic ordering, and consider the Hahn series field $k((t^\Gamma))$.

[Kevin Buzzard]

Right. But I think I'm asking something different. For example you can get single variable power series by applying the construction with Gamma=nat. But I don't think the construction in Wikipedia will give you power series in two variables...oh, does it? I just take nat^2? Oh!

[Kevin Buzzard]

They stick to ordered groups in Wikipedia but ordered monoids seem to work fine

[Adam Topaz]

But you won't get a valuation ring in general.

[Adam Topaz]

(I don't know if this matters to you :) )

[Kevin Buzzard]

I might get a valuation though

[Adam Topaz]

Does every totally ordered monoid embed in its group completion?

[Kevin Buzzard]

I'll have to look at what mathlib thinks a totally ordered monoid is. If a<b implies a+c<b+c then you're fine because this implies a!=b -> a+c != b+c which is what you need for an embedding. But if the axiom is a<=b implies a+c<=b+c then there problems because {0,1,2} with absorbing 2 (1+2=2 etc) is a counterexample

[Kevin Buzzard]

docs#linear_ordered_monoid

[Kevin Buzzard]

docs#ordered_monoid

[Kevin Buzzard]

Hmm, maybe they have to be commutative?

[Kevin Buzzard]

docs#linear_ordered_comm_monoid

[Kevin Buzzard]

Apparently they don't exist in Lean?

[Kevin Buzzard]

docs#linear_ordered_comm_monoid_with_zero

[Kevin Buzzard]

Those exist but the < axiom isn't there because you can have c=0

[Kevin Buzzard]

Maybe this is the way to think about it. A partial order on something is a binary relation. But which relation? We often use $\leq$ but $<$ is just as fundamental: in a partial order $a<b$ iff $a\leq b$ and $a\not=b$, and conversely $a\leq b$ iff $a<b$ or $a=b$. Now consider the function $f:\R\to\R$ defined by $f(x)=0$. Is this monotonic, i.e. does it preserve the partial order? Well, $a\leq b\implies f(a)\leq f(b)$ is true, and $a<b\implies f(a)<f(b)$ is false. Perhaps people say "monotonic" for $\leq$-preserving, and "strictly monotonic" for $<$-preserving. Looking at the relationship between $\leq$ and $<$ you can see that the dictionary mentions $=$ and $\not=$. Now every map is $=$-preserving -- this is the so-called substitution property of equality, known to Lean as eq.rec. But the $\not=$-preserving maps are the injections, and your question is about injections.

The fact that in some sense we don't know whether the fundamental operator which we should be considering is $\leq$ or $<$ thus gives us this ambiguity when defining morphisms (should they be monic or strict monic?). But it also gives us ambiguity when defining algebraic structures on top of partial orders. Let's try to guess what an ordered commutative semiring should be. There are completely natural definitions for both $\leq$ and $<$. For addition we can say $a\leq b\implies a+c\leq b+c$ and $a\leq b, 0\leq c\implies ac\leq bc$. Or we can say $a<b\implies a+c<b+c$ and $a<b,0<c\implies ac<bc$. These give us different answers. Even for commutative totally ordered additive monoids they're different because fin n = $\{0,1,2,\ldots,n-1\}$ with its absorbing addition (a+b:=n-1 if real a+b is >= n-1) is $\leq$-preserving but not $<$-preserving, and this is happening because $x\mapsto x+a$ might not be injective if we just preserve $\leq$ but it must be injective if we preserve $<$ because preserving $<$ on a total order is the same as preserving $\leq$ and $\not=$.

I think that if we stick to total orders then this related to the question of whether a morphism of structures-with-a-binary-relation $R$ should satisfy $R(a,b)\implies R(f(a),f(b)$ or whether it should satisfy $R(a,b)\iff R(f(a),f(b)))$. Ultimately both concepts are useful. If you preserve $<$ on a total order then you also preserve $>$ and so $a<b\iff f(a)<f(b)$. However if you only preserve $\leq$ then you might not reflect it (i.e. $f(a)\leq f(b)$ might not imply $a\leq b$).

In short, it seems to me that there are two reasonable (from the point of view of model theory) definitions of a totally ordered commutative monoid, and the answer to your question is "yes" for one and "no" for the other.

[Kevin Buzzard]

Ok I thought more about Hahn series and Laurent series. @Aaron Anderson what do you think about this. Make a typeclass for well-founded subsets of a totally ordered type and try to get it to do the work. Define Hahn series for a totally ordered commutative add_monoid. The main goals are that power series in 1 variable are isomorphic to Hahn series if the monoid is $\N$ and that power series in one variable X and then invert X is isomorphic to Hahn series if the monoid is $\Z$.

[Kevin Buzzard]

These two results will probably inform the API for well-ordered subsets of a totally ordered type/abelian additive group. Note that Hahn series can be defined as functions to Gamma whose support is well-ordered and we have the API for support already

[Kevin Buzzard]

Also I think one can construct a valuation from Hahn series on Gamma to with_zero (multiplicative Gamma) and this would be another good test of the API

[Kevin Buzzard]

For me this sounds like a really fun couple of worlds in the lean puzzle game

[Kevin Buzzard]

The other approach I was considering was just localising power series at the variable, but now I believe that the Hahn approach is much better. We'll need Hahn series one day anyway (they came up in the document we had to formalise perfectoid spaces but we skipped them) so we may as well do them now. Defining a Laurent series as a localisation is one line but then making the API for coefficients is a slight hassle; this way the coefficients will be easy. Finally localising power series gives a several variable version of Laurent series but I can't see the use of it. It's not even true that k((X))((Y))=k((Y))((X)), and neither these nor the localisation of k[[X,Y]] at X and Y is the field of fractions of k[[X,Y]] anyway, as far as I can see, so I can't really see any use in a multivariable Laurent series or even a natural construction, however if we do Hahn series we can apply to Z x Z and claim that this is something (I think it's k((X))((Y)) )

[Filippo A. E. Nuccio]

Well, actually my game with the add_comm_monoid structure on $\mathbb{N}$ this morning was aimed precisely at a definition of the Laurent series, without Hahn series. I think this should be doable, but I prefer not to interfere, basically because these Hahn series are probably more general, and because I am having enough fun in defining them that I'd go on even if it turns out that you will opt for another definition. Also, I can't spend too much time on this and I am very slow, so I don't feel like blocking anyone.

[Adam Topaz]

Concerning the "multivariable" issue -- I think it is actually reasonable to think about $k((t^\Gamma))$ with $\Gamma = \mathbb{Z} \times \mathbb{Z}$ as a 2-variable object. We just have to keep in mind that $\Gamma$ is not a plain group, but rather an ordered group, so the convex subgroup $\mathbb{Z} \times 0$ is "canonical" in the sense that it's the unique nontrivial proper convex subgroup. This corresponds to the coarsening of the valuation on $k((t^\Gamma))$ whose residue field is the Hahn series field of the quotient $(\mathbb{Z} \times \mathbb{Z} )/( \mathbb{Z} \times 0 )\cong \mathbb{Z}$.

In other words, $k((t^\Gamma))$ has it's usual canonical valuation $v$ with value group $\Gamma$, but there is also a "canonical" valuation $w$ which coarsens $v$ whose value group is $\mathbb{Z}$ and the induced valuation on the residue field of $w$ again has value group $\mathbb{Z}$.

Geometrically, this should be thought of as the completion of a function field of a surface at a rank-2 flag of prime divisors. So in this sense, it really is a 2-dimensional object.

[Adam Topaz]

In any case, I completely agree that it would be a fun project to formalize this stuff :)

[Aaron Anderson]

Kevin Buzzard said:

Ok I thought more about Hahn series and Laurent series. Aaron Anderson what do you think about this. Make a typeclass for well-founded subsets of a totally ordered type and try to get it to do the work. Define Hahn series for a totally ordered commutative add_monoid. The main goals are that power series in 1 variable are isomorphic to Hahn series if the monoid is $\N$ and that power series in one variable X and then invert X is isomorphic to Hahn series if the monoid is $\Z$.

Starting over at #6113

[Filippo A. E. Nuccio]

I've defined some Laurent series, and the discussion is here:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Hahn.20Series/near/226499114

[Aaron Anderson]

Kevin Buzzard said:

Also I think one can construct a valuation from Hahn series on Gamma to with_zero (multiplicative Gamma) and this would be another good test of the API

I'm aaaalmoooost there, and I've just found out that the order is backwards.

[Aaron Anderson]

I might just slap on a negative sign today, but this convinces me: we need a separate add_valuation definition (and possibly to flip the order on multiplicative)

[Kevin Buzzard]

I know exactly what you're talking about :-) This happens already for DVR s

[Adam Topaz]

Can we just introduce a negative_log already? :smile:

[Aaron Anderson]

Would it be a problem to define add_valuation directly for now, and then figure out how to connect it to valuation?

[Aaron Anderson]

It seems like a better idea than just leaving the valuation on DVRs totally unbundled

[Aaron Anderson]

It also looks like we don't even have the p-adic valuation as a valuation?

[Adam Topaz]

We have "the p-adic absolute value", right?

[Adam Topaz]

docs#padic.is_absolute_value

[Adam Topaz]

Oh, I see, you want the bundled docs#valuation version.

[Adam Topaz]

Oh, this is a mess: docs#padic.valuation is the additive valuation, but it's just a plain function

[Aaron Anderson]

I'm going to venture a guess that we have more unbundled additive valuations than we have bundled multiplicative valuations...

[Aaron Anderson]

...but then polynomial.degree could be an additive valuation (if defined on monoids), but the order would be follow the multiplicative convention. What a headache.

[Aaron Anderson]

Adam Topaz said:

Can we just introduce a negative_log already? :smile:

What would this do?

[Adam Topaz]

Take an ordered multiplicative monoid and map to an additive monoid with the opposite ordering.

[Aaron Anderson]

So would this be a class/structure of bundled functions that do that, or would this be an explicit construction of one such function?

[Adam Topaz]

I haven't actually thought about how to do this.

[Kevin Buzzard]

We want it to go from an additive monoid with a top to a monoid with zero

[Filippo A. E. Nuccio]

I've just seen the discussion you had yesterday about valuation vs add_valuation but I think I miss the point. @Aaron Anderson What do you mean that "the order is backwards"?

[Kevin Buzzard]

Is v(1) < v(p) or not? Depends on whether v is the additive or multiplicative valuation

[Filippo A. E. Nuccio]

And do I also get it right that the add_val you created in the discrete_val_ring file is not OK for the work here, since it definitionally takes values in N?

[Kevin Buzzard]

That is an auxiliary definition which can easily be turned into a valuation in this sense

[Kevin Buzzard]

The reason I stopped afterwards is that the actual structure I wanted was not there. Aaron is making it now. I just mimiced the structure we had on the p-adic numbers

[Filippo A. E. Nuccio]

Namely, having a the def of multiplicative valuation and obtain the additive one automatically?

[Kevin Buzzard]

The point is that there is no definition of the structure of an additive valuation in mathlib (and more generally no structure encapsulating f(a*b)=f(a)+f(b) so we can't talk about additive valuations at all, until now. It's just a missing definition, nothing profound. But every definition comes with a cost -- the cost of making the API for the definition.

[Aaron Anderson]

Compare the additive axiom of a valuation in the multiplicative and additive versions. In one version, you have v(x + y) <= max (v(x), v(y)), in the other, you have min(v(x),v(y)) <= v(x + y).

[Filippo A. E. Nuccio]

Oh, now I understand (looked up in wikipedia). What you call a "multiplicative valuation with values in $\mathbb{R}$" is an absolute value, and the "multiplicative valuations" generalize this to other codomains. Right?

[Aaron Anderson]

Absolute values are different yet still, as there you want v(x + y) <= v(x) + v(y).

[Aaron Anderson]

A multiplicative valuation with values in $\mathbb{R}$ is an ULTRAmetric absolute value, which is stronger.

[Aaron Anderson]

My Laurent series PR has finally arrived: #7604

[Aaron Anderson]

Taking requests for the API beyond this localization map.

[Filippo A. E. Nuccio]

@Aaron Anderson I was looking at the file hahn_series and I see it still says that still remain TO DO

  * Given `[linear_ordered_add_comm_group Γ]` and `[field R]`, define `field (hahn_series Γ R)`.
  * Build an API for the variable `X`
  * Define Laurent series

But it seems to me that the third is OK, and I don't understand what is the second exactly. What about the first? Also, don't you think it would be nicer to point at the file laurent_series in this doc so that one knows where to look at, if needed?

[Aaron Anderson]

You're right, I need to update that. Documentation PR coming ASAP.

[Aaron Anderson]

#8883

[Filippo A. E. Nuccio]

Thanks!