with_zero (multiplicative int)

Stream: maths

[Kevin Buzzard]

I would like to define a new constant $\Gamma_0$, which is the multiplicative monoid whose terms are the constant 0 and the termsq^n for n : int. You can put a bunch more structure on it, especially if you start pretending that q is a complex number with norm less than 1, or q is a $p$-adic number becuause you're doing $p$-adic modular forms (e.g. in some of my papers doing explicit calculations with Calegari we use precisely this abstract $\Gamma_0$ at times).

The goal would be to make the constant and then, like the real numbers, write down the universal property which classifies it up to unique isomorphism amongst monoids with a 0 and an invertible q.

Does anyone have any comments on whether such a thing is a good or bad idea? It is blocking development of DVRs; these are my current thoughts on how to proceed. I want to show that a valuation ring has a valuation on it, in the sense of mathlib, and this is the natural target monoid.

One thing that happened during the perfectoid project was that Johan and my understanding of how to think about valuations developed, we came across this whole idea about a valuation being a monoid hom to a monoid with zero. I wanted to set things up in this generality (and I still kind of think that we should -- am I right?) but I kept being busy with work stuff and Johan just set it all up so that a valuation has to go to a group with zero. I am wondering if that decision will come back to bite us but I'm not sure if it will. If I'm really supposed to be working with monoids with zero then I might find later on that I need a name for the nat analogue of the construction above, i.e. with_zero (multiplicative nat). Again one can prove a universal property.

[Adam Topaz]

This is the free group_with_zero on one generator $q$, right?

[Adam Topaz]

So I agree this is a natural target for a discrete valuation (of rank 1), but the notation $\Gamma$ is also used for the value group of an arbitrary valuation.

[Adam Topaz]

Also, I think defining this as a constant will get annoying when one starts talking about ramification.

[Adam Topaz]

This is a silly observation: You can define a "hypersemiring" structure on a totally ordered comm_group_with_zero where multiplication is as above, and addition of two elements $a,b$ is multivalued (the interval $[0,max(a,b)]$). Any commutative ring is a hyperring in the obvious sense, and a valuation then just becomes a morphism of hyperrings.

[Bryan Gin-ge Chen]

Hyperrings and other hyperstructures would be fun to see formalized. Hyperfields (and various generalizations / variants) have gotten some attention recently in the theory of matroids, per https://arxiv.org/abs/1709.09707 and https://arxiv.org/abs/1809.03542.

[Adam Topaz]

Also, when you view valuation theory via hyperrings, things like tropical geometry become more natural :)

[Kevin Buzzard]

@Johan Commelin hope you're having a happy holiday; you'll like this.

[Kevin Buzzard]

There's a canonical map from nat to End(Gamma0) ($g\mapsto g^n$) and when talking abut ramification one just uses these maps.

[Kevin Buzzard]

PS I don't care what we call it, I just think it's deserving of a name.

[Adam Topaz]

Is it possible to introduce general notation that works for any ordered abelian group?

[Adam Topaz]

Yeah, the ramification thing is not much of an issue. My thought was mainly that if/when we have algebraic closures, discretely valued fields, etc, we would want a nice way to say that the value group of a prolongation to the algebraic closure has to be $\mathbb{Q}$.

[Adam Topaz]

But this can be done with divisible hulls, etc.

[Kevin Buzzard]

We have a general theory of valuations of fields so this is no problem. "Independent" of the theory of valuations on fields is the theory of discrete valuations on fields -- I think.

[Adam Topaz]

I don't think they're independent.

[Adam Topaz]

At least mathematically.