Zulip Chat Archive

Stream: condensed mathematics

Topic: laurent series


view this post on Zulip 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 RR defined as (σ →₀ ℕ) → R (so in particular X1+X2+X3+X_1+X_2+X_3+\cdots is allowed if all the XiX_i are variables). If RR 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?

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Feb 02 2021 at 15:45):

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

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 15:45):

I think there's a well-defined map from the localisation to the RR-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).

view this post on Zulip Peter Scholze (Feb 02 2021 at 15:46):

Localization also has a universal property on RR-modules

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 15:50):

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

view this post on Zulip Peter Scholze (Feb 02 2021 at 15:50):

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

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 15:50):

Yes, but this is just a gimmick

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 15:50):

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

view this post on Zulip Peter Scholze (Feb 02 2021 at 15:50):

OK, that's the same

view this post on Zulip Peter Scholze (Feb 02 2021 at 15:51):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 02 2021 at 15:52):

Note that in LTE I also define the (_)T1(\_)^{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.

view this post on Zulip Peter Scholze (Feb 02 2021 at 15:53):

Sounds good to me! Equalizers are just uglier to draw

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 16:08):

So to give an A[1/S]A[1/S]-module is to give an AA-module on which the elements of SS act as bijections -- thanks Peter! Now if RR is a commutative ring (or probably even a commutative semiring) then M:=M:=(σ →₀ ℤ) → R is a module for the ring A=R[[σ]]:=A = R[[\sigma]]:=(σ →₀ ℕ) → Rin which the elements of σ\sigma act as bijections, so it's a module for A[1/σ]A[1/\sigma], and now you can define a map A[1/σ]MA[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 RR is an ID, a field if RR 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!

view this post on Zulip Peter Scholze (Feb 02 2021 at 16:10):

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

view this post on Zulip Peter Scholze (Feb 02 2021 at 16:11):

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

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 16:12):

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

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 16:12):

I have students looking for projects.

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 16:12):

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

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 16:13):

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

view this post on Zulip Peter Scholze (Feb 02 2021 at 16:13):

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

view this post on Zulip Johan Commelin (Feb 02 2021 at 16:13):

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

view this post on Zulip Peter Scholze (Feb 02 2021 at 16:13):

Yes, basic intuition about dimensions gets pretty safely fucked up

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 16:14):

(it was Judith Ludwig who taught me this)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 16:54):

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

view this post on Zulip 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.

view this post on Zulip Xavier Xarles (Feb 05 2021 at 09:49):

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

view this post on Zulip Peter Scholze (Feb 05 2021 at 09:50):

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

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 11:38):

I had initially ruled out the approach of going via formal infinite series nZanTn\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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 06 2021 at 23:08):

Do you know if there's a multivariable version?

view this post on Zulip Adam Topaz (Feb 06 2021 at 23:17):

@Kevin Buzzard what do you mean by multivariable?

view this post on Zulip Adam Topaz (Feb 06 2021 at 23:21):

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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Feb 06 2021 at 23:44):

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

view this post on Zulip Adam Topaz (Feb 06 2021 at 23:47):

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

view this post on Zulip Adam Topaz (Feb 06 2021 at 23:47):

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

view this post on Zulip Kevin Buzzard (Feb 06 2021 at 23:55):

I might get a valuation though

view this post on Zulip Adam Topaz (Feb 07 2021 at 00:03):

Does every totally ordered monoid embed in its group completion?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 07:06):

docs#linear_ordered_monoid

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 07:07):

docs#ordered_monoid

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 07:09):

Hmm, maybe they have to be commutative?

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 07:13):

docs#linear_ordered_comm_monoid

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 07:16):

Apparently they don't exist in Lean?

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 07:17):

docs#linear_ordered_comm_monoid_with_zero

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 07:18):

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

view this post on Zulip 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<ba<b iff aba\leq b and aba\not=b, and conversely aba\leq b iff a<ba<b or a=ba=b. Now consider the function f:RRf:\R\to\R defined by f(x)=0f(x)=0. Is this monotonic, i.e. does it preserve the partial order? Well, ab    f(a)f(b)a\leq b\implies f(a)\leq f(b) is true, and a<b    f(a)<f(b)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 ab    a+cb+ca\leq b\implies a+c\leq b+c and ab,0c    acbca\leq b, 0\leq c\implies ac\leq bc. Or we can say a<b    a+c<b+ca<b\implies a+c<b+c and a<b,0<c    ac<bca<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,,n1}\{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 xx+ax\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 RR should satisfy R(a,b)    R(f(a),f(b)R(a,b)\implies R(f(a),f(b) or whether it should satisfy R(a,b)    R(f(a),f(b)))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    f(a)<f(b)a<b\iff f(a)<f(b). However if you only preserve \leq then you might not reflect it (i.e. f(a)f(b)f(a)\leq f(b) might not imply aba\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.

view this post on Zulip 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\N and that power series in one variable X and then invert X is isomorphic to Hahn series if the monoid is Z\Z.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 13:27):

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

view this post on Zulip 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)) )

view this post on Zulip Filippo A. E. Nuccio (Feb 08 2021 at 14:00):

Well, actually my game with the add_comm_monoid structure on N\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.

view this post on Zulip Adam Topaz (Feb 08 2021 at 14:28):

Concerning the "multivariable" issue -- I think it is actually reasonable to think about k((tΓ))k((t^\Gamma)) with Γ=Z×Z\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 Z×0\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Γ))k((t^\Gamma)) whose residue field is the Hahn series field of the quotient (Z×Z)/(Z×0)Z(\mathbb{Z} \times \mathbb{Z} )/( \mathbb{Z} \times 0 )\cong \mathbb{Z}.

In other words, k((tΓ))k((t^\Gamma)) has it's usual canonical valuation vv with value group Γ\Gamma, but there is also a "canonical" valuation ww which coarsens vv whose value group is Z\mathbb{Z} and the induced valuation on the residue field of ww again has value group Z\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.

view this post on Zulip 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 :)

view this post on Zulip 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\N and that power series in one variable X and then invert X is isomorphic to Hahn series if the monoid is Z\Z.

Starting over at #6113

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 22:57):

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

view this post on Zulip Adam Topaz (Mar 01 2021 at 22:58):

Can we just introduce a negative_log already? :smile:

view this post on Zulip 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?

view this post on Zulip Aaron Anderson (Mar 01 2021 at 23:04):

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

view this post on Zulip Aaron Anderson (Mar 01 2021 at 23:06):

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

view this post on Zulip Adam Topaz (Mar 01 2021 at 23:07):

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

view this post on Zulip Adam Topaz (Mar 01 2021 at 23:08):

docs#padic.is_absolute_value

view this post on Zulip Adam Topaz (Mar 01 2021 at 23:08):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Aaron Anderson (Mar 01 2021 at 23:45):

Adam Topaz said:

Can we just introduce a negative_log already? :smile:

What would this do?

view this post on Zulip Adam Topaz (Mar 01 2021 at 23:47):

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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Mar 01 2021 at 23:51):

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

view this post on Zulip 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

view this post on Zulip 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"?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 04 2021 at 08:15):

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

view this post on Zulip 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

view this post on Zulip Filippo A. E. Nuccio (Mar 04 2021 at 08:18):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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 R\mathbb{R}" is an absolute value, and the "multiplicative valuations" generalize this to other codomains. Right?

view this post on Zulip 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).

view this post on Zulip Aaron Anderson (Mar 04 2021 at 17:20):

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


Last updated: May 09 2021 at 22:13 UTC