There are no `canonically_linear_ordered_monoid`s

Stream: maths

[Kevin Buzzard]

In #5286 Bryan pointed out that mathlib has canonically_linear_ordered_add_monoid (and very natural types like the naturals, and nnreal, are instances of this), but it does not have the multiplicative version canonically_linear_ordered_monoid. He suggested I add it because it was very much in the spirit of the PR.

I initially accepted because I thought that the ideals of a Dedekind domain would be a canonically linearly ordered monoid under multiplication. But now I realise they are not -- they satisfy $I\leq J\iff \exists K, I=J*K$ -- multiplication makes things smaller rather than bigger ("canonical" in the additive setting means $a\leq b\iff \exists c, b=a+c$ which is true for $\mathbb{N}$). The non-existing class $[1,\infty)$ of reals at least 1 (or rationals at least 1) would be an instance of canonically_linear_ordered_monoid, but these classes are not in mathlib and I don't see any compelling reason to add them.

However in valuation theory one would be interested in $[0,1]$ as a totally ordered monoid, and also examples such as $\{0\}\cup\{p^{-n}\,|\,n\in\mathbb{N}\,\}$, because these are the target monoids for the $p$-adic valuation on the $p$-adic integers (and also on the usual integers $\mathbb{Z}$). All of these (plus ideals of Dedekind domains) are also examples of totally ordered monoids which are "anti-canonically ordered": $a\leq b\iff \exists c, a=bc$. In particular I know of no natural canonically_linear_ordered_monoids but I can think of several totally ordered monoids for which their order_dual is canonically_linear_ordered_monoid. I was surprised by this! Is this enough of an argument for adding canonically_linear_ordered_monoid? It seemed to me that this was a pretty weak argument and we would rather have anticanonically_linear_ordered_monoid if anything at all, but then of course we don't get all the to_additive goodies. Adding canonically_linear_ordered_monoid when there are no instances in mathlib seemed like a pretty random thing to do and my instinct now is not to do it. Does anyone have any thoughts on whether this should be done anyway? I'll happily do it if I can see that there's a good reason to add another class to the heirarchy...

[Johan Commelin]

this "contravariance" indeed seems very funny. It's exactly what happens when you move between additive and multiplicative valuations

[Johan Commelin]

What is the additive analogue of an ordered_group_with_zero? It should be some ordered_add_group_with_top

[Kevin Buzzard]

Exactly. Indeed you can see this in ordered_monoid.lean -- there's a with_zero section (actually namespace) proving results about ordered_comm_monoids and then a with_top section proving results about ordered_add_comm_monoids.

[Kevin Buzzard]

This Lean separation of + and * has always been of interest to me because even though people say "well formally everything is the same, in Agda there's only one group" or whatever, in practice addition and multiplication are treated differently by mathematicians. The analysts have exp and log which are order-preserving and switch one to the other, but the p-adic exp and log have no order to preserve, and the valuation dictionary is order-reversing.

[Kevin Buzzard]

Aah, the ordered_add_comm_monoid also has a with_bot section! I guess one uses this for stuff like degree of a polynomial (deg(fg)=deg(f)+deg(g) is true for all f,g in with_bot nat, although the ordering is weird because f | g implies deg(f)<=deg(g) or deg(g)=bot -- this is so confusing! )

[Kevin Buzzard]

Got one! associates R for R a DVR :D

[Adam Topaz]

Kevin, isn't this a canonically_linearly_ordered_monoid_with_zero?

[Kevin Buzzard]

Indeed it is :-)

[Kevin Buzzard]

except that I strongly suspect that these don't exist...