# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: laurent series

#### Kevin Buzzard (Feb 02 2021 at 15:43):

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 (Feb 02 2021 at 15:44):

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

#### Peter Scholze (Feb 02 2021 at 15:45):

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

#### Kevin Buzzard (Feb 02 2021 at 15:45):

I think there's a well-defined map from the localisation to the $R$-module `(σ →₀ ℤ) → R`

although 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 (Feb 02 2021 at 15:46):

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

#### Peter Scholze (Feb 02 2021 at 15:50):

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 (Feb 02 2021 at 15:50):

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 (Feb 02 2021 at 15:50):

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

#### Kevin Buzzard (Feb 02 2021 at 15:50):

Yes, but this is just a gimmick

#### Kevin Buzzard (Feb 02 2021 at 15:50):

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

#### Peter Scholze (Feb 02 2021 at 15:50):

OK, that's the same

#### Peter Scholze (Feb 02 2021 at 15:51):

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

#### Kevin Buzzard (Feb 02 2021 at 15:51):

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

#### Johan Commelin (Feb 02 2021 at 15:52):

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 (Feb 02 2021 at 15:53):

Sounds good to me! Equalizers are just uglier to draw

#### Peter Scholze (Feb 02 2021 at 15:54):

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

#### Peter Scholze (Feb 02 2021 at 15:55):

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 (Feb 02 2021 at 16:08):

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]]:=$`(σ →₀ ℕ) → R`

in 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 (Feb 02 2021 at 16:10):

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 (Feb 02 2021 at 16:11):

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

#### Kevin Buzzard (Feb 02 2021 at 16:12):

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

#### Kevin Buzzard (Feb 02 2021 at 16:12):

I have students looking for projects.

#### Kevin Buzzard (Feb 02 2021 at 16:12):

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

#### Kevin Buzzard (Feb 02 2021 at 16:13):

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

#### Peter Scholze (Feb 02 2021 at 16:13):

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

#### Johan Commelin (Feb 02 2021 at 16:13):

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

#### Peter Scholze (Feb 02 2021 at 16:13):

Yes, basic intuition about dimensions gets pretty safely fucked up

#### Kevin Buzzard (Feb 02 2021 at 16:14):

(it was Judith Ludwig who taught me this)

#### Filippo A. E. Nuccio (Feb 02 2021 at 16:21):

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 (Feb 02 2021 at 16:23):

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

#### Kevin Buzzard (Feb 02 2021 at 16:43):

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 (Feb 02 2021 at 16:54):

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

#### Xavier Xarles (Feb 05 2021 at 09:41):

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 (Feb 05 2021 at 09:49):

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

#### Peter Scholze (Feb 05 2021 at 09:50):

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 (Feb 05 2021 at 11:38):

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 (Feb 06 2021 at 22:45):

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 (Feb 06 2021 at 23:08):

Do you know if there's a multivariable version?

#### Adam Topaz (Feb 06 2021 at 23:17):

@Kevin Buzzard what do you mean by multivariable?

#### Adam Topaz (Feb 06 2021 at 23:21):

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 (Feb 06 2021 at 23:40):

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 (Feb 06 2021 at 23:44):

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

#### Adam Topaz (Feb 06 2021 at 23:47):

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

#### Adam Topaz (Feb 06 2021 at 23:47):

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

#### Kevin Buzzard (Feb 06 2021 at 23:55):

I might get a valuation though

#### Adam Topaz (Feb 07 2021 at 00:03):

Does every totally ordered monoid embed in its group completion?

#### Kevin Buzzard (Feb 07 2021 at 07:05):

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 (Feb 07 2021 at 07:06):

#### Kevin Buzzard (Feb 07 2021 at 07:07):

#### Kevin Buzzard (Feb 07 2021 at 07:09):

Hmm, maybe they have to be commutative?

#### Kevin Buzzard (Feb 07 2021 at 07:13):

docs#linear_ordered_comm_monoid

#### Kevin Buzzard (Feb 07 2021 at 07:16):

Apparently they don't exist in Lean?

#### Kevin Buzzard (Feb 07 2021 at 07:17):

docs#linear_ordered_comm_monoid_with_zero

#### Kevin Buzzard (Feb 07 2021 at 07:18):

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

#### Kevin Buzzard (Feb 07 2021 at 09:26):

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 (Feb 08 2021 at 13:23):

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 (Feb 08 2021 at 13:24):

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 (Feb 08 2021 at 13:26):

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 (Feb 08 2021 at 13:27):

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

#### Kevin Buzzard (Feb 08 2021 at 13:34):

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 (Feb 08 2021 at 14:00):

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 (Feb 08 2021 at 14:28):

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 (Feb 08 2021 at 14:29):

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

#### Aaron Anderson (Feb 09 2021 at 04:53):

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 (Feb 16 2021 at 10:58):

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 (Mar 01 2021 at 22:46):

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 (Mar 01 2021 at 22:47):

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 (Mar 01 2021 at 22:57):

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

#### Adam Topaz (Mar 01 2021 at 22:58):

Can we just introduce a `negative_log`

already? :smile:

#### Aaron Anderson (Mar 01 2021 at 23:01):

Would it be a problem to define `add_valuation`

directly for now, and then figure out how to connect it to `valuation`

?

#### Aaron Anderson (Mar 01 2021 at 23:04):

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

#### Aaron Anderson (Mar 01 2021 at 23:06):

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

?

#### Adam Topaz (Mar 01 2021 at 23:07):

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

#### Adam Topaz (Mar 01 2021 at 23:08):

#### Adam Topaz (Mar 01 2021 at 23:08):

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

#### Adam Topaz (Mar 01 2021 at 23:13):

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

#### Aaron Anderson (Mar 01 2021 at 23:14):

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

#### Aaron Anderson (Mar 01 2021 at 23:15):

...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 (Mar 01 2021 at 23:45):

Adam Topaz said:

Can we just introduce a

`negative_log`

already? :smile:

What would this do?

#### Adam Topaz (Mar 01 2021 at 23:47):

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

#### Aaron Anderson (Mar 01 2021 at 23:50):

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 (Mar 01 2021 at 23:51):

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

#### Kevin Buzzard (Mar 02 2021 at 07:38):

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

#### Filippo A. E. Nuccio (Mar 04 2021 at 08:04):

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 (Mar 04 2021 at 08:07):

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

#### Filippo A. E. Nuccio (Mar 04 2021 at 08:11):

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 (Mar 04 2021 at 08:15):

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

#### Kevin Buzzard (Mar 04 2021 at 08:16):

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 (Mar 04 2021 at 08:18):

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

#### Kevin Buzzard (Mar 04 2021 at 09:14):

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 (Mar 04 2021 at 16:48):

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 (Mar 04 2021 at 17:00):

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 (Mar 04 2021 at 17:19):

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

.

#### Aaron Anderson (Mar 04 2021 at 17:20):

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

Last updated: May 09 2021 at 22:13 UTC