log

Stream: maths

[Kevin Buzzard]

In @Adam Topaz 's talk at LT2021 he defined a log function (link to repo) between fields. This is some sort of fundamental construction which I think should probably be made in more generality -- perhaps from any monoid to an add_monoid? In this situation it's simply what a mathematician would call a morphism of monoids. Perhaps if 0 is important one could define it from a monoid_with_zero to an add_monoid. The inverse is exp, which has come up in my own work on valuations. exp is a function from an add_monoid to a monoid preserving the monoid law and sending 0 to 1. Again there is an "extra" in the situation I was interested in -- my add_monoids had a top and my monoids had a zero, and exp sent top to zero (my functions are like $e^x$ for $0<e<1$ so they're order-reversing).

I find it fascinating that this design decision to bundle the group law notation into the definition did not completely derail the construction of a maths library. In essentially every example we've seen so far of morphisms of monoids, the natural monoid law notation is the same on both sides. There's quite a well-developed theory of additive valuations on rings (these are like exp) taking values in $\mathbb{N}\cup\infty$ and $\mathbb{Z}\cup\infty$ but when one starts generalising valuations a la Huber/Scholze one seems to slip back into the multiplicative notation. I am currently confused about whether the switch from multiplication to addition is somehow a profound thing which represents some fundamental change of viewpoint or whether this is all just noise and it's a fluke that most morphisms of monoids in mathlib so far happen to be not just operation-preserving but also notation-preserving.

[Eric Wieser]

Well, the ones which aren't notation preserving we work around with monoid_hom X (multiplicative Y), right? I think we do have that in a handful of places.

[Kevin Buzzard]

My grepping regex skills are not good enough for me to be able to find any

[Eric Wieser]

docs#powers_mul_hom is one example, but maybe there aren't as many as I thought

[Eric Wieser]

Also git blame reveals I added that one myself, so that's not a terribly good example of established convention

[Kevin Buzzard]

Aah I looked for multiplicative on the other side. Furthermore this is not a "general" result -- this is specifically about multiplicative int which I think deserves its own notation in mathlib -- it is $C_\infty$ in maths (the infinite cyclic group).