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_monoids had a
top and my
monoids had a zero, and exp sent top to zero (my functions are like for 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 and 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):
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 in maths (the infinite cyclic group).
Last updated: May 11 2021 at 16:22 UTC