Kronecker

Stream: FLT-regular

[Alex J. Best]

Today I worked on the theorem of Kronecker that an algebraic integer with all conjugates having absolute value one is a root of unity (3.3 in the blueprint, or lemma 1.6 in Washington's book). The file is https://github.com/leanprover-community/flt-regular/blob/master/src/number_theory/cyclotomic/absolute_value.lean . It needs a lot of cleanup and most of the lemmas moving to mathlib (or at least to to_mathlib) but it is almost proved.
There is one remaining issue that I haven't worked out the best way around yet (the two sorries in that file), we need to factor the minpoly of our integral element t in K into the product of x - phi t over embeddings phi of the field K into C, this works on the nose if t generates K, but if it lies in a smaller subfield there will be multiple embeddings for each root of the minpoly in C. One approach is to teach lean that ℚ⟮x⟯ viewed as a type rather than an intermediate field is a number field which seems good, and then apply some of the lemmas to that field rather than K when trying to prove the result for K. The other would be to accept that the product of the embeddings will be a power of the minimal polynomial and factor that into the argument.
I think its most natural to try and remove the ambient number field where possible, as hopefully that will make the lemma more applicable, but maybe we should wait and see how https://leanprover-community.github.io/flt-regular/sect0003.html#lemma:_unit_lemma looks first.

[Chris Birkbeck]

Oh wow this looks really good! We might have enough there to prove the primitive element theorem as well (which I couldn't find in mathlib).

[Chris Birkbeck]

I'm happy to help clean this up, but you guys are much faster than I am, so I don't want to disturb the files you are working on. I was planning on stating some more of the FLT_facts results today. But if you aren't working on these files later, I can try and extract all of the embedding stuff into a separate file and see about this unit_lemma.

[Alex J. Best]

Feel free to disturb it! I think I stared at lean a little bit too much yesterday so I don't think I'll be doing any today :smiley:

[Riccardo Brasca]

That's great Alex!

[Riccardo Brasca]

It's probably a good idea to ask in the math stream.

[Riccardo Brasca]

The primitive element theorem is in field_theory.primitive_element

[Chris Birkbeck]

oh what? I thought I'd searched for it and nothing came up. I must've made a typo.

[Riccardo Brasca]

docs#field.exists_primitive_element

[Riccardo Brasca]

The formulation in docs#field.power_basis_of_finite_of_separable is probably better for working with the trace

[Chris Birkbeck]

Yeah I found it now. I don't know what happened the first time I searched for it :P

[Riccardo Brasca]

Concerning Alex's original question, for the minimal polynomial, I think the best approach is to fix a docs#power_basis of the larger field, rather than an element. In this way everything should work smoothly, and a lot of mathlib's results are stated using powerbasis.

[Alex J. Best]

Today I worked on the theorem of Kronecker that an algebraic integer with all conjugates having absolute value one is a root of unity (3.3 in the blueprint, or lemma 1.6 in Washington's book). The file is https://github.com/leanprover-community/flt-regular/blob/master/src/number_theory/cyclotomic/absolute_value.lean . It needs a lot of cleanup and most of the lemmas moving to mathlib (or at least to to_mathlib) but it is almost proved.
There is one remaining issue that I haven't worked out the best way around yet (the two sorries in that file), we need to factor the minpoly of our integral element t in K into the product of x - phi t over embeddings phi of the field K into C, this works on the nose if t generates K, but if it lies in a smaller subfield there will be multiple embeddings for each root of the minpoly in C. One approach is to teach lean that ℚ⟮x⟯ viewed as a type rather than an intermediate field is a number field which seems good, and then apply some of the lemmas to that field rather than K when trying to prove the result for K. The other would be to accept that the product of the embeddings will be a power of the minimal polynomial and factor that into the argument.
I think its most natural to try and remove the ambient number field where possible, as hopefully that will make the lemma more applicable, but maybe we should wait and see how https://leanprover-community.github.io/flt-regular/sect0003.html#lemma:_unit_lemma looks first.

[Chris Birkbeck]

Oh wow this looks really good! We might have enough there to prove the primitive element theorem as well (which I couldn't find in mathlib).

[Chris Birkbeck]

I'm happy to help clean this up, but you guys are much faster than I am, so I don't want to disturb the files you are working on. I was planning on stating some more of the FLT_facts results today. But if you aren't working on these files later, I can try and extract all of the embedding stuff into a separate file and see about this unit_lemma.

[Alex J. Best]

Feel free to disturb it! I think I stared at lean a little bit too much yesterday so I don't think I'll be doing any today :smiley:

[Riccardo Brasca]

That's great Alex!

[Riccardo Brasca]

It's probably a good idea to ask in the math stream.

[Riccardo Brasca]

The primitive element theorem is in field_theory.primitive_element

[Chris Birkbeck]

oh what? I thought I'd searched for it and nothing came up. I must've made a typo.

[Riccardo Brasca]

docs#field.exists_primitive_element

[Riccardo Brasca]

The formulation in docs#field.power_basis_of_finite_of_separable is probably better for working with the trace

[Chris Birkbeck]

Yeah I found it now. I don't know what happened the first time I searched for it :P

[Riccardo Brasca]

Concerning Alex's original question, for the minimal polynomial, I think the best approach is to fix a docs#power_basis of the larger field, rather than an element. In this way everything should work smoothly, and a lot of mathlib's results are stated using powerbasis.