# Zulip Chat Archive

## Stream: maths

### Topic: There are no `canonically_linear_ordered_monoid`s

#### Kevin Buzzard (Dec 17 2020 at 12:56):

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_monoid`

s 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 (Dec 17 2020 at 12:59):

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

#### Johan Commelin (Dec 17 2020 at 13:00):

What is the additive analogue of an `ordered_group_with_zero`

? It should be some `ordered_add_group_with_top`

#### Kevin Buzzard (Dec 17 2020 at 13:02):

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_monoid`

s.

#### Kevin Buzzard (Dec 17 2020 at 13:04):

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 (Dec 17 2020 at 13:07):

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 (Dec 17 2020 at 17:16):

Got one! `associates R`

for `R`

a DVR :D

#### Adam Topaz (Dec 17 2020 at 17:56):

Kevin, isn't this a `canonically_linearly_ordered_monoid_with_zero`

?

#### Kevin Buzzard (Dec 17 2020 at 18:07):

Indeed it is :-)

#### Kevin Buzzard (Dec 17 2020 at 18:07):

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

Last updated: May 10 2021 at 07:15 UTC