Gauss sums

Stream: maths

[Michael Stoll]

I am now adding Gauss sums: #15684
@Kevin Buzzard @Riccardo Brasca @Johan Commelin
The next step will be to use these results to prove a (generalized version of) Quadratic Reciprocity for quadratic characters of finite fields and for the Legendre Symbol.

[Michael Stoll]

Based on @Johan Commelin 's suggestion, I have added a comm_group instance for add_char R R' (when R is a add-comm_group and R' is a comm_monoid -- perhaps this should be in mathlib more generally: G \to* M is a commutative group when G is one and M is a commutative monoid, since you can do the inversion on the domain side), which allows to write ψ⁻¹ instead of mul_shift ψ (- 1) in one of the main results on Gauss sums.

[Yaël Dillies]

Are you talking about docs#monoid_hom.comm_group ?

[Michael Stoll]

No. In the situtation I'm talking about, the domain is a (commutative) group, but the target is only a (commutative) monoid.

[Michael Stoll]

So you can define the inverse of f : G → M as λ x, f x⁻¹. But I guess that supplying an instance for this could lead to a problematic diamond when the target is a group, since we then get two different definitions of the inverse that are likely not defeq.

[Yaël Dillies]

Yes unfortunately that would be relying on f x⁻¹ = (f x)⁻¹ being defeq, which it is not.

[Michael Stoll]

@Eric Wieser See above.

[Eric Wieser]

Apologies for repeating a variant of this discussion in the PR. I think the easy way out here is to make add_char semireducible (ie not reducible as the abbreviation keyword makes it), so that we can choose to have this new instance without the old one at all

[Michael Stoll]

I assume this would then require to sort of copy over the comm_monoid instance? Or does apply_instance find it also when add_char is semireducible?

[Eric Wieser]

You would indeed have to copy things across

[Michael Stoll]

I'll give it a try. I'll ask here if I run into problems.

[Eric Wieser]

Something like

instance : monoid (add_char R R') := monoid_hom.monoid

Should work

[Michael Stoll]

(I have made some changes to algebra.big_operators.fin (suggested by Johan), and now I'm building mathlib to see if anything breaks. This is going to take a while; before continuing, I'll wait until it's done.)

[Junyan Xu]

Can't you do @[derive [comm_monoid, ...]] def add_char : ...?

[Michael Stoll]

No, since at this point, R is just an add_monoid and R' is a monoid. To get a monoid structure on the homomorphisms, the target needs to be commutative.

[Michael Stoll]

The first problem I have is that Lean doesn't know how to interpret an add_char as a function. What do I need to put in @[derive [???]] def add_char ... to get the correct instance for this? (I tried has_coe_to_fun and fun_like, but this doesn't seem to work.)

[Michael Stoll]

I now have the following.

@[derive [comm_monoid, inhabited]] def add_char : Type (max u v) := (multiplicative R) →* R'

instance : has_coe_to_fun (add_char R R') (λ x, (multiplicative R → R')) :=
begin
  dsimp only [add_char],
  apply_instance,
end

instance add_char.monoid_hom_class : monoid_hom_class (add_char R R') (multiplicative R) R' :=
begin
  dsimp only [add_char],
  apply_instance,
end

which seems to be working. But I wonder whether this could be done more elegantly...

[Johan Commelin]

@Michael Stoll If with "elegantly" you mean "shorter", you can write show_term { apply_instance } which will tell you how to turn the proofs into 1-line term-mode constructions.

[Michael Stoll]

I was more thinking of including the latter two in the @[derive ...] thing.

[Johan Commelin]

But as you said, those instances aren't true in the full generality, right?

[Johan Commelin]

I'm a bit surprised that you are deriving comm_monoid...

[Michael Stoll]

I have changed the target requirement from monoid to comm_monoid :smile:

[Michael Stoll]

(I doubt that the added generality (with [monoid R']) would be that useful...)

[Junyan Xu]

It seems derive currently doesn't work with classes with non-class arguments, like M and N in docs#monoid_hom_class. Theoretically there could be multiple monoid_hom_class instances on the same type with different M and N.

[Michael Stoll]

I have replaced the proofs of the two instances by one-liners (following @Johan Commelin 's suggestion). I hope the new state of affairs is sufficiently satisfactory now. (Building mathlib will take a while, since a lot depends on algebra.big_operators.fin.)

[Kevin Buzzard]

One example where things aren't commutative is exponentiation from a lie algebra to a lie group eg matrix exponentiation

[Michael Stoll]

Kevin Buzzard said:

One example where things aren't commutative is exponentiation from a lie algebra to a lie group eg matrix exponentiation

I think it is better to wait for add_monoid_to_monoid_hom for this.
add_char is really meant for characters on additive groups (of rings) with values in commutative rings.
Once add_monoid_to_monoid_hom is available, there is no need whatsoever to use add_char outside the setting it is intended for.

[Junyan Xu]

One example where things aren't commutative is exponentiation from a lie algebra to a lie group eg matrix exponentiation

Hmm that sends zsmul to zpow but definitely isn't a homomorphism in the noncommutative case; we have the Baker–Campbell–Hausdorff formula. It sends add to mul if the bracket of the two elements is zero, though.

[Kevin Buzzard]

Aah yes of course! So this exponentiation doesn't fit into the picture at all.

[Michael Stoll]

It does when the Lie group is the group of points of an abelian variety over some local field. (Which is something that comes up in the context of Chabauty's method...)

[Michael Stoll]

(But in this case, you write the group usually additively, so it's perhaps a moot point in the context of this discussion.)

[Kevin Buzzard]

Michael I have been confused for years now about when mathematicians are interested in maps which change * to +. For elliptic curves we've used + as the group law. When Huber sets up valuation theory to do adic spaces he uses multiplicative monoids as a target rather than additive ones, so his valuations send * to *. Another interesting example is Hilbert 90; group cohomology group law will be + so there's something funny going on with $H^1(Gal(L/K),L^\times)=0$; however this generalises to $H^1(Gal(L/K),GL_n(L))={1}$ as a pointed set and I'm now wondering whether Hilbert 90 should be reinterpreted as claiming that a pointed set is trivial :-/ I had this exp and log map between Lie algebras and Lie groups in my mind as something else I didn't understand for a while but it's only today that Junyan has pointed out that I was wrong about this. I think tropicalisation of rings is another place where this comes up, but this is something I know next to nothing about.

[Michael Stoll]

I'm not sure I can think if many examples of homomorphisms between additively and multiplicatively written monoids in a non-commutative setting. After all, there is the convention that additive notation should only be used when the operation is commutative. So in most cases, the multiplicative monoid that shows up will be commutative, too.

[Michael Stoll]

@Johan Commelin @Eric Wieser @Junyan Xu I would think that #15684 should be fine now.

[Michael Stoll]

@Junyan Xu suggested to make the private lemmas gauss_sum_mul_aux₁ and gauss_sum_mul_aux₂ public.
My feeling was that at least gauss_sum_mul_aux₁ is maybe too specfic to be useful outside the proof of gauss_sum_mul_gauss_sum_eq_card. The other one, gauss_sum_mul_aux₂, could be more useful. If it is made public, it should probably go into add_character.lean (and get a more descriptive name like add_char.sum_mul) , since it only involves an additive character.
Opinions? @Johan Commelin @Eric Wieser @Kevin Buzzard @Riccardo Brasca

[Riccardo Brasca]

I am still on holiday, I will have a look before next weekend :sweat_smile:

[Alex J. Best]

I'm generally of the opinion that private lemmas don't really serve a useful purpose. Iirc: They aren't lookable up in the docs (for someone reading the proof) and they make it so that someone who copy pastes your proof to a new file will immediately have a broken proof. If we want to guide users to the most interesting results in a file we should do it with big docstrings and a list of the main results in the file header. So even if a lemma is only useful in a specific situation we can just give it a name that won't cause clashes and leave it public

[Violeta Hernández]

Disagree. Sometimes private lemmas are completely subsumed by the result they're used in. Sometimes they break established API conventions as a necessary evil. Sometimes they're so specific and unrelated to the rest of the file that it serves no purpose making it public, and it would only make the docs more confusing.

[Violeta Hernández]

That said, if you're even considering that a private lemma might be useful, that's an indication that it shouldn't have been made private to begin with.

[Violeta Hernández]

I find that programmers will always find a way to have private functions even in languages where there's no such functionality. Think of all the wasted underscores in languages like Python or C. Let's not give them the chance to do this in Lean.

[Michael Stoll]

I have made what used to be gauss_sum_mul_aux₂ public and moved it to add_character.lean as add_char.sum_mul_shift.
I have left the other lemma (now gauss_sum_mul_aux) private for now, but I'd be interested in more input on this.

[Michael Stoll]

@Junyan Xu has shortened some of the proofs quite a bit and made the code quite a bit more efficient.
So I hope the PR can be merged now.

[Michael Stoll]

If there is nothing more to be done, then perhaps sombody can push #15684 onto the merge queue? @Johan Commelin

[Michael Stoll]

#15888 provides the next step on the way of proving QR using Gauss sums. It adds results to number_theory.legendre_symbol.quadratic_char that give the values of a quadratic character at 2, -2 and odd primes.
(The next and last step will be to use these for the Legendre symbol.)

[Michael Stoll]

I'll be on a long trip home from Park City, but it would be nice if people could have a look while I'm offline.
@Johan Commelin @Kevin Buzzard @Junyan Xu

[Michael Stoll]

@Johan Commelin Most of the names in number_theory/legendre_symbol/quadratic_char.lean begin with quadratic_char_. Should they go into the root namespace, rater than char.?

[Johan Commelin]

As a rule of thumb, I think the fully-qualified name should try not to repeat itself.

[Michael Stoll]

OK, then I'll move the quadratic_char_ names to the root namespace and the is_square_neg_one and similar ones to the finite_field namespace.

[Michael Stoll]

Can #15888 go on the merge queue now? @Johan Commelin @Riccardo Brasca

[Michael Stoll]

@Johan Commelin Thanks!