mem_roots_of_unity_of_abs_eq_one

Stream: FLT-regular

[Xavier Roblot]

I have started to work on adding mem_roots_of_unity_of_abs_eq_one to mathlib. Since the whole thing is quite big and involves different parts, I think it might be easier to split into several PR. Here are some ideas on how I could that. Please let me know what you think about this proposal.

• General results about embeddings of number field (definitions, proof there are as many as the degree of the field, lift to an extension, etc) are quite basic results in algebraic number theory, so I think they belong to src/number_theory/number_field.lean. In the same way, I think that the fact that $\mathbb{Q}[X]/(f)$, for $f(X) \in \mathbb{Q}[X]$ irreducible, is a number field also belongs to src/number_theory/number_field.lean. This should be an easy PR.

• There are results about polynomials by @Alex J. Best culminating with the expression of the coefficients of a polynomial in terms of its roots. These are quite technical and quite long. Looking at similar results, they probably belong to field_theory.splitting_field where weak versions of this result can be find, such as: docs#polynomial.prod_roots_eq_coeff_zero_of_monic_of_split or docs#polynomial.sum_roots_eq_next_coeff_of_monic_of_split. This should be a separate PR and I might need Alex help for this one (Alex notes that one could probably shorten the proof by using the results in ring_theory.polynomial.vieta so I'll have to figure that out).

• There are two simp lemmas that should probably be added in another PR to the right place (I'll have to think where that is exactly) if people thinks they are useful.

@[simp] lemma ring_hom.apply_eq_zero_iff_of_injective {R S : Type*} [non_assoc_semiring R]
  [non_assoc_semiring S] {f : R →+* S} (hf : function.injective f) (x : R) : f x = 0 ↔ x = 0 :=
⟨λ h, hf $ by rw [h, f.map_zero], λ h, by rw [h, f.map_zero]⟩

@[simp] lemma map_eq_zero_of_injective [semiring S] {f : R →+* S}
  (hf : function.injective f) : p.map f = 0 ↔ p = 0 :=
by simp [polynomial.ext_iff, coeff_map, ring_hom.apply_eq_zero_iff_of_injective hf, coeff_zero]

• Once everything else is in place, I'll do a last PR to add the two mains results: mem_roots_of_unity_of_abs_eq_one and absolute_value_one to cyclotomic.lean

PS. @Alex J. Best, just by curiosity, I see that you use section forward and section backward in the files. Does that mean anything special?

[Riccardo Brasca]

Splitting a PR is generally a good idea. You can also create dependent PRs to show where are you going, but this is not necessary. Also, don't be afraid of creating new files if you don't find one with all the required imports.

Concerning flt-regular, if can you please move the material you have PRed to the folder ready_for_mathlib, adding a comment with the PR number? I will try to keep https://github.com/leanprover-community/flt-regular/wiki updated.

[Alex J. Best]

I think that some of the results I proved are basically unintentional duplicates of those in ring_theory.polynomial.vieta, I'm not sure if mine were better in any way (e.g. less strict assumptions), but it might be the case that some of the long technical proofs can be deleted

[Alex J. Best]

I don't recall forwards/backwards being anything special, maybe just the directions of an iff statement?

[Alex J. Best]

Hmm I'm not sure if those simp lemmas will fire as simp lemmas very often, as they have side conditions that seem like simp won't prove that often, they certainly seem useful to have though, so I'm not sure if they are worth adding. It may be more harm than good in this case

[Alex J. Best]

Great that you are PRing this material!

[Xavier Roblot]

Ok. Thanks for the advice. I'll start working on the PRs now.

[Xavier Roblot]

The following auxiliary result from Alex is very useful at a couple of places for the proofs I am trying to PR but is not directly related to the content of the PR:

lemma mem_roots_map_of_injective [comm_ring S] [is_domain S] {f : R →+* S} {x : S}
  (hf : function.injective f) (hp : p ≠ 0) : x ∈ (p.map f).roots ↔ p.eval₂ f x = 0

What is the best strategy in this case:

• Add it to mathlib (say in data.polynomial.ring_division in the same or another PR)
• Incorporate its proof where needed and just delete it

From my personal point of view, I find it a quite useful result and think it could be a nice addition to mathlib.

[Riccardo Brasca]

Surely add it to mathlib!! When in doubts it's almost always better to add a new result rather then repeating its proof over and over (I really think that if you use the same result twice it deserves to be singled out).

Small PR are welcome, but you can also include it in a bigger one, since it is just a couple of lines, this is up to you.

[Xavier Roblot]

Ok. Thanks. I'll do that

[Xavier Roblot]

Sorry, I have not contributed much to the project lately since I was working quite hard on this PR (and I am still far from being done). I have #15008 which seems to be stuck (since it competes with #14908 and nobody seems to want to take a decision about which one to use) and also now #15275 which proves a more general version of a result needed for this PR: if the roots of a polynomial are bounded, then the coefficients are bounded too. This PR depends on #14908 or #15008. I'll work on the main PR now.

[Riccardo Brasca]

I think this week everybody is busy with lftcm so all PRs have to wait a little more than usual...

[Eric Rodriguez]

Lfctm?

[Chris Birkbeck]

https://icerm.brown.edu/topical_workshops/tw-22-lean/#schedule-2022-07-11

[Eric Rodriguez]

Oh, that's cool!

[Riccardo Brasca]

I've updated the graph, turning sum_pow_unit (that it should be is_primitive_root.sum_pow_unit, @Chris Birkbeck can you confirm?) and unit_lemma (thank's @Eric Rodriguez !) green. There is flt_fact_3 that seems easy to do, and maybe also flt_fact_4 (should we find better names?).

[Riccardo Brasca]

We are really close to case I

[Chris Birkbeck]

Ah yes that looks good!

[Chris Birkbeck]

Actually I'm going to change 3.8 to zeta_pow_sub_eq_unit_zeta_sub_one since this is actually what we will use.

[Chris Birkbeck]

But yes we should be really close to case I now.

[Eric Rodriguez]

I think we already have flt_fact_3 as exists_int_sub_pow_prime_dvd, and I _think_ I made that sorry free

[Eric Rodriguez]

I'm also not sure I fully get flt_fact_4

[Chris Birkbeck]

Eric Rodriguez said:

I'm also not sure I fully get flt_fact_4

Maybe thats because I messed up the statement :P It should say what the a_i's are

[Chris Birkbeck]

let me fix that

[Chris Birkbeck]

Eric Rodriguez said:

I think we already have flt_fact_3 as exists_int_sub_pow_prime_dvd, and I _think_ I made that sorry free

This looks pretty sorry free to me.

[Riccardo Brasca]

Yes, it is it, and it is sorry free (confirmed by #print axioms lemma exists_int_sub_pow_prime). I am including it.

[Thomas Browning]

Mathlib already has flt for n=4, doesn't it?

[Riccardo Brasca]

Yes

[Riccardo Brasca]

docs#not_fermat_4

[Thomas Browning]

Ah, I see. flt_fact_4 is not FLT for n=4 :grinning:

[Riccardo Brasca]

We should find better names...

[Chris Birkbeck]

Is the n=3 case in there? I thought I remember seeing this done, but I can't remember if it was in mathlib

[Riccardo Brasca]

It is not in mathlib

[Riccardo Brasca]

https://github.com/Ruben-VandeVelde/flt

[Riccardo Brasca]

@Ruben Van de Velde can we include your code in the flt-regular project? I think we need to tread the case n=3 separately (in exchange we will maintain it updated wrt to mathlib).

[Kevin Buzzard]

What definition of regular do you end up with for case 1?

[Chris Birkbeck]

The class number version

[Kevin Buzzard]

Can you prove that 3 is regular?

[Eric Rodriguez]

I don't even think we can prove 2 is regular

[Kevin Buzzard]

That sounded easier than 3.

[Chris Birkbeck]

I think we can do 2 right? We must know that $\mathbb{Z}$ is a PID?

[Eric Rodriguez]

image.png

[Riccardo Brasca]

For 3 we will need stuff about quadratic fields, but it shouldn't be too hard too prove that it is a PID

[Eric Rodriguez]

the quadratic fields are long overdue in mathlib...

[Alex J. Best]

Me @Anne Baanen @Nirvana Coppola @Sander Dahmen are working on computing small class numbers (and a definition of quadratic fields) it's still in the works but somewhat mature at this point. So hopefully coming within the next couple of months anyways

[Ruben Van de Velde]

Riccardo Brasca said:

Ruben Van de Velde can we include your code in the flt-regular project? I think we need to tread the case n=3 separately (in exchange we will maintain it updated wrt to mathlib).

Yes, of course. I'd been hoping to find time to push it into mathlib, but that hasn't happened yet.

[Eric Rodriguez]

ok, turns out two is doable, although somehow we still have int algebra diamonds there... regardless, the example is there

[Eric Rodriguez]

There's also a lot of definitions that don't push forward or at least get preserved under equivalences that should - is_dedekind_domain is one

[Kevin Buzzard]

Someone here at ICERM is working on quadratic fields! I don't know if they're on the Zulip, I'll tell them about this thread. It might be a nice goal!

[Junyan Xu]

Kevin Buzzard said:

I had a student prove Z[omega] is a Euclidean domain and another student prove Z[sqrt(3)] is a Euclidean domain :-)

Any updates?

[Xavier Roblot]

The PR containing the main result is finally ready: #15143. I also PRed the opposite statement, that is root of unity are of norm 1: #16426.

I put the results in the number_field.lean file but I am wondering if it would be a good idea to make a number_field directory, move the first definitions and results to basic.lean, all the results about embeddings in their own file (I want to work on complex embeddings in the near future) and maybe even put the new result mem_roots_of_unity_of_norm_eq_one in a units.lean file since it is an important step in the proof of Dirichlet unit's theorem. There might be also results about number field, eg. finitude of class groups, that could be moved to this new directory.

[Riccardo Brasca]

I totally agree that number_field should be a directory sooner or later. But this is for another PR

[Kevin Buzzard]

Thanks Xavier! I think it's so cool that this stuff is getting done :-)

[Xavier Roblot]

I am having difficulty merging the project with the version of mem_roots_of_unity_of_abs_eq_one (now called number_field.embeddings.pow_eq_one_of_norm_eq_one) that is in mathlib. To reproduce the problem, merge with the latest version of mathlib and replace line 424 of number_theory/cyclotomic/Unit_lemmas.lean by

  have := @number_field.embeddings.pow_eq_one_of_norm_eq_one K _ _ ℂ _ _ _
    (u * (unit_gal_conj K p u)⁻¹ : K) _ _,

The error is maximum class-instance resolution depth has been reached. Looking at the log with the option trace.class_instances true, I see a lot of output involving ℝ with messages like: @normed_algebra ℝ ℝ real.normed_field.

[Xavier Roblot]

I am afraid, I don't know how to solve this kind of error...

[Eric Rodriguez]

can you push the code that causes the issue to a branch?

[Xavier Roblot]

I pushed to the branch origin/pow_eq_one_of_norm_eq_one (if I got my git commands right).

[Riccardo Brasca]

I am done for today, but I can have a look at tomorrow. Feel free to remove everything it is in mathlib, we will fix the problems.

[Eric Rodriguez]

oh, there seems to be some diamond issue again :(

[Eric Rodriguez]

but it's to do with complex not with any of our stuff..

[Eric Rodriguez]

oh, no, I'm wrong, something weirder is going on...

[Eric Rodriguez]

for now you can put haveI : normed_algebra ℚ ℂ := normed_algebra_rat, before your have := @... line and this will fxi it

[Eric Rodriguez]

I am not sure why the typeclass system is getting lost trying to find this lemma, though

[Eric Rodriguez]

oh, open_locale cyclotomic is at the top of the page, and doesn't seem to be needed

[Eric Rodriguez]

this is super cursed right now, if you remove it it should work fine

[Eric Rodriguez]

the file seems to compile without it

[Xavier Roblot]

Thanks to Eric, I was able to fix the problem and push the new version.

[Riccardo Brasca]

Thanks!

[Xavier Roblot]

I have started to work on adding mem_roots_of_unity_of_abs_eq_one to mathlib. Since the whole thing is quite big and involves different parts, I think it might be easier to split into several PR. Here are some ideas on how I could that. Please let me know what you think about this proposal.

• General results about embeddings of number field (definitions, proof there are as many as the degree of the field, lift to an extension, etc) are quite basic results in algebraic number theory, so I think they belong to src/number_theory/number_field.lean. In the same way, I think that the fact that $\mathbb{Q}[X]/(f)$, for $f(X) \in \mathbb{Q}[X]$ irreducible, is a number field also belongs to src/number_theory/number_field.lean. This should be an easy PR.

• There are results about polynomials by @Alex J. Best culminating with the expression of the coefficients of a polynomial in terms of its roots. These are quite technical and quite long. Looking at similar results, they probably belong to field_theory.splitting_field where weak versions of this result can be find, such as: docs#polynomial.prod_roots_eq_coeff_zero_of_monic_of_split or docs#polynomial.sum_roots_eq_next_coeff_of_monic_of_split. This should be a separate PR and I might need Alex help for this one (Alex notes that one could probably shorten the proof by using the results in ring_theory.polynomial.vieta so I'll have to figure that out).

• There are two simp lemmas that should probably be added in another PR to the right place (I'll have to think where that is exactly) if people thinks they are useful.

@[simp] lemma ring_hom.apply_eq_zero_iff_of_injective {R S : Type*} [non_assoc_semiring R]
  [non_assoc_semiring S] {f : R →+* S} (hf : function.injective f) (x : R) : f x = 0 ↔ x = 0 :=
⟨λ h, hf $ by rw [h, f.map_zero], λ h, by rw [h, f.map_zero]⟩

@[simp] lemma map_eq_zero_of_injective [semiring S] {f : R →+* S}
  (hf : function.injective f) : p.map f = 0 ↔ p = 0 :=
by simp [polynomial.ext_iff, coeff_map, ring_hom.apply_eq_zero_iff_of_injective hf, coeff_zero]

• Once everything else is in place, I'll do a last PR to add the two mains results: mem_roots_of_unity_of_abs_eq_one and absolute_value_one to cyclotomic.lean

PS. @Alex J. Best, just by curiosity, I see that you use section forward and section backward in the files. Does that mean anything special?

[Riccardo Brasca]

Splitting a PR is generally a good idea. You can also create dependent PRs to show where are you going, but this is not necessary. Also, don't be afraid of creating new files if you don't find one with all the required imports.

Concerning flt-regular, if can you please move the material you have PRed to the folder ready_for_mathlib, adding a comment with the PR number? I will try to keep https://github.com/leanprover-community/flt-regular/wiki updated.

[Alex J. Best]

I think that some of the results I proved are basically unintentional duplicates of those in ring_theory.polynomial.vieta, I'm not sure if mine were better in any way (e.g. less strict assumptions), but it might be the case that some of the long technical proofs can be deleted

[Alex J. Best]

I don't recall forwards/backwards being anything special, maybe just the directions of an iff statement?

[Alex J. Best]

Hmm I'm not sure if those simp lemmas will fire as simp lemmas very often, as they have side conditions that seem like simp won't prove that often, they certainly seem useful to have though, so I'm not sure if they are worth adding. It may be more harm than good in this case

[Alex J. Best]

Great that you are PRing this material!

[Xavier Roblot]

Ok. Thanks for the advice. I'll start working on the PRs now.

[Xavier Roblot]

The following auxiliary result from Alex is very useful at a couple of places for the proofs I am trying to PR but is not directly related to the content of the PR:

lemma mem_roots_map_of_injective [comm_ring S] [is_domain S] {f : R →+* S} {x : S}
  (hf : function.injective f) (hp : p ≠ 0) : x ∈ (p.map f).roots ↔ p.eval₂ f x = 0

What is the best strategy in this case:

• Add it to mathlib (say in data.polynomial.ring_division in the same or another PR)
• Incorporate its proof where needed and just delete it

From my personal point of view, I find it a quite useful result and think it could be a nice addition to mathlib.

[Riccardo Brasca]

Surely add it to mathlib!! When in doubts it's almost always better to add a new result rather then repeating its proof over and over (I really think that if you use the same result twice it deserves to be singled out).

Small PR are welcome, but you can also include it in a bigger one, since it is just a couple of lines, this is up to you.

[Xavier Roblot]

Ok. Thanks. I'll do that

[Xavier Roblot]

Sorry, I have not contributed much to the project lately since I was working quite hard on this PR (and I am still far from being done). I have #15008 which seems to be stuck (since it competes with #14908 and nobody seems to want to take a decision about which one to use) and also now #15275 which proves a more general version of a result needed for this PR: if the roots of a polynomial are bounded, then the coefficients are bounded too. This PR depends on #14908 or #15008. I'll work on the main PR now.

[Riccardo Brasca]

I think this week everybody is busy with lftcm so all PRs have to wait a little more than usual...

[Eric Rodriguez]

Lfctm?

[Chris Birkbeck]

https://icerm.brown.edu/topical_workshops/tw-22-lean/#schedule-2022-07-11

[Eric Rodriguez]

Oh, that's cool!

[Riccardo Brasca]

I've updated the graph, turning sum_pow_unit (that it should be is_primitive_root.sum_pow_unit, @Chris Birkbeck can you confirm?) and unit_lemma (thank's @Eric Rodriguez !) green. There is flt_fact_3 that seems easy to do, and maybe also flt_fact_4 (should we find better names?).

[Riccardo Brasca]

We are really close to case I

[Chris Birkbeck]

Ah yes that looks good!

[Chris Birkbeck]

Actually I'm going to change 3.8 to zeta_pow_sub_eq_unit_zeta_sub_one since this is actually what we will use.

[Chris Birkbeck]

But yes we should be really close to case I now.

[Eric Rodriguez]

I think we already have flt_fact_3 as exists_int_sub_pow_prime_dvd, and I _think_ I made that sorry free

[Eric Rodriguez]

I'm also not sure I fully get flt_fact_4

[Chris Birkbeck]

Eric Rodriguez said:

I'm also not sure I fully get flt_fact_4

Maybe thats because I messed up the statement :P It should say what the a_i's are

[Chris Birkbeck]

let me fix that

[Chris Birkbeck]

Eric Rodriguez said:

I think we already have flt_fact_3 as exists_int_sub_pow_prime_dvd, and I _think_ I made that sorry free

This looks pretty sorry free to me.

[Riccardo Brasca]

Yes, it is it, and it is sorry free (confirmed by #print axioms lemma exists_int_sub_pow_prime). I am including it.

[Thomas Browning]

Mathlib already has flt for n=4, doesn't it?

[Riccardo Brasca]

Yes

[Riccardo Brasca]

docs#not_fermat_4

[Thomas Browning]

Ah, I see. flt_fact_4 is not FLT for n=4 :grinning:

[Riccardo Brasca]

We should find better names...

[Chris Birkbeck]

Is the n=3 case in there? I thought I remember seeing this done, but I can't remember if it was in mathlib

[Riccardo Brasca]

It is not in mathlib

[Riccardo Brasca]

https://github.com/Ruben-VandeVelde/flt

[Riccardo Brasca]

@Ruben Van de Velde can we include your code in the flt-regular project? I think we need to tread the case n=3 separately (in exchange we will maintain it updated wrt to mathlib).

[Kevin Buzzard]

What definition of regular do you end up with for case 1?

[Chris Birkbeck]

The class number version

[Kevin Buzzard]

Can you prove that 3 is regular?

[Eric Rodriguez]

I don't even think we can prove 2 is regular

[Kevin Buzzard]

That sounded easier than 3.

[Chris Birkbeck]

I think we can do 2 right? We must know that $\mathbb{Z}$ is a PID?

[Eric Rodriguez]

image.png

[Riccardo Brasca]

For 3 we will need stuff about quadratic fields, but it shouldn't be too hard too prove that it is a PID

[Eric Rodriguez]

the quadratic fields are long overdue in mathlib...

[Alex J. Best]

Me @Anne Baanen @Nirvana Coppola @Sander Dahmen are working on computing small class numbers (and a definition of quadratic fields) it's still in the works but somewhat mature at this point. So hopefully coming within the next couple of months anyways

[Ruben Van de Velde]

Riccardo Brasca said:

Ruben Van de Velde can we include your code in the flt-regular project? I think we need to tread the case n=3 separately (in exchange we will maintain it updated wrt to mathlib).

Yes, of course. I'd been hoping to find time to push it into mathlib, but that hasn't happened yet.

[Eric Rodriguez]

ok, turns out two is doable, although somehow we still have int algebra diamonds there... regardless, the example is there

[Eric Rodriguez]

There's also a lot of definitions that don't push forward or at least get preserved under equivalences that should - is_dedekind_domain is one

[Kevin Buzzard]

Someone here at ICERM is working on quadratic fields! I don't know if they're on the Zulip, I'll tell them about this thread. It might be a nice goal!

[Junyan Xu]

Kevin Buzzard said:

I had a student prove Z[omega] is a Euclidean domain and another student prove Z[sqrt(3)] is a Euclidean domain :-)

Any updates?

[Xavier Roblot]

The PR containing the main result is finally ready: #15143. I also PRed the opposite statement, that is root of unity are of norm 1: #16426.

I put the results in the number_field.lean file but I am wondering if it would be a good idea to make a number_field directory, move the first definitions and results to basic.lean, all the results about embeddings in their own file (I want to work on complex embeddings in the near future) and maybe even put the new result mem_roots_of_unity_of_norm_eq_one in a units.lean file since it is an important step in the proof of Dirichlet unit's theorem. There might be also results about number field, eg. finitude of class groups, that could be moved to this new directory.

[Riccardo Brasca]

I totally agree that number_field should be a directory sooner or later. But this is for another PR

[Kevin Buzzard]

Thanks Xavier! I think it's so cool that this stuff is getting done :-)

[Xavier Roblot]

I am having difficulty merging the project with the version of mem_roots_of_unity_of_abs_eq_one (now called number_field.embeddings.pow_eq_one_of_norm_eq_one) that is in mathlib. To reproduce the problem, merge with the latest version of mathlib and replace line 424 of number_theory/cyclotomic/Unit_lemmas.lean by

  have := @number_field.embeddings.pow_eq_one_of_norm_eq_one K _ _ ℂ _ _ _
    (u * (unit_gal_conj K p u)⁻¹ : K) _ _,

The error is maximum class-instance resolution depth has been reached. Looking at the log with the option trace.class_instances true, I see a lot of output involving ℝ with messages like: @normed_algebra ℝ ℝ real.normed_field.

[Xavier Roblot]

I am afraid, I don't know how to solve this kind of error...

[Eric Rodriguez]

can you push the code that causes the issue to a branch?

[Xavier Roblot]

I pushed to the branch origin/pow_eq_one_of_norm_eq_one (if I got my git commands right).

[Riccardo Brasca]

I am done for today, but I can have a look at tomorrow. Feel free to remove everything it is in mathlib, we will fix the problems.

[Eric Rodriguez]

oh, there seems to be some diamond issue again :(

[Eric Rodriguez]

but it's to do with complex not with any of our stuff..

[Eric Rodriguez]

oh, no, I'm wrong, something weirder is going on...

[Eric Rodriguez]

for now you can put haveI : normed_algebra ℚ ℂ := normed_algebra_rat, before your have := @... line and this will fxi it

[Eric Rodriguez]

I am not sure why the typeclass system is getting lost trying to find this lemma, though

[Eric Rodriguez]

oh, open_locale cyclotomic is at the top of the page, and doesn't seem to be needed

[Eric Rodriguez]

this is super cursed right now, if you remove it it should work fine

[Eric Rodriguez]

the file seems to compile without it

[Xavier Roblot]

Thanks to Eric, I was able to fix the problem and push the new version.

[Riccardo Brasca]

Thanks!