monoid_hom from additive to multiplicative structures

Stream: Is there code for X?

[Apurva Nakade]

Is there any bundled way to encode the fact that pow is a monoid morphism from the additive structure on nat to the multiplicative structure, of say, a monoid M (for a fixed base m : M).

[Yakov Pechersky]

We can make a tropical hom and untropical homs, I guess.

[Apurva Nakade]

My problem is very low key for this much technology! I'll just leave the three lemmas unbundled for now.

[Eric Wieser]

We have docs#powers_hom

[Kevin Buzzard]

Much of mathematics (and this was very surprising to me) is very good at sticking to the principle that the natural maps which show up in the theory don't just commute with random monoid structures, they commute with monoid structures which have the same notation for the monoid law. There are ->+ and ->* everywhere. pow n _ and exp are rare exceptions where the notation changes, and log is the canonical example the other way. Note that things called exp and log appear in several different branches of geometry, with exp often being used to map a linear structure (eg a tangent space) to a nonlinear structure like a Lie group (where addition may not even be defined). However there are sufficiently few of these things in mathlib right now for us not to have had any need to come up with a bundled typeclass for (and notation for!) the predicate on functions f such that f(a+b)=f(a)*f(b) or f(ab)=f(a)+f(b). I thought that we were going to have to make one when doing valuation theory because the p-adic valuation on the integers satisfies v(ab)=v(a)+v(b) but there's a strange thing about that function -- it really wants to take the value +infinity at 0 and this is inconvenient in type theory. We dealt with it by only using multiplicative valuations N taking values in a monoid with zero, and now N(ab)=N(a)N(b) and N(0)=0 and it looks much more like the kind of function that mathlib likes.

[Yury G. Kudryashov]

We have two ways to express things like this: M →+ additive Nand multiplicative M →* N.

[Apurva Nakade]

I see, so if I understand correctly multiplicative nat is simply the monoid structure * over nat defined as a * b = a + b. Thanks!

[Apurva Nakade]

Eric Wieser said:

We have docs#powers_hom

Is it worth adding a lemma saying that pow (n : M) : multiplicative nat \to (powers n) is a monoid_hom or is it better to just unravel docs#powers_hom and use some subtype lemmas whenever the above monoid_hom structure is needed?

[Eric Wieser]

defined as a * b = a + b. Thanks

It's less confusing to think of it as of_add a * of_add b = of_add (a + b) (docs#of_add_add)

[Eric Wieser]

Don't you mean is a mul_equiv?

[Eric Wieser]

I think that's just docs#monoid_hom.mrange_restrict. Although there might be some complications if docs#powers isn't defeq to powers_hom.range