ordered_comm_monoid (with_zero α)

Stream: general

[Kevin Buzzard]

Three years ago @Mario Carneiro added with_zero and wrote this line making with_zero of an ordered_comm_monoid and ordered_comm_monoid, but he used instance rather than def and, this being three years ago, there's no explanation as to why. Is there a reason for this or is it just an oversight?

This is the type with the bad name -- it should have beenordered_add_comm_monoid (and it now is); I am now un-to-additiving everything. Interestingly, to_additive changes the hypothesis one_le into not zero_le but nonneg :-)

[Eric Wieser]

but he used instance rather than def

I'm confused, the line you links to uses def. Did you say that backwards, or are you referring to a different version to the one the link goes to?

[Mario Carneiro]

What needs explanation here exactly? This is showing sufficient conditions for a with_zero to be a ordered_comm_monoid

[Mario Carneiro]

I'm not saying this is a recommended construction or anything, it's just a factoid

[Mario Carneiro]

As Eric says, it's not an instance, and even if it wasn't a really bizarre instance it can't be one because of the non-typeclass hypothesis

[Kevin Buzzard]

Sorry, I meant "he used def rather than instance" -- and now I see why. Thanks!

[Kevin Buzzard]

Related: we have instance [partial_order α] : partial_order (with_zero α) := with_bot.partial_order. Is this insanity? Can I do instance [partial_order α] : partial_order (with_one α) := with_bot.partial_order? It would make to_additive happy!

[Adam Topaz]

instance [partial_order α] : partial_order (with_one α) := with_bot.partial_order is surely insanity, e.g. for Ico 0 1.

[Mario Carneiro]

If anything it should be with_top.partial_order

[Mario Carneiro]

I think it's okay if not everything in this space is using to_additive. It's not true that literally everything is the same, or else we wouldn't have two names for "addition" and "multiplication"

[Kevin Buzzard]

Mario Carneiro said:

If anything it should be with_top.partial_order

Yes exactly! There is some weird duality going on here in the kind of applications we're thinking about. The standard additive p-adic valuation on the integers takes values in with_top nat, sends p^n to n and 0 to +infinity. The standard multiplicative valuation takes values in nnreal or even [0,1], sends p^n to p^{-n} and 0 to 0. The translation from the additive to the multiplicative world is order-reversing.

[Mario Carneiro]

I think the safest thing is just not to put an order

[Kevin Buzzard]

I would really like to have a name for the object {0} union {e^n} where n : nat and you can think of e as being a real between 0 and 1; I just need this abstract object as a totally ordered commutative monoid with 0. It's the fundamental monoid which receives the multiplicative valuation on any discrete valuation ring. For example if k is any field then there's a multiplicative valuation on the power series ring $k[[T]]$ sending $aT^n+bT^{n+1}+\cdots$ to $e^n$ if $a\not=0$, and sending $0$ to $0$. This is a monoid homomorphism into a fundamental object which doesn't seem to have a name in mathlib yet.

[Kevin Buzzard]

The target of the additive version does have a name -- here $aT^n+\cdots$ gets sent to $n$ and $0$ goes to \top; the target space is with_top nat but with these conventions the map doesn't have a name because it satisfies $v(ab)=v(a)+v(b)$.

[Kevin Buzzard]

So the thing I want is multiplicative (order_dual (with_top nat))) and this is not going to be much fun to work with I suspect.

[Kevin Buzzard]

If I can name it I can make an API for it (it's an anti-canonically-linear-ordered-monoid!) but I don't know what to call it! Mathematicians don't have a name for it as far as I know.

[Kevin Buzzard]

Its with_zero_group of fractions is with_zero (multiplicative int) which also doesn't have a name.

[Kevin Buzzard]

or strictly speaking with_zero (multiplicative (order_dual int)) but you can't see the order_dual, it's just that the canonical map from the nat thing sends n to -n.

[Mario Carneiro]

you could just go ahead and give it a name

[Mario Carneiro]

co_enat? I have no idea