Additive characters

Stream: maths

[Michael Stoll]

I'm preparing a PR introducing additive characters.

[Michael Stoll]

#15499

[Michael Stoll]

@Riccardo Brasca @Johan Commelin @Kevin Buzzard Maybe you'd like to have a look at #15499.

[Michael Stoll]

@Kevin Buzzard I left some questions related to your comments at #15499.

[Michael Stoll]

Kevin Buzzard said in a comment on #15499:

For me this PR raises an interesting question. My impression is that the community are not keen on adding the structure of maps f:A -> G such that f(a+b)=f(a)*f(b), because then we have to make an API for it, and how it composes with additive maps on one side and multiplicative maps on the other side, and then there are maps G -> A and etc etc. Another proposal is to define add_char so that it contains an application of of_add : R -> multiplicative R and then just write add_char.map_add : \psi (a + b) = \psi a * \psi b and a bit more API for it.

My position on this has come from a huge struggle I had in the past using with_top because it would often leak to option, and if you were working with with_top and with_bot then you didn't know whether none was bot or top. Being principled with types in statements of results goes a long way towards stopping this kind of leakage.

To add to Kevin 's comment above, I find it quite painful to have to use multiplicative R →* R' instead of something like, say, R +→* R' and having to convert between R and multiplicative R via of_add and to_add. (And as one can see from Kevin's comments on the PR, I didn't manage to do it completely right...). If homomorphisms between additive and multiplicative structures also occur in some other places, it may be worth the effort of having dedicated type classes and API for them. Maybe there is a way of auto-generate them, something like a "left" or "right" version of to_additive?

[Yakov Pechersky]

We've done a lot of work recently to plug the holes of the with_top and with_bot implementation to prevent the leaking of some and none, without having to resort to irreducible.

[Yakov Pechersky]

Part of the leakage often occurs with "cute" proofs that (ab)use the fact that the underlying type is the same. What we need better are useful recursors

[Yakov Pechersky]

Like we know have with docs#with_top.rec_top_coe for example

[David Ang]

Michael Stoll said:

Kevin Buzzard said in a comment on #15499:

For me this PR raises an interesting question. My impression is that the community are not keen on adding the structure of maps f:A -> G such that f(a+b)=f(a)*f(b), because then we have to make an API for it, and how it composes with additive maps on one side and multiplicative maps on the other side, and then there are maps G -> A and etc etc. Another proposal is to define add_char so that it contains an application of of_add : R -> multiplicative R and then just write add_char.map_add : \psi (a + b) = \psi a * \psi b and a bit more API for it.

My position on this has come from a huge struggle I had in the past using with_top because it would often leak to option, and if you were working with with_top and with_bot then you didn't know whether none was bot or top. Being principled with types in statements of results goes a long way towards stopping this kind of leakage.

To add to Kevin 's comment above, I find it quite painful to have to use multiplicative R →* R' instead of something like, say, R +→* R' and having to convert between R and multiplicative R via of_add and to_add. (And as one can see from Kevin's comments on the PR, I didn't manage to do it completely right...). If homomorphisms between additive and multiplicative structures also occur in some other places, it may be worth the effort of having dedicated type classes and API for them. Maybe there is a way of auto-generate them, something like a "left" or "right" version of to_additive?

I am all for having some kind of +→*. From my experience this occurs in quite a few places I care about: additive valuations, Kummer theory, complete 2-descent, Galois cohomology, etc. It was incredibly annoying for me as well, especially when trying to do a quotient_group.map of homomorphisms from + to * to define things like Selmer groups.

[David Ang]

There is a discussion of this in the "map from mult gp to add gp" topic in the general stream.

[Michael Stoll]

David Ang said:

There is a discussion of this in the "map from mult gp to add gp" topic in the general stream.

Here is a link to the other topic.

[Michael Stoll]

@riccardo lasagno @Johan Commelin The discussion in the other topic notwithstanding, I would like to get the additive characters stuff (#15499) into mathlib. @Kevin Buzzard has looked through it and I think he is OK with it (after the changes I made that he had suggested). When homomorphisms from additive monoids to (multiplicative) monoids are availble, I'll happily adapt the code; it should then be less cumbersome and easier to read and understand. But short-term, I'd like to be able to define Gauss sums (albeit in an ugly way) and prove stuff about them (this would likely be my next PR).

[Johan Commelin]

@Michael Stoll I'm interested in knowing whether you would still prefer to have +->*.

[Johan Commelin]

Because your add_char is exactly that.

[Johan Commelin]

If you define it for add_monoid and monoid instead of for two rings, then you have your definition.

[Michael Stoll]

Yes, of course. But what I then do in the file is mostly geared towards the intended use with Gauss sums.

[Michael Stoll]

I.e., I wouldn't want to (have to) provide the complete API for general homomorphisms from additive monoids to monoids. But when this eventually exists somewhere, I would very much like to use it. However, my impression is that this may take some time, so I'd prefer to proceed for now with what is there (i.e., multiplicative R and friends).

[Johan Commelin]

Ok. I still think that it is good to make the definition with the weakest assumptions possible, even if you then restrict to comm_rings directly afterwards.

[Michael Stoll]

I've changed the definition so that the domain only needs to be an add_monoid and the target, a monoid. I've also removed the definition of trivial and replaced the occurrences by (1 : add_char R R'). And I changed the lemma names as suggested.

[Michael Stoll]

@Johan Commelin If you have time, could you push it to the merge queue? (Unless there is something else that should be changed.)

[Yaël Dillies]

@Michael Stoll, we're using add_char for LeanAPAP and we need to talk about the double dual embedding (eg here).

[Yaël Dillies]

Currently, our definition of the double dual embedding is

def double_dual_emb : add_char G (add_char (additive $ add_char G R) R) := monoid_hom.eval

and we're pretty annoyed about the fact that we need this additive because the operation on add_char is multiplication.

[Yaël Dillies]

In fact, this is a general problem in our project, because we're doing additive combinatorics, not multiplicative combinatorics, and the fact that add_char is a multiplicative group forces us to go through weird hoops to use our definitions.

[Yaël Dillies]

What do you think of changing the operation from * to +?

[Michael Stoll]

I'm against that, since in all number theoretic applications, additive characters are homomorphisms from an additive to a multiplicative group. In particular, everywhere in the (NT) literature, additive characters on a given domain are considered as a multiplicative group.

How bad is it to set up an API that does the translation into a form that is suitable for you?

I had to fight fairly hard to find a way to set it up so that it is not too painful to use in the context we need in number theory (i.e., so that one does not have to do the additive/multiplicative conversion by hand every time)...

[Yaël Dillies]

Michael Stoll said:

in all number theoretic applications, additive characters are homomorphisms from an additive to a multiplicative group. In particular, everywhere in the (NT) literature, additive characters on a given domain are considered as a multiplicative group.

How does the second sentence follow from the first? There's several design decisions at play here: the operation on the domain, the operation on the codomain, and the operation on the characters.

[Yaël Dillies]

Michael Stoll said:

I had to fight fairly hard to find a way to set it up so that it is not too painful to use in the context we need in number theory (i.e., so that one does not have to do the additive/multiplicative conversion by hand every time)...

Doing additive combinatorics, I'm currently at this stage of converting everywhere...

[Johan Commelin]

@Yaël Dillies would it work for LeanAPAP to use add_monoid_hom and convert the codomain R into an additive gadget with additive?

[Yaël Dillies]

No, because we're talking about complex-valued characters and we need to add the values.

[Michael Stoll]

Yaël Dillies said:

Michael Stoll said:

in all number theoretic applications, additive characters are homomorphisms from an additive to a multiplicative group. In particular, everywhere in the (NT) literature, additive characters on a given domain are considered as a multiplicative group.

How does the second sentence follow from the first? There's several design decisions at play here: the operation on the domain, the operation on the codomain, and the operation on the characters.

Well, usually the group structure on maps is defined via the group structure on the target, which is multiplicative here.

[Yaël Dillies]

That I understand, but the fact that characters are maps is an implementation issue, at least in additive combinatorics.

[Yaël Dillies]

What's important is that characters act on the original group.

[Johan Commelin]

Do they, in mathlib?

[Michael Stoll]

In the number theory context, an additive character is a group homomorphism from the additive group of a (finite) field or ring into the multiplicative group of a field (or maybe ring). add_char is basically a wrapper around homomorphisms plus switching additive and multiplicative structures. The latter was the main point of the exercise; otherwise something like add_group_hom would just do.

[Michael Stoll]

What do you mean by "acting" on the original (= source?) group?

[Yaël Dillies]

Michael, your message explains why add_char G R is defined as multiplicative G →* R (or G →+ additive R), but it doesn't explain why the group operation on add_char G R is multiplication.

[Eric Wieser]

Can you link to the operation you mean, @Yaël Dillies?

[Yaël Dillies]

I'm talking about comm_monoid (add_char G R) from docs3#add_char.comm_monoid. I'm arguing for turning that into add_comm_monoid (add_char G R).

[Yaël Dillies]

So far, the only argument that Michael has advanced for the current instance is that it means we have (ψ * χ) x = ψ x * χ x. WIth my instance, it would be (ψ + χ) x = ψ x * χ x. To me, that's a much better option than all the pain I'm currently going through.

[Yaël Dillies]

In fact, we could have both instances simultaneously and I would be happy with that even if that's possibly not very elegant.

[Michael Stoll]

I'm fine with having both instances.
(I find (ψ * χ) x = ψ x * χ x much more natural than (ψ + χ) x = ψ x * χ x, but my main point is that this is what people in number theory are used to; I think mathlib should try to be as close notation-wise as possible to what mathematicians actually use.)

[Eric Wieser]

With no other context, the (ψ * χ) x = ψ x * χ x we currently have seems much more natural (and consistent with the rest of mathlib) to me.

[Yaël Dillies]

Eric, try defining the double dual embedding and come back to me :wink:

[Yaël Dillies]

And we can play this game the other way around, actually. Currently we have ψ⁻¹ x = ψ (-x). With my instance, this becomes (-ψ) x = ψ (-x).

[Michael Stoll]

Did you mean ψ⁻¹ x = (ψ x)⁻¹? :smile:

[Eric Wieser]

Mathlib is pretty consistent that operations on fun_like objects commute with coercion. What you're proposing @Yaël Dillies would violate that, and AFAIK is the only such case

[Yaël Dillies]

I agree it's pretty rare but I don't believe it would be the only such case. At any rate, I'm happy to break this rule (is it any important?) if it means I can use add_char (add_char G complex) complex for the double dual instead of additive (add_char (additive $ add_char G complex) complex).

[Eric Wieser]

Is additive (add_char (additive $ add_char G complex) complex) the same as
additive (add_char G complex →* complex)?

[Yaël Dillies]

@Eric Wieser, indeed there's at least another case where function coercion doesn't commute with an algebraic operation on a fun_like type: multiplication on monoid.End is given by composition, namely (f * g) a = f (g a)`.

[Yaël Dillies]

Eric Wieser said:

Is additive (add_char (additive $ add_char G complex) complex) the same as
additive (add_char G complex →* complex)?

Yes it is, but if the codomain of your double dual embedding is this, then double_dual_emb is not an add_char! You would need to peel off the additive and also turn the inner ->* into an add_char every time you want to use it as a character.

[Yaël Dillies]

I have just tried endowing add_char with an add_comm_monoid/add_comm_group instance in LeanAPAP, and everything became suddenly much easier. No more mentions of additive, less mentions of multiplicative, and I don't have to keep both an additive and multiplicative version of the definitions that are internal to the proof anymore.