Quadratic Hilbert symbol over ℚ

Stream: maths

[Michael Stoll]

As already mentioned in a different thread, I have written code that defines the (quadratic) Hilbert symbol for rational numbers and proves (among other properties) the product formula.
There appears to be interest to include this into mathlib, so I'll try to break this up (it is several thousand lines of code) into a number of reasonably-sized PRs, which I'm going to discuss here first.

[Michael Stoll]

The overall plan is roughly as follows.

• Define a type for places of ℚ

• Define the symbol on integers and separately for

  • the place at infinity
  • the place 2
  • the odd places
    by an explicit formula

• Prove properties (symmetry, multiplicativity, ...) in each case separately

• Then conclude that these properties are valid in general (over the integers)
• Prove the product formula (over the integers) by multiplicativity using quadratic reciprocity
• Define the symbol over ℚ via the integral version and prove the relevant things over ℚ

[Kevin Buzzard]

Do you think it's worth defining a type of places for a general number field and then proving that the places of \Q are what we know they are? Other than that, this looks like a fine plan

[Michael Stoll]

In particular, I am relying on Quadratic Reciprocity (and the auxiliary laws), so I need to use properties of the Legendre symbol. The relevant file, number_theory.quadratic_reciprocity, unfortunately does not have a lot of API lemmas, and some of those that are there are only for natural numbers a (in the symbol (a/p)), whereas the symbol is defined for integers a. This is a bit painful, since there is no obvious reduction to natural numbers.
So I propose to change the lemmas that are there to deal with integers a (using search in VScode, I checked that they arenot used outside the file) and add some new ones that I find useful. Does that sound like a good first step?

[Michael Stoll]

Kevin Buzzard said:

Do you think it's worth defining a type of places for a general number field and then proving that the places of \Q are what we know they are? Other than that, this looks like a fine plan

I want to define def hilbert_sym (v : plcℚ) (a b : ℚ) : ℤ := ..., where plcℚ is the type for places of ℚ, and then be able to do case distinctions according to the nature of the place (so that I can invoke the explicit definitions). For this purpose, my simple-minded definition

@[derive decidable_eq]
inductive plcℚ : Type
| infty : plcℚ -- the place at infinity
| finpl (p : ℕ) (hp : fact p.prime) : plcℚ -- finite places correspond to prime numbers

works fine. (One question here is whether hp should better be a type class instance argument.)

[Michael Stoll]

For my purposes right now, places of general number fields seem to be overkill.

[Michael Stoll]

But it would make sense to eventually have suitable glue.

[Adam Topaz]

I seem to recall Ostrowski's theorem being formalized somewhere...

[Adam Topaz]

https://github.com/RaitoBezarius/berkovich-spaces is the relevant repo, but it seems that this never made it into mathlib

[Junyan Xu]

(deleted)

[Alex J. Best]

At one point I tried to generalize the Legendre symbol file to integers completely

[Michael Stoll]

So what happened to that attempt?

[Alex J. Best]

But I remember it being a bit subtle / annoying to convert some of the proofs there. A lot of it should be doable though, but it's not clear to me if it's easiest to generalize the proofs or to just add the integer versions using the natural ones and dealing with negation appropriately

[Alex J. Best]

I will try to find it tomorrow. It may be on GitHub or on my computer or deleted unfortunately

[Michael Stoll]

OK; I hadn't yet looked at the proofs in that file in detail. I was assuming that it should in fact be more natural to work with integers. I'll wait to see if you find something.

[Johan Commelin]

Shouldn't we generalize to the Jacobi symbol, or something like that?

[Junyan Xu]

Another direction of generalization would be Hilbert symbol -> Steinberg symbol :) A lot of basic algebraic K-theory seems low-hanging ...

[Adam Topaz]

Yeah it would take about 5 minutes to define Milnor K theory. I actually have some (other) applications for this in mind. Maybe we should just do it! Proving that the tame symbol and norm maps are well defined should be a fun project.

[Kevin Buzzard]

You should just do it. We have things like definition of flat and projective modules with very little API because we're not quite ready for the API (need more homological algebra) but it was clear what the definition should be

[Michael Stoll]

I'm not sure whether I should open a new topic on this, but it is related to my attempt at refactoring the Legendre symbol code.

The present file number_theory/quadratic_reciprocity uses [fact (p % 2 = 1)] in a number of places. Doing grep with fact (.* % 2 = 1) over all of mathlib shows that it is used exactly twice elsewhere: docs#zmod.le_div_two_iff_lt_neg and docs#zmod.ne_neg_self. Of these two, the first apears to be used nowhere, and the second is used only in quadratic_reciprocity.

My question is, is it at all useful to have statements depending on [fact (n % 2 = 1)]? Or would it be better to just add explicit hypotheses? In the Legendre symbol code, I would prefer to have an explicit hypothesis p ≠ 2 instead. Opinions?

[Michael Stoll]

(#find fact (_ % 2) = 1 times out, BTW...)

[Kevin Buzzard]

If you need it everywhere then another possibility is just to add it as a hypothesis and then include it. The fact solution for adding a fact everywhere is not a great one.

[Michael Stoll]

I have no problem with adding explicit hypotheses where I need them.

[Michael Stoll]

Of course, most statements about the Legendre symbol need that p is an odd prime, but for some, it is not necessary (the way it is defined).

[Michael Stoll]

Another question: is there a naming convention for statements that say that something is a multiplicative function? Concretely, I have

theorem legendre_sym_mult (a b : ℤ) : legendre_sym (a*b) p = legendre_sym a p * legendre_sym b p := ...

(add (p : nat) [fact p.prime]) but I am not sure about the name...

[Johan Commelin]

Mathlib's definition of the Legendre symbol is wrong for p = 2, isn't it?

[Johan Commelin]

@Michael Stoll The name would be legendre_sym_mul, or possibly mul_left if you think it's ambiguous.

[Michael Stoll]

Johan Commelin said:

Mathlib's definition of the Legendre symbol is wrong for p = 2, isn't it?

The Legendre symbol is only defined when the second argument is an odd prime, so there is no "wrong" definition...

[Michael Stoll]

Johan Commelin said:

Michael Stoll The name would be legendre_sym_mul, or possibly mul_left if you think it's ambiguous.

I'll change the name to legendre_sym_mul then, since there is no mul_right. (That would be different for the Jacobi symbol.)

[Johan Commelin]

Michael Stoll said:

The Legendre symbol is only defined when the second argument is an odd prime, so there is no "wrong" definition...

Aah, ok. But the Legendre symbol for p = 2 is also not computing what's needed for quadratic reciprocity with p = 2. I think that's what I remembered, at least.

[Michael Stoll]

Unless somebody objects, I will also replace the [fact (p % 2 = 1)] arguments with p ≠ 2s.

[Michael Stoll]

Johan Commelin said:

Michael Stoll said:

The Legendre symbol is only defined when the second argument is an odd prime, so there is no "wrong" definition...

Aah, ok. But the Legendre symbol for p = 2 is also not computing what's needed for quadratic reciprocity with p = 2. I think that's what I remembered, at least.

One could try to define (a / 2) so that QR works. But then the problem is that 2 is neither 1 nor 3 mod 4, so it is not clear what the "correct" version of QR would be.

[Johan Commelin]

I agree that using p ≠ 2 assumptions makes more sense than [fact (p % 2 = 1)]. I think the QR file is pretty old. We didn't haven an even/odd API back then either.

[Michael Stoll]

The copyright notice says 2018. I have no idea what "pretty old" means for mathlib :smile:

[Johan Commelin]

If you define legendre a p = if (a : zmod p) = 0 then 0 else if is_square (a : zmod p) then 1 else -1, then you get something different from what we have now, for p = 2, right?

[Michael Stoll]

No: when p = 2, we have a ^ (p /2) = a = 1 (in zmod 2) when a is not zero mod 2.

[Johan Commelin]

Aahrg, I'm being terribly confused.

[Damiano Testa]

I would be inclined to make the definition at 2 work out to be true for as many theorems as possible, so that the assumption p ≠ 2 only bugs you as little as possible.

[Johan Commelin]

Maybe I shouldn't try to recall some issue I had when I was working with this file more than a year ago...

[Michael Stoll]

example (a : ℤ) (ha : (a : zmod 2) ≠ 0) : legendre_sym a 2 = 1 :=
begin
  simp [legendre_sym, ha],
  have h : ∀ b : zmod 2, b = 0 ∨ b = 1 := by dec_trivial,
  have hh := h ↑a,
  tauto,
end

(The proof can certainly be simplified.)

[Damiano Testa]

"Everyone" knows that two is odd and that Legendre symbols shouldn't make sense at 2. That's a little like dividing by zero, in my understanding.

[Michael Stoll]

I think it is the usual approach to prefer total functions with "garbage" values at arguments where they should not be defined.

[Junyan Xu]

Michael Stoll said:

theorem legendre_sym_mult (a b : ℤ) : legendre_sym (a*b) p = legendre_sym a p * legendre_sym b p := ...

It's map_mul if you make λ x, legendre_sym x p a monoid_hom.

[Johan Commelin]

But to do that you have to swap the order of the arguments...

[Michael Stoll]

Johan Commelin said:

But to do that you have to swap the order of the arguments...

I was debating with my self whether I should suggest swapping the arguments anyway.

[Michael Stoll]

Should I set up a poll on this? How would I do that?

[Damiano Testa]

Would it make sense to make the Legendre symbol take value in sign_type?

[Johan Commelin]

/poll some title
- some option
- another option

Make sure you don't have other text in the same post.

[Michael Stoll]

Is sign_type a multiplicative monoid?

[Damiano Testa]

Yes, it is, but I'm not sure it is already in mathlib: let me check

[Damiano Testa]

docs#sign_type

[Michael Stoll]

/poll Order of arguments in legendre_sym: should (a / p) be

• legendre_sym a p (this is what it is currently)
• legendre_sym p a (would make legendre_sym p a multiplicative function)

[Michael Stoll]

Damiano Testa said:

docs#sign_type

The link gives me a 404 error.

[Damiano Testa]

Not yet: #12835

[Michael Stoll]

How do I get from h : (a : zmod p) ≠ 0 and hp : p = 2 to (a : zmod 2) ≠ 0?

[Michael Stoll]

simp_rw [hp] at h does not seem to work...

[Damiano Testa]

Does subst hp work?

[Michael Stoll]

failed to revert '_inst_1', it is a frozen local instance (possible solution: use tactic `unfreezing` to temporarily reset the set of local instances)

(there is [fact p.prime] somewhere...)

[Johan Commelin]

unfreezing { subst hp }

[Michael Stoll]

unfreezing is unknown, but unfreezingI exists and seems to work.

[Damiano Testa]

Is it unfreezing or unfreezingI? Is there a difference?

[Johan Commelin]

Ooh, so that error message contains a typo.

[Damiano Testa]

This sentence contais three erors.

[Michael Stoll]

Junyan Xu said:

It's map_mul if you make λ x, legendre_sym x p a monoid_hom.

This now looks like this:

def legendre_sym_mul' : ℤ →* ℤ :=
{ to_fun := legendre_sym p, map_one' := legendre_sym_one p, map_mul' := legendre_sym_mul p }

(after swapping the arguments of legendre_sym).

[Michael Stoll]

While working on Legendre symbols, I find myself changing the file number_theory/quadratic_reciprocity quite thoroughly; it is also growing longer. What would be the recommended way of proceeding so that the PRs are manageable?

[Kevin Buzzard]

If you make a new def or change a def then don't do much else, try to PR the def and some basic stuff because people might complain about the definition and then everything breaks when you change it. If you're refactoring theorems you can probably get away with bigger PRs.

[Michael Stoll]

Hmmm... I guess this means that I start fresh with a new branch and move my changes over incrementally?

[Michael Stoll]

I have now started by swapping the arguments to legendre_symbased on the result of the poll above: #13311

[Kevin Buzzard]

Thanks a lot for taking this on. As you know I'm a number theorist but I seem to spend much of my lean research time doing other stuff (eg this Scholze project). My post-doc Maria has defined Adeles and ideles and we hope to start our journey towards things related to class field theory later

[Michael Stoll]

I have looked at the RPs labeled "ready-to-merge" and see that "my" PR #13311 is blocked because of a "merge conflict" (the same seems to be true for most of the other ones currently in the queue). Is this normal? Is there something I should do? In any case, when I click on "Details" next to "bors — Merge conflict", I only see "Permission denied", so it seems I have no way of figuring our what the problem might be.

[Johan Commelin]

I think you don't have to do anything. The merge conflict happened with another PR. Bors should give more precise error messages :expressionless:

[Michael Stoll]

How long will it take until this is resolved? (I'd like to get on with my list of changes...)

[Johan Commelin]

Can you see https://app.bors.tech/repositories/24316? Or do you get a "Permission denied" error?

[Johan Commelin]

As you can see, there are a lot of PRs trying to get into master right now.

[Johan Commelin]

Bors is trying to make sure that they all play well together, and get merged in batches.

[Johan Commelin]

But this might take a couple of hours to sort out :sad:

[Johan Commelin]

In principle, you can just create other PRs that depend on your current PR. git provides good support for that.

[Michael Stoll]

I can see the page under the link, thanks.

[Yaël Dillies]

Johan Commelin said:

But this might take a couple of hours to sort out :sad:

What an understatement :grinning: The queue has been going haywire for two days straight. docs#category_theory.groupoid_of_elements timing out is still causing most batch failures.

[Michael Stoll]

I'll have to learn git while doing this... Is there a nice and easy introduction available somewhere?

[Michael Stoll]

There is now the second PR: #13393.
This is just changing the type of a from ℕ to the more natural ℤ in a number of places, so that one can use the API lemmas for all allowed arguments of legendre_symbol.

[Michael Stoll]

Since I am going to add a substantial amount of code eventually, I would like to distribute the material over several files.
I assume the most reasonable way of doing this is to set up a new subdirectory legendre_symbol (say) in the number_theory directory and put the various files in there.
The first step (and next PR) would then be to create that subdirectory and move quadratic_reciprocity in there.
Are there any objections to that or suggestions to proceed differently?

[Johan Commelin]

Sounds good to me

[Michael Stoll]

#13441

[Johan Commelin]

@Michael Stoll It looks like you forgot to git add the new file

[Michael Stoll]

I had moved it outside VScode. It should be added now...

[Johan Commelin]

Thanks. I kicked it on the queue

[Michael Stoll]

#13449 splits off part of the code into a new file gauss_eisenstein_lemmas.lean. This is the part of the code I'm going to leave alone.

[Johan Commelin]

The linter is complaining that you should now write a module docstring for this file...

[Michael Stoll]

OK, will do.

[Michael Stoll]

Could somebody push this along? Johan seems to be taking a break...

[Michael Stoll]

@Damiano Testa How do I get a decidable instance for is_square a when a : F and F is a finite field?

[Yaël Dillies]

decidable_of_iff (∃ b, b * b = a) your_proof_here

[Michael Stoll]

And what do I write for your_proof_here?
Intuitively, every statement should be decidable in a finite field...

[Yaël Dillies]

Something like docs#is_square_iff_exists_sq

[Michael Stoll]

I found the following:

  haveI hdec : decidable (is_square a) :=
  by { change decidable (∃ b, a = b*b), exact set.decidable_set_of (λ (b : F), a = _) Exists, },

which seems to work.

[Yaël Dillies]

Don't!

[Yaël Dillies]

Oh wait, it's definitionally equal, then it's fine.

[Reid Barton]

This is fine, but you can also just write decidable_of_iff (∃ b, a = b * b) iff.rfl or something

[Michael Stoll]

This?

  haveI h := decidable_of_iff (∃ b, a = b * b) iff.rfl,
  unfreezingI { change decidable (is_square a) at h, },

[Reid Barton]

More simply, just declare h with the intended type from the start

[Michael Stoll]

OK, thanks; I tend to forget about this possibility...

[Alex J. Best]

import field_theory.finite.basic

instance {K : Type*} [fintype K] [monoid K] [decidable_eq K] : decidable_pred (is_square : K → Prop) :=
λ a, decidable_of_iff' _ (is_square_iff_exists_sq a)

is one answer to the question

[Michael Stoll]

This looks like it should go either into field_theory.finite.basic or into algebra.parity.

[Michael Stoll]

In any case, this looks like the best way of achieving what I want.

[Yaël Dillies]

Notice that this has nothing to do with fields.

[Michael Stoll]

#13474 removes arguments of the form [fact (p % 2 = 1)] and replaces them by (p ≠ 2) in quadratic_reciprocity.lean.

[Michael Stoll]

The next step will be to define the quadratic character on a finite field (and, by specialization, on zmod p) and prove the relevant properties in this setting. Then I will change the definition of legendre_sym to use this and simplify the proofs by making use of the API for the quadratic character.

[Michael Stoll]

Is the following name reasonable for mathlib?

lemma quadratic_char_dichotomy {a : F} (ha : a ≠ 0) :  quadratic_char F a = 1 ∨ quadratic_char F a = -1 := ...

or is the more unwieldy, but also more precise quadratic_char_eq_one_or_neg_one preferred?

[Johan Commelin]

I probably would have gone with the snd option. But I understand your dichotomy name perfectly fine.

[Michael Stoll]

Can you have a look at #13474 and, if it's OK, put it in the merge queue?

[Michael Stoll]

For the next PR, which will be a new file with new code, would it be OK to have ~300 lines of code in one go? Or should I split it up? Since it usually takes a day or so for one PR to be merged, the second option looks to me to be the less efficient one, but it may be more efficient in terms of the review.

[Johan Commelin]

300 lines of continuous diff is probably fine. A 300 line diff split over 5 files is probably a lot harder to review.

[Michael Stoll]

OK, thanks. I'll then go ahead with this once #13474 is done.

[Michael Stoll]

A general question: How do I rewrite terms under a sum? E.g.,

import field_theory.finite.basic
import algebra.big_operators.ring

open_locale big_operators

variables {F : Type*} [field F] [fintype F]

example : ∑ (a : F), a * (-1) = -∑ (a : F), a :=
begin
  rw [mul_comm], -- does not work
  sorry
end

(simp_rw does not work, either.) Do I have to use stuff like docs#fintype.sum_bijective or is there a simpler way?

[Ruben Van de Velde]

I think I'd try neg_sum and then sum_congr (untested)

[Michael Stoll]

I was trying to give a simple example. My use case is more involved. My question is, how can I manipulate the term under the sum? (A simple simp solves the goal in the example, so maybe it was not a good choice here.)

[Yaël Dillies]

You should use simp_rw

[Michael Stoll]

The term under the sum in my case is a product of four factors a * b * (c * d), which I want to rewrite to (a * c) * (b * d).

[Michael Stoll]

As mentioned above, simp_rw did not work.

[Yaël Dillies]

You can simp_rw mul_mul_mul_comm _ b

[Yaël Dillies]

The reason it did not work is that simp_rw rewrites as long as it finds an occurrence of the LHS of the lemma you're rewriting by, so in your case it was turning a * b * (c * d) into a * c * (b * d)into a * b * (c * d) into a * c * (b * d)... Givingexplicit arguments prevents it from looping.

[Michael Stoll]

The problem is that b is really some term involving the summation variable, so if I use that, I get an unknown identifier error.

[Damiano Testa]

When simp_rw does not work, conv can be helpful. It takes some time to learn how to navigate thee expressions, but eventually you should be able to reach what you want.

[Damiano Testa]

In particular, conv in (Type) { tactics } is usually helpful. Note that in Type you should use underscores for bound variables (or at least I think so).

[Michael Stoll]

Roughly something like ∑ (x : α × β), (f x.fst) * (g x.fst) * ((f' x.snd) * (g' x.snd)).

[Damiano Testa]

Besides rw, you move around with congr, funext, skip.

[Damiano Testa]

Does conv in (_ * _ * _) { rw mul_mul_mul_comm } work?

[Michael Stoll]

Yes, that looks reasonably good. Let's see how far I get with this.

[Damiano Testa]

You can chain more rw in the same conv.

[Michael Stoll]

How would I navigate within conv begin ... end to the term under the sum?

[Damiano Testa]

Maybe funext?

[Damiano Testa]

It always takes me quite a bit of guess-work.

[Damiano Testa]

I cycle using funext, congr, skip and some list formed of those commands works. When that fails, I use conv in (_).

Others can tell you more about using conv, I hope!

[Damiano Testa]

My mental picture is that congr will take apart stuff that looks like relations, funext gets you inside function applications and skip moves over to the next part`.

[Damiano Testa]

This mental picture is not always coherent/accurate, but is what I go by.

[Damiano Testa]

If you have a LHS and a RHS, I think that conv_lhs {...} gets you to the obvious starting point.

[Damiano Testa]

Honestly, conv and calc were some of the hardest tools to learn for me.

[Damiano Testa]

I'm still not too comfortable with conv and I try to put myself in a situation of not needing it. Ultimately, trying to rw bound variables is a major source of difficulty.

[Damiano Testa]

My impression is that for rw to work, they need to be in a not-so-bound state, hence the funext might allow for progress.

[Kevin Buzzard]

@Michael Stoll Just checking you know about https://leanprover-community.github.io/extras/conv.html

[Junyan Xu]

works in this case:

import data.fintype.card
open_locale big_operators
example {α} [fintype α] (f g f' g' : α → ℕ) : ∑ x : α × α, f x.1 * g x.1 * (f' x.2 * g' x.2) = 0 → true :=
begin
  rw fintype.sum_congr,
  swap 2, intro, rw [mul_mul_mul_comm, mul_assoc],
  /-∑ (a : α × α), f a.fst * (f' a.snd * (g a.fst * g' a.snd)) = 0 → true-/
  intro, trivial,
end

[Michael Stoll]

Kevin Buzzard said:

Michael Stoll Just checking you know about https://leanprover-community.github.io/extras/conv.html

I've had a look at it, yes.
But I think I'm going to organize my proof a bit differently...

[Michael Stoll]

New question:
When I add #lint at the end of the file that is supposed to be added in the next PR, I get some messages like

/- The `unused_arguments` linter reports: -/
/- UNUSED ARGUMENTS. -/
#check @char.finite_field.odd_card_of_char_not_two /- argument 4: [_inst_3 : decidable_eq F] -/

and

/- The `decidable_classical` linter reports: -/
/- USES OF `decidable` SHOULD BE REPLACED WITH `classical` IN THE PROOF. -/
#check @char.finite_field.odd_card_of_char_not_two /- The following `decidable` hypotheses should be replaced with
                      `classical` in the proof. argument 4: [_inst_3 : decidable_eq F] -/

I have a line

variables (F : Type*) [field F] [fintype F] [decidable_eq F]

near the beginning.

Should I do anything about these?
(I need [decidable_eq F] for a definition using ite, and anyway, any finite field will satisfy decidability, so the use/advantage of removing this assumption seems questionable to me.)

[Eric Rodriguez]

Put the decidable_eq on the definition, and skip it elsewhere. Mathematically, sure, but it makes things easier with typeclasses if you just skip proofs' decidability requirements and just use classical instead.

[Yaël Dillies]

Yes, you should follow what the linter says. This might be a bit annoying to add and remove decidable_eq F by sections, so instead you can call it [dec : decidable_eq F] and include dec/omit dec at will.

[Michael Stoll]

OK, thanks!

[Michael Stoll]

This is now #13503.
It adds a new file quadratic_char.lean in number_theory/legendre_symbol/, which defines the quadratic character on a finite field and proves a number of properties.
The next step will then be to change the definition of legendre_sym to use quadratic_char and to add API/simplify proofs based on quadratic_char.lean.

[Michael Stoll]

As suggested by @Johan Commelin, I'm trying to weaken the assumptions on the definition of quadratic_char. However, I'm running into problems with decidability instances:

import field_theory.finite.basic

instance {M : Type*} [fintype M] [monoid M] [decidable_eq M] : decidable_pred (is_square : M → Prop) :=
λ a, decidable_of_iff' _ (is_square_iff_exists_sq a)

def quadratic_char (α : Type*) [monoid_with_zero α] [decidable_eq α] [decidable_pred (is_square : α → Prop)] (a : α) : ℤ :=
if a = 0 then 0 else if is_square a then 1 else -1

variables {F : Type*} [fintype F] [field F] [decidable_eq F]

def qcF := quadratic_char F -- complains "failed to synthesize type class instance for decidable_pred is_square"

-- but the following works fine
def quadratic_char' (a : F) : ℤ :=
if a = 0 then 0 else if is_square a then 1 else -1

So why is Lean unable to infer the instance [decidable_pred (is_square : F → Prop)] when I try to specialize the more general definition to the case of a (finite) field F, whereas this does not seem to be a problem when I use the same definition in this more restricted setting? (And how can I work around it?)

[Eric Rodriguez]

this seems to be the relevant TC log:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 a : decidable
  (@is_square F
     (@distrib.to_has_mul F (@ring.to_distrib F (@division_ring.to_ring F (@field.to_division_ring F _inst_2))))
     a) := @asda (?x_3 a) (?x_4 a) (?x_5 a) (?x_6 a) (?x_7 a)
failed is_def_eq

I renamed the above instance to asda for ctrl+f purposes, and I made a goal to look-up the instance of decidable_pred (is_square : M \to Prop)

[Eric Rodriguez]

I don't know what a is here

[Michael Stoll]

In the original context, a is a term of type F.

[Michael Stoll]

In any case, the ?x_n a arguments look weird, but I don't have any experience so far in trouble-shooting these things...

[Eric Rodriguez]

this is the trace for the line def test : decidable_pred (is_square : F → Prop) := by apply_instance, so there's no a

[Michael Stoll]

a is a bound variable in the definition of the instance.

[Michael Stoll]

How do I get the trace?

[Eric Rodriguez]

set_option trace.class_instances true

[Michael Stoll]

For the second definition, the trace looks like this:

[class_instances] (0) ?x_0 : decidable
  (@is_square F
     (@distrib.to_has_mul F (@ring.to_distrib F (@division_ring.to_ring F (@field.to_division_ring F _inst_2))))
     a) := @is_square_decidable ?x_3 ?x_4 ?x_5 ?x_6 ?x_7

(I used the name is_square_decidable instead of asda.)

[Reid Barton]

I'm guessing it has to do with the fact that is_square only needs a has_mul instance but your decidability instance asks for monoid, and Lean chose some goofy path from field to has_mul that doesn't pass through monoid

[Michael Stoll]

monoid is needed for is_square_iff_exists_sq.

[Reid Barton]

True, but you can easily avoid doing that

[Eric Rodriguez]

import field_theory.finite.basic

instance {M : Type*} [fintype M] [has_mul M] [decidable_eq M] : decidable_pred (is_square : M → Prop) :=
λ a, fintype.decidable_exists_fintype

def quadratic_char (α : Type*) [monoid_with_zero α] [decidable_eq α] [decidable_pred (is_square : α → Prop)] (a : α) : ℤ :=
if a = 0 then 0 else if is_square a then 1 else -1

variables {F : Type*} [fintype F] [field F] [decidable_eq F]

def qcF := quadratic_char F

[Eric Rodriguez]

but not for just unfolding is_square:)

[Michael Stoll]

Reid Barton said:

I'm guessing it has to do with the fact that is_square only needs a has_mul instance but your decidability instance asks for monoid, and Lean chose some goofy path from field to has_mul that doesn't pass through monoid

It goes via field --> division_ring --> ring --> distrib --> has_mul.

[Johan Commelin]

Ahh, good old distribs strike back (-;

[Reid Barton]

Now what would be interesting is what to do about this if you really did need monoid to write the instance

[Yaël Dillies]

I doubt this can be the problem. Such things happen all the time.

[Reid Barton]

I am confused about this too, including why it apparently did work in the last part of the example.

[Reid Barton]

Does it have something to do with the higher-order-ness of decidable_pred?

[Reid Barton]

I guess normally what would happen is that the first argument ?x_3 of the instance gets filled in with F, then the others get synthesized by instance search and Lean notices that the two different paths are defeq

[Reid Barton]

I take it qcF does actually work after generalizing the decidable_pred instance?

[Michael Stoll]

Reid Barton said:

I take it qcF does actually work after generalizing the decidable_pred instance?

Yes, it does.

[Michael Stoll]

The second definition apparently went via ... --> ring --> monoid (which is what I would have expected as a mathematician).

[Michael Stoll]

Anyway, I have now made most of the changes @Johan Commelin suggested to #13503.

[Michael Stoll]

@Johan Commelin, can you look at #13503 again?

[Johan Commelin]

@Michael Stoll Thanks for the ping. I left some comments.

[Michael Stoll]

I made the changes you suggested. Thanks!

[Johan Commelin]

Thanks! Please kick it on the queue after CI gives a :check:

[Michael Stoll]

OK.

[Johan Commelin]

eliminary result in some mod_forms repo/project, for example

[Johan Commelin]

Sorry for the noise. I blame the German railway network and mobile internet infrastructure.

[Joachim Breitner]

I see you have started to assimilate. Complaining about the Deutsche Bahn is a national past time here.

[Michael Stoll]

Is there a simpler way of proving the following?

import tactic
import algebra.parity

example {α} [group α] (a : α) : (∃ x : α, x ^ 2 = a) ↔ ∃ x : α, a = x ^ 2 :=
begin
  split;
  { rintro ⟨x, h⟩,
    use x,
    exact h.symm, }
end

[Yaël Dillies]

by simp_rw eq_comm or exists_congr $ λ _, eq_comm

[Yaël Dillies]

A useful general rule to remember is that foo.symm : foo x y → foo y x and foo_comm : foo x y ↔ foo y x

[Michael Stoll]

Which of the two would be preferred for mathlib?

[Yaël Dillies]

Either is fine. The second one is particularly useful if you're building a proof term.

[Michael Stoll]

I'm not so much into building proof terms (yet?)... :smile:

[Michael Stoll]

The next PR is #13667.
It mainly changes the definition of legendre_sym to use quadratic_charfor zmod p. Then we can use properties of the quadratic character to prove corresponding properties of the Legendre symbol. I'm also adding a few more API lemmas.

[Michael Stoll]

The next steps will be to add statements on the quadratic character of -1 (first in quadratic_char.lean) and then on the quadratic character of 2. The ultimate goal here is to formalise the proof of QR using Gauss sums (and use this to replace the current proof using Gauss' and Eisenstein's lemmas).

[Kevin Buzzard]

Probably in the tactic proof you can do exact \<x, h.symm\> instead of use + exact (untested but I'm optimistic); exist goals are no different to any other structure so you can use the pointy bracket constructor to just build the term you want.

[Kevin Buzzard]

To give a term of type exists a, P a is to give a pair consisting of a term x and a proof of P x.

[Michael Stoll]

I would like to write down the set {x : F | x ^ 2 = a} as a finset (where F is a finite field and a : F). How do I do that?

[Yaël Dillies]

finset.univ.filter (λ x, x ^ 2 = a). You will need decidable_eq F.

[Michael Stoll]

Thanks. It doesn't read very naturally, though...

[Kevin Buzzard]

In Lean 3, the { x : X | P x} notation is built into core Lean IIRC, which means it's very inflexible. In Lean 4 syntax will be super-flexible and it would not surprise me if one could use this notation or something very close to it to make finsets from fintypes.

[Yaël Dillies]

Yeah, docs#finset.filter is really the same as docs#set.sep, and it's a bit of a shame that the notation doesn't follow through.

[Kevin Buzzard]

I guess one issue is that people might still want to make subsets from fintypes, so one might have to use separate notation for the two constructions.

[Yaël Dillies]

Context can be enough to infer the type.

[Michael Stoll]

Is something like this in mathlib?

example {F} [field F] (a b : F) (h : b ^ 2 = a) (x : F) : x ^ 2 = a ↔ x = b ∨ x = -b := sorry

(The assumptions can be weakened, of course.)

[Yaël Dillies]

We have docs#sq_eq_sq_iff_abs_eq_abs which is pretty close

[Michael Stoll]

docs#eq_or_eq_neg_of_sq_eq_sq
The other one requires a linearly ordered structure.

[Yaël Dillies]

Ah that's the one I was looking for!

[Yaël Dillies]

Why is it not stated as an iff?

[Michael Stoll]

Yaël Dillies said:

finset.univ.filter (λ x, x ^ 2 = a). You will need decidable_eq F.

I would expect something like

set_to_finset_of_fintype {T} [fintype T] (s : set T) : finset T

in mathlib, with the obvious property that ↑(set_to_finset_of_fintype s) = s.

[Michael Stoll]

... so that I could write set_ot_finset_of_fintype {x : F | x ^ 2 = a}.

[Yaël Dillies]

docs#set.to_finset

[Kevin Buzzard]

We don't include of_fintype in the name because it doesn't work otherwise so you can infer it

[Michael Stoll]

Is there also coe : set T → finset T? When I tried {x : F | x^2 = a} : finset F, it didn't work.

[Kevin Buzzard]

And docs#set.coe_to_finset . Note that you can use dot notation. Does {x : P x}.to_finset work though?

[Kevin Buzzard]

I think there won't be a coercion because I think the type class inference system handles it and there's a coercion the other way so this would give a loop

[Michael Stoll]

docs#set.coe_to_finset is just the specification.

[Kevin Buzzard]

But I'm not an expert in these matters, I could be wrong

[Kevin Buzzard]

Right -- the specification is the "obvious property" you wanted above, right?

[Michael Stoll]

{x : F | x^2 = a}.to_finset does typecheck.

[Michael Stoll]

#13667 has now a merge conflict. Apparently some other PR changed number_theory/legendre_symbol/quadratic_reciprocity.lean before my PR was merged. How do I resolve this?

[Eric Wieser]

You can either click the "resolve conflicts" button in-browser, which will give you a clumsy editor and markers along the lines of

<<<<<<< your_branch
lemma your_version
=======
lemma their_version
>>>>>>> master

or you can run git fetch; git merge origin/master locally, and solve the same markers in vscode

[Eric Wieser]

(your goal is to merge the things within the <<<<<< ... ====== ... >>>>>)

[Michael Stoll]

@Johan Commelin can you (or somebody else) have a look at #13667 at some point?

[Michael Stoll]

On the latest commit of #13667, I get the message that "Lint mathlib failed", but when I click on "Details", the orange circle in front of "lint" is still spinning. So how do I figure out what the complaint is? (Adding #lint to the bottom of the files I changed does not turn up any problems, BTW.)

[Oliver Nash]

I'd guess the linter failed to __run__ (for unknown reasons) rather than to succeed.

[Oliver Nash]

I've just clicked the "rerun" button: if this succeeds then my above hypothesis is very likely correct.

[Michael Stoll]

OK, thanks! Let's see what happens.

[Michael Stoll]

Looks good...

[Michael Stoll]

@Johan Commelin I made the suggested change to #13667. It should be ready now.

[Johan Commelin]

Thanks for the ping:

[Michael Stoll]

Thanks!

[Michael Stoll]

@Damiano Testa Why is docs#even.neg_one_pow not a simp lemma? (docs#odd.neg_one_pow is.)

[Yaël Dillies]

I was the one (re)writing it two weeks ago. Neither even.neg_one_pow nor odd.neg_pow is a simp lemma because even n or odd n is not a precondition that's usually filled by simp (or rather we have specific lemmas when it is).

[Yaël Dillies]

docs#even.neg_one_zpow and docs#odd.neg_one_zpow are not simp either. I don't know where you've seen this.

[Yaël Dillies]

The relevant PR is #13268.

[Damiano Testa]

Yaël already gave a justification. I am not too sure of what constitutes a good simp lemma and what does not. Until recently, I would have probably thought "even/odd" is a condition that simp will not produce, so this lemma should always be passed onto simp to trigger it, defeating the purpose of the simp tag.

However, Johan pointed out to me that if even 2 were a simp lemma (maybe it is, I'm on mobile), then the lemma might trigger when n = 2. So, my heuristic is not correct and I am back at not knowing what a good simp lemma is!

[Yaël Dillies]

But 2 = bit0 1, and we have lemmas about (-a)^bit0 b.

[Damiano Testa]

So, I think that I am even further back at the step where I am not really sure what is a good simp lemma!

[Michael Stoll]

Yaël Dillies said:

docs#even.neg_one_zpow and docs#odd.neg_one_zpow are not simp either. I don't know where you've seen this.

You are right; I guess my eye slipped to the next line (where docs#even_neg_two is a simp lemma). Sorry about that; I was getting tired...

[Kevin Buzzard]

@Damiano Testa the concept of a good simp lemma is a bit subtle. Scott once mentioned to me that I could do a better job of teaching simp in NNG; the explanation was that I didn't understand simp at the time myself. One thing which suddenly made it all look easy was when I learnt about the Knuth-Bendix theorem, which gives a concrete Noetherian confluent rewrite system for groups ie proves that you can make a group tactic like ring but for groups just with the command simp only [mul_assoc, one_inv, ...] (you need about ten random statements in group theory of the form X=Y with Y in some kind of simpler form than X). However that doesn't mean that all the things on the list are good simp lemmas in practice! For example mul_assoc is not a simp lemma.

[Michael Stoll]

Damiano Testa said:

However, Johan pointed out to me that if even 2 were a simp lemma (maybe it is, I'm on mobile), then the lemma might trigger when n = 2. So, my heuristic is not correct and I am back at not knowing what a good simp lemma is!

docs#even_two is a simp lemma in fact (as is docs#even_neg_two).
I would think that if I have a hypothesis h : even n in my context and docs#even.neg_one_pow were a simp lemma,
then simp [h] would simpify (-1)^n to 1, which could be useful.

[Johan Commelin]

That's true. But arguably it shouldn't be in the default simp-set. Maybe simp [h, even.neg_one_pow] is also a reasonable way.
In this case, there is also another option: add it to the parity_simps simp-set. Then simp [h] with parity_simps will make that simplification.

[Johan Commelin]

In the end, this is a question about balancing UX (user experience) vs performance.

[Johan Commelin]

Putting everything in the default simp-set makes it easy to have short proofs, and it can help people discover simp-lemmas that they didn't know about. But it comes at the cost/risk of making the default simp-set very slow.

[Michael Stoll]

Of course, I can use simp [even.neg_one_pow h] in any case.

[Yaël Dillies]

You mean h.neg_one_pow!

[Damiano Testa]

Kevin, thanks for putting this concept in words! I have observed something similar while working with laurent_polynomial, where I feel that I am declaring lemmas to be simp, just because it makes sense in this context. In this situation, I am helped by the fact that they are in the laurent_polynomial namespace, so they won't trigger when they shouldn't. The situation is different with mul_assoc, of course.

[Scott Morrison]

You know simp doesn't care about namespaces? They are all there as soon as the file is imported.

[Damiano Testa]

Scott, I do, what I meant is that they will not apply unless you really have a laurent_polynomial, in which case they are useful!

[Damiano Testa]

It is just that the lemmas "look like" they would apply to polynomials as well, but they do not!

[Kevin Buzzard]

I think it's more the type of the lemma, rather than the namespace, which is making that happen.

[Damiano Testa]

Yes, maybe I should have said that the types of the lemmas all contain laurent_polynomial somewhere, rather than confusing this with the fact that the lemmas are all in the laurent_polynomial namespace.

[Kevin Buzzard]

Another simp story while I'm waiting for a local LTE to compile: when I made the complex number game (a super-unpopular game because I never made a web interface, despite the fact that the levels are really clean), I found that to prove that the complex numbers were a ring it was great to have z = w \iff z.re = w.re \and z.im = w.im in the simp set, because I was proving all the ring axioms, which are equalities, and I always wanted to do it by checking on real and imaginary parts. But then Scott pointed out to me that you don't want that to be the default behaviour in the wild, because people don't want simp randomly breaking up their equality of some random integrals into real and imaginary parts. Better to use the proper tool, which is ext.

[Damiano Testa]

Actually, this makes me think that I sometimes wonder why the lemma that says that a product is zero iff one of its factors is zero (with appropriate typeclass assumptions) is in the simp set: I almost never want to get to an or in my proofs! And I constantly go through the loop:
simp → squeeze_simp → Try this add a - in front of the name of the lemma, remove only and squeeze again!

[Damiano Testa]

docs#mul_eq_zero: I was convinced that the name of the lemma was more complicated...

[Michael Stoll]

New PR: #13831 adds two properties of quadratic characters/Legendre symbols (value is -1 precisely on non-squares and number of square roots of a given element is 1 plus the value of the character).

[Michael Stoll]

We have docs#nat.odd_of_mod_four_eq_one and docs#nat.odd_of_mod_four_eq_three. For the API for the quadratic character of -1, I will need the converse, i.e.,

lemma nat.odd_mod_four {n : nat} (hn : n % 2 = 1) : n % 4 = 1 \or n % 4 = 3

Would it make sense to put it next to the other two? And is the name OK? (I don't like nat.eq_one_or_three_mod_four_of_odd, since I will also need a similar one for mod 8, and the name would get really unwieldy...)

[Michael Stoll]

Should there also be counterparts for int?

[Michael Stoll]

@Johan Commelin Can you have a look at #13831 (see above) at some point?

[Michael Stoll]

I'd also like to get feedback on nat.odd_mod_four...

[Johan Commelin]

@Michael Stoll I left some comments

[Michael Stoll]

@Johan Commelin I have replied to your comments on #13831.

[Michael Stoll]

There is a new PR: #13978.
It adds results on the quadratic character of -1; the main new lemmas are

variables {F : Type*} [field F] [fintype F]

lemma char.quadratic_char_neg_one [decidable_eq F] (hF : ring_char F ≠ 2) :
  quadratic_char F (-1) = χ₄ (fintype.card F)

lemma char.is_square_neg_one_iff : is_square (-1 : F) ↔ fintype.card F % 4 ≠ 3

The first has a counterpart for the Legendre symbol; the second was already present in a similar form (but now has a simpler proof based on char.is_square_neg_one_iff). I have taken the liberty of rewriting the statement in terms of is_square (rather than spelling it out explicitly); similarly for zmod.euler_criterion.

I needed some additional auxiliary lemmas (odd_mod_four as mentioned earlier and finite_field.even_card_of_char_two), which I have added near the top of number_theory/legendre_symbol/quadratic_char.lean; the plan is to collect these auxiliary lemmas there and move them collectively to appropriate places at some later point.
There is also some API for the quadratic character mod 4, zmod.χ₄.
Perhaps @Johan Commelin can have a look, but of course, everybody is welcome to review it.

[Michael Stoll]

@Johan Commelin Can you have another look? The points you raised should now be dealt with.

[Johan Commelin]

LGTM

[Michael Stoll]

New PR #14027. This just moves the auxiliary lemmas into a separate file, to facilitate future changes. @Johan Commelin

[Michael Stoll]

Another PR that is meant to improve the file structure: #14178. It moves the material on the quadratic characters on zmod 4 and zmod 8 to a separate file zmod_char.lean (within number_theory/legendre_symbol/) and also adds some API lemmas for the characters on zmod 8 (and shortens a proof). @Johan Commelin

[Michael Stoll]

I have code for the "Gauss sum proof" of the value of the quadratic character at 2, but before I add this, I want to see if it can be obtained from more general Gauss sum machinery (which I will need for the Gauss sum proof of Quadratic Reciprocity).

[Johan Commelin]

LGTM!

[Johan Commelin]

@Michael Stoll Do you think it's worth it to deduplicate the two characters for n = 8, by passing a parameter to the character?

[Michael Stoll]

@Johan Commelin I don't think it would save a lot of code (I don't really expect more API lemmas here). We can perhaps lookt at it again at some later point.

[Michael Stoll]

I have now finished writing the code that leads to the proof of Quadratic Reciprocity via Gauss sums.

This is a total of ~1400 lines of code. Would the following be a reasonable sequence of PRs?

1. Add the necessary auxiliary statements to number_theory/legendre_symbol/auxiliary.lean (~200 lines)
2. Add results on multiplicative characters (new file .../mul_character.lean, ~200 lines)
3. Add results on additive characters (new file .../add_character.lean, ~300 lines)
4. Add results on Gauss sums (new file .../gauss_sum.lean, ~400 lines)
5. Add results on the value of the quadratic character at 2 and at odd primes to .../quadratic_char.lean (~150 lines)
6. Add corresponding statements to .../quadratic_reciprocity.lean (replacing the current combinatorial proofs) and move the Gauss and Eisenstein lemmas to .../gauss_eisenstein_lemmas.lean

@Johan Commelin

[Kevin Buzzard]

This sounds great to me, keeping stuff <= 200 lines is really helpful to the maintainers

[Michael Stoll]

I take it that 400 may still be OK?

[Michael Stoll]

Of course, if desired, I can split the longer files into two parts and PR them separately.

[Kevin Buzzard]

Once you've got good at PRs people are a lot more tolerant of 400 line efforts :-)

[Violeta Hernández]

you can sometimes convince them of much larger things if you're good enough or nagging enough

[Johan Commelin]

@Michael Stoll Sounds like a good plan to me.

[Johan Commelin]

Also "400 lines in one file" is typically easier to review than "300 lines scattered across 5 files".

[Michael Stoll]

The first PR is there: #14572

[Johan Commelin]

@Michael Stoll Concerning the Github discussion about moving preliminary lemmas. Do you already have a good overview of 10-20 prelim lemmas that you'll be adding in the next few PRs? Because then you could already gather all of those together now, and make a prep PR first.

[Michael Stoll]

@Johan Commelin That's what I'm doing with #14572. It should contain all the lemmas I need for the sequence of PRs I outlined.
When the sequence of PRs is complete, we can move everything that is in auxiliary.lean to appropriate places (that would be number 7 in the list above).

[Michael Stoll]

I've edited the message above to add item number 7.

[Alex J. Best]

I still don't really understand why not make step 1 and 7 at the same time then? That seems way less confusing for review. If 1 is merged with lemmas in the right place you will soon get the olean files for it and not have to recompile anything later

[Yaël Dillies]

Yes, step 1 and step 7 should be one and only. We basically never purposefully put lemmas in the wrong place (I've only done it once, and it was to ease a refactor touching 138 files).

[Michael Stoll]

OK; if you tell me where to put each lemma, then I'll move them now. I just would like to avoid having to make changes later on (beacuse a lemma was moved to the "wrong" file or was too specific or ...).

[Yaël Dillies]

That's why reviewing is for :wink:

[Yaël Dillies]

The best way to decide where a lemma should go is by

1. Looking for similar lemmas
2. Looking for the lemmas used in the proof

[Michael Stoll]

Is there a way of avoiding triggering CI every time I push a commit? Building/linting mathlib is likely to take a long time each time I modify a file like algebra/group/basic.lean...

[Johan Commelin]

If you push, the previous runs will automatically be cancelled.

[Johan Commelin]

If you still want to save CI cycles, I guess the solution is to commit, but postpone pushing till you have a batch of commits that you want to test with CI.

[Alex J. Best]

Or you can manually cancel if you still want to have the commits distributed. If the GitHub actions extension for vscode or the command like gh tool supports cancelling actions this could be quite quick

[Michael Stoll]

I was thinking of having the review process work its way without triggering CI. This will reqire that I push the commits so that reviewers can see them and comment on them.

[Michael Stoll]

Perhaps one way to go is for me to add comments to the lemmas with suggestions where they should go?
If there are no objections, I can then move them and hope for the best...

[Michael Stoll]

@Johan Commelin @Alex J. Best @Yaël Dillies I have now added suggestions regarding suitable places for the lemmas to #14572. Please comment!

[Michael Stoll]

@Johan Commelin @Alex J. Best @Yaël Dillies How can I help to push this along reasonably quickly?
I'd like to get on to the "real" stuff...

[Yaël Dillies]

Yaël Dillies said:

The best way to decide where a lemma should go is by

1. Looking for similar lemmas
2. Looking for the lemmas used in the proof

Have you tried doing this? :point_of_information:

[Yaël Dillies]

Also, what are we supposed to do with your suggestions? We're the ones suggesting and you're the one changing :grinning:

[Michael Stoll]

I basically did what you said and added suggestions (in comments) where the lemmas should go.

[Michael Stoll]

I'm basically waiting to see if you think they make sense, as I would like to avoid moving things around several times.

[Michael Stoll]

Also, in some cases, the obvious files are missing some imports, and I'm not sure what the established way is in such cases.

[Yaël Dillies]

See point number 1.

[Michael Stoll]

Can you define "similar"?

[Yaël Dillies]

When this happens, it usually means that there's a file lower down the hierarchy which has the same theme but heavier imports.

[Yaël Dillies]

By "similar", I mean similar conclusions and similar assumptions (including instance ones!).

[Yaël Dillies]

See file#data/set/pointwise, file#analysis/normed/group/pointwise, file#analysis/normed_space/pointwise for an example of such file gradation.

[Michael Stoll]

For example, there does not seem to be a file that imports both algebra.group.unitsand algebra.char_p.basic.
(BTW, is there a way to check that rigorously without clicking through everything?)

[Yaël Dillies]

This is probably false, given that algebra.group.units is very low down the hierarchy. You can try @Eric Wieser's import tree tool, but I haven't yet managed to use it myself.

[Michael Stoll]

If it is false, how do I find a file that imports both?

[Yaël Dillies]

You can also write #check some_declaration_in_algebra_group_units in algebra.char_p.basic and see whether Lean knows the declaration.

[Eric Wieser]

If the tool you're talking about is my visualization, it's not useful for this

[Eric Wieser]

I think there's another thread with some python or JavaScript code that _might_ be useful

[Yaël Dillies]

Yes, I'm talking about the python code.

[Yaël Dillies]

... and indeed

import algebra.char_p.basic

#check units
-- units : Π (α : Type u_1) [_inst_1 : monoid α], Type u_1

[Michael Stoll]

OK; it tlooks like the chain from algebra.char_p.basic to algebra.group.units is fairly long, though.

[Michael Stoll]

Anyway, I still don't quite know what to do. If you say you are the ones suggesting and I'm supposed to make the changes, then I'm missing the suggestions.

[Yaël Dillies]

I am currently writing some :wink:

[Michael Stoll]

@Yaël Dillies @Johan Commelin Are there any further suggested changes to #14572?

[Yaël Dillies]

It would be easier if you simply performed the moves instead of waiting for our pre-emptive approval, which you won't get because it's much easier to review things when they are in the correct place.

[Michael Stoll]

I'm trying to do that now.
My experience is that when I change things in files like algebra.char_p.basic, then work becomes nearly impossible -- orange bars won't go away, building takes ages...
So I would like to endure this only once if possible.

[Michael Stoll]

Actually, data.nat.modeq is even worse...

[Mario Carneiro]

you can check the file itself without too much trouble, and if you are working on a different file which is far away you can either lean --make that particular file which shouldn't take too long, or you can push to the PR and wait for CI to finish to download the oleans

[Mario Carneiro]

Don't try to use the server itself to compile that far away file. It's a complete waste of resources because it doesn't produce oleans on disk and is more likely to cause lean to run out of memory

[Yaël Dillies]

The trick is to touch the far away files top to bottom. That is, if A imports B and you want to modify them both, start by modifying B. And close the file you're moving the lemmas from, to avoid triggering its recompilation.

[Michael Stoll]

Mario Carneiro said:

you can check the file itself without too much trouble, and if you are working on a different file which is far away you can either lean --make that particular file which shouldn't take too long, or you can push to the PR and wait for CI to finish to download the oleans

lean --make the relevant files also takes something like two hours...

[Michael Stoll]

Anyway, I have now moved everything (and deleted auxiliary.lean).

[Michael Stoll]

Let's see how long CI will take...

[Michael Stoll]

Building mathlib failed after two hours, but clicking on the "details" link showed the orange circle still spinning at "leanpkg build", so I restarted the faeild job(s). Now it progressed to linting...

[Michael Stoll]

#14572 is now green. It would be nice if it could be merged soon.

[Riccardo Brasca]

Can you please hit the Resolve conversation button if you've taken into account a comment?

[Riccardo Brasca]

(This has no effect on the code, but it makes easier to read the discussion.)

[Riccardo Brasca]

I think it's almost ready to go.

[Michael Stoll]

Just doing the two hours recompilation of everything between algebra.group_power.basic and field_theory.finite.basic again on my machine, so that I can then check the comment on field_theory.finite.trace...

[Yaël Dillies]

You know how to get cache using leanproject, right?

[Michael Stoll]

I changed algebra.group_power.basic by adding the suggested simp lemmas, so I don't see how I can avoid the recompilation (other than pushing and then later getting the new oleans from the branch, which I assume would not really be faster).

[Yaël Dillies]

You can temporarily cancel the changes you made to get back to a situation you have the oleans for, do the other changes, then put back the changes which invalidated the oleans and tada!

[Michael Stoll]

It just finished. I guess the real problem was data.nat.modeq when I did this before (and it took two hours or so).

[Alex J. Best]

Michael, have you seen https://leanprover-community.github.io/tips_and_tricks.html#old-mode, if you are sure that you just changed a proof or docstring or lemma only used by you and want to quickly get working on other stuff based on it, you can use this flag to tell lean to ignore intermediate files. I.e. pretend that they still compile fine

[Michael Stoll]

Yes, but I have tried to avoid that so far.

[Michael Stoll]

I have now pushed the changes that were suggested.

[Michael Stoll]

bors tells me that #14572 was merged, but when I download mathlib, the changes are not there. Do I just have to wait a bit longer, or is there a problem somewhere?

[Patrick Stevens]

What precisely are you doing when you say you "download mathlib"?

[Patrick Stevens]

(For example, git pull for me correctly points origin/master to commit d6eb634b58906ef0cc4bba155e099da9d7d99615, which is the most recent commit according to GitHub and which is the commit resulting from the merge of #14572.)

[Michael Stoll]

I did leanproject up in another project.

[Michael Stoll]

Also, https://leanprover-community.github.io/mathlib_docs/ still mentions 97c9ef8cd3e7a896a61ee35aa39c7827e03980ce, which is the commit before #14572.

[Michael Stoll]

OK, now I get the latest commit. So I guess it takes a while until it becomes visible?

[Patrick Stevens]

The documentation is rendered automatically from https://github.com/leanprover-community/mathlib_docs which happens some time after the commit enters master, yes. I don't know about leanproject up, although looking at its definition (https://github.com/leanprover-community/mathlib-tools/blob/bdae7e9ae3e014fd845e7023e68a084e1165c9a2/mathlibtools/lib.py#L755) it really should be instant unless you were on the wrong git branch; were you on master when you ran leanproject up?

[Michael Stoll]

I realized that I forgot to update the module docstring for the new file field_theory.finite.trace after I removed the definition of trace_to_zmod. I'm fixing this with #14711.

[Michael Stoll]

I have now made the next PR (adding results on multiplicative characters): #14716.

[Michael Stoll]

@Alex J. Best @Riccardo Brasca

[Riccardo Brasca]

I've left a couple of comments, but I think you should define what a mul_character is. If we do it carefully we can take advantage of the existing API for monoid_with_zero_hom and friends.

[Riccardo Brasca]

Unless for you a multiplicative character it's just a monoid_with_zero_hom (I don't know if we want nonunits to be mapped to 0 or not).

[Michael Stoll]

In applications, the domain will usually be a field (then 0 is the only non-unit). I didn't want to restrict what a multiplicative character is (beyond a monoid_with_zero_hom), since I'm not sure whether there might be cases where it's reasonable to use a map that takes nonzero values on some non-units.
In the intended application (to Gauss sums), I do have an assumption that non-units are mapped to zero in some places, though.

[Riccardo Brasca]

Well, I think this is a delicate question. It's really important to set up good definitions. If we map nonunits to 0 then multiplicative characters form a group, right? So this allows all the usual notation χ ^ 0 would be the trivial character, and that's nice.

[Riccardo Brasca]

Because otherwise you have to prove by hand all the stuff like χ ^ (n + m) = ..., and that can be a lot of work

[Michael Stoll]

OK. I see the following advantages.

• commutative group structure on mul_char R R' (as you mentioned)
• no need for extra hypotheses that non-units are mapped to zero
• can define, e.g., Dirichlet characters modulo n as composition of ℤ → zmod n with a mul_char (zmod n) ℂ

Disadvantages:

• Dirichlet characters are not mul_chars (there are very few mul_chars on the integers with the restricted def.)
• the comm_group structure has a lot of fields that need to be filled
• whenever one constructs a mul_char, one has a proof obligations that non-units are mapped to zero

[Michael Stoll]

But I would think that the advantages are worth it.

[Michael Stoll]

Would it be better to define mul_char as an extension of monoid_with_zero_hom or as an extension of monoid_hom?
In both cases by a field map_non_unit (or so) that contains a proof that non-units are mapped to zero, I would think.

[Michael Stoll]

And I may need some help in setting this up in the right way, since I haven't yet done something similar so far.

[Michael Stoll]

I have now managed to get a comm_group instance on mul_char R R'. I will continue with rewriting the file to see how well I can work with it and then push a new version (perhaps tomorrow).

[Riccardo Brasca]

Hmm, I don't know, excluding Dirichlet character seems quite bad.

[Yaël Dillies]

Sending non-units to zero is the wrong behavior for the inverse in a docs#division_monoid, at least.

[Riccardo Brasca]

Sacrificing the inverse is not a big deal. But I am afraid we are missing a good pnat-powers API on semigroups...

[Riccardo Brasca]

The point is that the theory is a mess. Peoples tend to modify these little details to their needs, but we really want a uniform definition, otherwise we will have to do a lot of code duplication.

[Michael Stoll]

Yaël Dillies said:

Sending non-units to zero is the wrong behavior for the inverse in a docs#division_monoid, at least.

The nice thing with this definition is that one does get a commutative group structure (it is isomorphic to the group structure on group homomorphisms from the units of the domain ring into the units of the target ring), which should make it easier to work with the characters. I'll now continue working on the file, using the group structure.

[Michael Stoll]

@Alex J. Best @Riccardo Brasca @Yaël Dillies Is the following reasonable?
I add the variant with non_units mapped to zero as another file mul_char_alt.lean for comparison in #14716 (and mark the PR as WIP for the time being), so that the two can be compared.

[Riccardo Brasca]

Thanks, it's good that we can see both versions. I suggest you open a new thread with your question (the title of this one refers to something else).

[Michael Stoll]

The title of this one refers to the end goal :smile:, but it looks like there are quite some detours on the way...

[Michael Stoll]

I'll push the alternative file tomorrow (and open a new thread at the same time). It is getting late, and I'm tired...

[Junyan Xu]

I add the variant with non_units mapped to zero as another file mul_char_alt.lean for comparison in #14716 (and mark the PR as WIP for the time being), so that the two can be compared.

Isn't it better create another branch but leave it in the same file, so we can compare the new branch with the current branch side by side? If you implement the change in one commit (in the new branch), then we can just look at the diff of that one commit.

[Ashvni Narayanan]

Michael Stoll said:

OK. I see the following advantages.

• commutative group structure on mul_char R R' (as you mentioned)
• no need for extra hypotheses that non-units are mapped to zero
• can define, e.g., Dirichlet characters modulo n as composition of ℤ → zmod n with a mul_char (zmod n) ℂ

Disadvantages:

• Dirichlet characters are not mul_chars (there are very few mul_chars on the integers with the restricted def.)
• the comm_group structure has a lot of fields that need to be filled
• whenever one constructs a mul_char, one has a proof obligations that non-units are mapped to zero

Hi, I have done some stuff on Dirichlet characters, in case you are interested

[Ashvni Narayanan]

https://github.com/leanprover-community/mathlib/blob/p-adic/src/number_theory/dirichlet_character.lean

[Ashvni Narayanan]

And https://github.com/leanprover-community/mathlib/blob/p-adic/src/number_theory/dirichlet_character_properties.lean

[Michael Stoll]

Junyan Xu said:

Isn't it better create another branch but leave it in the same file, so we can compare the new branch with the current branch side by side? If you implement the change in one commit (in the new branch), then we can just look at the diff of that one commit.

How would I do that? (Still a beginner with git...)

[Junyan Xu]

For each PR you create a branch, so you know how to create a new branch right? Instead of creating it out of master, you could also create it out of another existing branch, like the branch legendre_symbol_mul_char in #14716. Github allows you to compare any two branches even without opening PR (but comment is not possible without PR), and each commit also has its own diff view.

[Michael Stoll]

The variant implementation is at #14768 now.
@Alex J. Best @Riccardo Brasca @Kevin Buzzard @Ashvni Narayanan

[Michael Stoll]

Ashvni Narayanan said:

https://github.com/leanprover-community/mathlib/blob/p-adic/src/number_theory/dirichlet_character.lean

Thanks for the pointers. My goal at this point is to define Gauss sums and prove some properties, so I need (additive and multiplicative) characters on finite commutative rings. But it would certainly make sense to have some interface with Dirichlet characters eventually.

[Michael Stoll]

I have now started a separate topic to discuss the relative merits of the two approaches to multiplicative characters.

[Kevin Buzzard]

@Michael Stoll Why not change all the R's to Cs, for the following reason. I find it really helpful when reading mathlib code to follow good variable naming conventions. This is something which apparently doesn't exist in computer science (they just say {\alpha \beta \gamma \delta : Type*} whether they're groups or fields or whatever. Your R' , the target ring, is the ring of coefficients, so C.

Imagine trying to explain your code to a smart 17 year old. You tell them that is says R is a ring, but if you like you can just pretend it's $\mathbb{R}$, the reals (I often do this with 1st year undergraduates when we're looking at modules over rings in Lean, I just say imagine R=$\mathbb{R}$ and tell them that module is French for vector space). And similarly C is a ring, but you can just imagine it's the complexes if you don't know what a ring is, because in practice it often is.

[Michael Stoll]

I'll keep this in mind for later. But since I don't want to do twice the work, I'd like to wait until it is clear which of the two variants will make it.