# Zulip Chat Archive

## Stream: maths

### Topic: log

#### Kevin Buzzard (Jan 08 2021 at 12:53):

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

s had a `top`

and my `monoid`

s 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 (Jan 08 2021 at 12:54):

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 (Jan 08 2021 at 12:57):

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

#### Eric Wieser (Jan 08 2021 at 13:01):

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

#### Eric Wieser (Jan 08 2021 at 13:04):

Also `git blame`

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

#### Kevin Buzzard (Jan 08 2021 at 14:10):

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).

Last updated: May 11 2021 at 16:22 UTC