non-mult valuation (or seminorm taking values outside reals)

Stream: Is there code for X?

[Scott Carnahan]

When R is a domain, the iterated Laurent series ring R((X))((Y)) has an additive valuation taking values in WithTop (ℤ ×ₗ ℤ) (docs#HahnSeries.addVal modulo #10781). However, if R has zero divisors, then we only have a weak version of multiplicativity, since the product of nonzero leading terms can vanish. We have a suitable weakening of multiplicativity in the context of seminorms of rings, but there, the values are restricted to non-negative reals. Is there interest in a "least common generalization", i.e., either a generalization of the values taken by seminorms, or an inequality in the multiplicativity condition for valuations?

[Kevin Buzzard]

The valuations used in the theory of adic spaces/perfectoid spaces can be higher rank but they need to satisfy the strong version of multiplicativity, which might be one reason that we have things set up as they are now. In particular I don't think we can change the definition to allow submultiplicativity because we need the version as stated. I don't really understand your example in some sense. If you're just computing the order of vanishing then maybe implicitly you're putting a norm on R with |0|=0 and |r|=1 for r nonzero and for me it feels like that's a bit weird because that's a poorly-behaved norm already, even before we start talking about laurent series. Are these higher rank seminorms actually useful anywhere? Note that we have the degree of a polynomial and that's also not well-behaved for the same reason but we just made an API for degree of a polynomial rather than introducing a new abstraction.

[Scott Carnahan]

Thank you for thinking about it. I don't have a concrete application in mind - I was asking out of curiosity.