Embeddings

Stream: FLT-regular

[Chris Birkbeck]

So I moved some of the embedding stuff that was in the cyclotomic/absolute_value.lean file into its own file. I also had a stab at defining real and complex embeddings, its probably not very good, but we can state the unit lemma now.

[Alex J. Best]

I started trying to prove the unit lemma based on this.
Some design questions I am having trouble with:

• When defining a Galois automorphism of a number field is it best to define it as an aut of the field and have a good api for restricting to the ring of integers or unit group, or should we define galois automorphisms on the ring of integers and extend somehow, these should be equivalent, there are lemmas showing that alg homs preserve integrality like docs#is_integral_alg_hom so maybe thats enough.
• I'm having trouble with the 3 nested structures that are important here, the field itself, its ring of integers and the unit group (and also the roots of unity inside that even). With all these we have multiple coercions which then don't interact well with the algebraic structure always (e.g. if we pass from the unit group to the field then we can commute the inverse and the coercion, but as soon as we insert the ring of integers in between we lose the ability to talk about inverses in that ring so we lose the ability to commute coes and inverses.
• More simp lemmas are needed / we should think about which way we want simplifications to go to make the proofs nicer.

[Thomas Browning]

You could show in general that when you have an extension L/K, then K-algebra automorphisms of L restrict to various substructures (e.g., the integral closure in L of a subring of K).

[Johan Commelin]

Concerning •₁, maybe it's worth it to state lemmas for "compatible pairs of automorphisms" and then show that both the "restrict from field pair" and the "extend from ROI pair" are "compatible". That would give the most flexible API, I think.

[Johan Commelin]

Perhaps with a suitable predicate and dot-notation, it wouldn't even be very verbose to work with.

[Kevin Buzzard]

But one might need 4 choose 2 definitions?

[Johan Commelin]

I guess the alternative is that you pick one defn, develop the API in terms of that defn, and after 2500 lines of code you discover that the maths forces some of the other definitions on you as well. And then you get ugly proofs because the API doesn't apply smoothly.

[Chris Birkbeck]

So I don't really have any intuition as to what will lead to a better API, so I'll leave that to the experts. But related to the unit lemma. I realise now that maybe we don't need to have element_is_real in the statement and that its probably enough to use that its an element fixed by gal_conj p. I'll have a closer look at the proof to make sure this is the case. But it might make the proof a tad nicer (but probably doesn't help with the main issue of Galois acting on all of these structures).

[Kevin Buzzard]

Regarding the problem in general, we ran into this when doing stuff from Atiyah-MacDonald. An issue one will have is that if you try to use bundled subobjects then you run into the problem that the unit group is both a subgroup of the integer ring and the number field. In comm alg in the example I'm thinking of we just made everything into a type (ie in this case the unit group is a group not a subgroup) and we used is_scalar_tower to keep track of the (analogue of the) compatibilities units -> integer ring -> number field

[Kevin Buzzard]

(we had A subring B subring C but I'm extrapolating what worked for us)

[Kevin Buzzard]

Note that if you use the is_scalar_tower approach then the emphasis moves from the maps R -> K, U -> K etc to the actions of R on K, U on K etc, and you recover the maps by acting on 1: all the four objects in question (roots of unity, units, integers, field) have got a 1.

[Chris Birkbeck]

Alex J. Best said:

I started trying to prove the unit lemma based on this.
Some design questions I am having trouble with:

• When defining a Galois automorphism of a number field is it best to define it as an aut of the field and have a good api for restricting to the ring of integers or unit group, or should we define galois automorphisms on the ring of integers and extend somehow, these should be equivalent, there are lemmas showing that alg homs preserve integrality like docs#is_integral_alg_hom so maybe thats enough.
• I'm having trouble with the 3 nested structures that are important here, the field itself, its ring of integers and the unit group (and also the roots of unity inside that even). With all these we have multiple coercions which then don't interact well with the algebraic structure always (e.g. if we pass from the unit group to the field then we can commute the inverse and the coercion, but as soon as we insert the ring of integers in between we lose the ability to talk about inverses in that ring so we lose the ability to commute coes and inverses.
• More simp lemmas are needed / we should think about which way we want simplifications to go to make the proofs nicer.

I'm having trouble working on the number_theory/cyclotomic/rat.lean file. It seems to be using up all of my ram (and the same is happening on gitpod). I tried doing leanproject build (after doing get-mathlib-cache) or lean -- make my_file and also tried splitting some of the content into another file but its still not working. Any ideas on how to fix this?

[Riccardo Brasca]

I am not sure, but you can try to bisect the file to see where the the problem is

[Chris Birkbeck]

Hmm well its seems to magically be working now, so let me see if the problem comes back.

[Alex J. Best]

Splitting definitely seems helpful anyways, I started PRing a few basic lemmas from absolute value to mathlib so we can separate out the parts of these files that may need changing more easily

[Alex J. Best]

I think some of the stuff in rat was giving me issues too

[Riccardo Brasca]

@Chris Birkbeck I was looking at equiv_alg in number_theory/cyclotomic/number_field_embeddings (git blame says you wrote it). I think you can golf it, and probably save some time, using docs#ring_hom.to_rat_alg_hom and the results there.

[Chris Birkbeck]

Oh no I didn't write it, I just moved it there from Alex's stuff

[Chris Birkbeck]

Sorry I split things up, trying to keep it organised, but in the process may have made the PR attributions a pain!

[Chris Birkbeck]

That said, I'm happy to try and golf it :) But I won't able to do much today or tomorrow on this :(

[Riccardo Brasca]

Splitting files it's always a good thing :)

[Riccardo Brasca]

And it's impossible to keep track of who exactly did what, so I don't care

[Alex J. Best]

Those lemmas /defs look helpful yeah, I used library search to end up with the only nontrivial parts of that proof. Certainly that equiv is a good candidate for mathlib inclusion when suitably golfed and generalized

[Alex J. Best]

It does raise the question of whether we should use ring homs at all for embeddings or only algebra homs

[Alex J. Best]

Algebra homs seems to be the better way to go to me for the project to link up better with the Galois theory and maybe be more general?

[Riccardo Brasca]

For the general results I think we need alg_hom. A lot of them should generalize without effort to any fields tower $E/L/K$ with $E$ algebraically closed.

[Chris Birkbeck]

Alex J. Best said:

I think some of the stuff in rat was giving me issues too

So I split the unit lemma into a new file and it seems to not use up all of my ram now. I'm just playing around with this to see if some quick coe lemmas can at least prove more of it (before trying to do Kevin's suggestion of using scalar_towers which sounds a bit scary to me at the moment)

[Chris Birkbeck]

So I moved some of the embedding stuff that was in the cyclotomic/absolute_value.lean file into its own file. I also had a stab at defining real and complex embeddings, its probably not very good, but we can state the unit lemma now.

[Alex J. Best]

I started trying to prove the unit lemma based on this.
Some design questions I am having trouble with:

• When defining a Galois automorphism of a number field is it best to define it as an aut of the field and have a good api for restricting to the ring of integers or unit group, or should we define galois automorphisms on the ring of integers and extend somehow, these should be equivalent, there are lemmas showing that alg homs preserve integrality like docs#is_integral_alg_hom so maybe thats enough.
• I'm having trouble with the 3 nested structures that are important here, the field itself, its ring of integers and the unit group (and also the roots of unity inside that even). With all these we have multiple coercions which then don't interact well with the algebraic structure always (e.g. if we pass from the unit group to the field then we can commute the inverse and the coercion, but as soon as we insert the ring of integers in between we lose the ability to talk about inverses in that ring so we lose the ability to commute coes and inverses.
• More simp lemmas are needed / we should think about which way we want simplifications to go to make the proofs nicer.

[Thomas Browning]

You could show in general that when you have an extension L/K, then K-algebra automorphisms of L restrict to various substructures (e.g., the integral closure in L of a subring of K).

[Johan Commelin]

Concerning •₁, maybe it's worth it to state lemmas for "compatible pairs of automorphisms" and then show that both the "restrict from field pair" and the "extend from ROI pair" are "compatible". That would give the most flexible API, I think.

[Johan Commelin]

Perhaps with a suitable predicate and dot-notation, it wouldn't even be very verbose to work with.

[Kevin Buzzard]

But one might need 4 choose 2 definitions?

[Johan Commelin]

I guess the alternative is that you pick one defn, develop the API in terms of that defn, and after 2500 lines of code you discover that the maths forces some of the other definitions on you as well. And then you get ugly proofs because the API doesn't apply smoothly.

[Chris Birkbeck]

So I don't really have any intuition as to what will lead to a better API, so I'll leave that to the experts. But related to the unit lemma. I realise now that maybe we don't need to have element_is_real in the statement and that its probably enough to use that its an element fixed by gal_conj p. I'll have a closer look at the proof to make sure this is the case. But it might make the proof a tad nicer (but probably doesn't help with the main issue of Galois acting on all of these structures).

[Kevin Buzzard]

Regarding the problem in general, we ran into this when doing stuff from Atiyah-MacDonald. An issue one will have is that if you try to use bundled subobjects then you run into the problem that the unit group is both a subgroup of the integer ring and the number field. In comm alg in the example I'm thinking of we just made everything into a type (ie in this case the unit group is a group not a subgroup) and we used is_scalar_tower to keep track of the (analogue of the) compatibilities units -> integer ring -> number field

[Kevin Buzzard]

(we had A subring B subring C but I'm extrapolating what worked for us)

[Kevin Buzzard]

Note that if you use the is_scalar_tower approach then the emphasis moves from the maps R -> K, U -> K etc to the actions of R on K, U on K etc, and you recover the maps by acting on 1: all the four objects in question (roots of unity, units, integers, field) have got a 1.

[Chris Birkbeck]

Alex J. Best said:

I started trying to prove the unit lemma based on this.
Some design questions I am having trouble with:

• When defining a Galois automorphism of a number field is it best to define it as an aut of the field and have a good api for restricting to the ring of integers or unit group, or should we define galois automorphisms on the ring of integers and extend somehow, these should be equivalent, there are lemmas showing that alg homs preserve integrality like docs#is_integral_alg_hom so maybe thats enough.
• I'm having trouble with the 3 nested structures that are important here, the field itself, its ring of integers and the unit group (and also the roots of unity inside that even). With all these we have multiple coercions which then don't interact well with the algebraic structure always (e.g. if we pass from the unit group to the field then we can commute the inverse and the coercion, but as soon as we insert the ring of integers in between we lose the ability to talk about inverses in that ring so we lose the ability to commute coes and inverses.
• More simp lemmas are needed / we should think about which way we want simplifications to go to make the proofs nicer.

I'm having trouble working on the number_theory/cyclotomic/rat.lean file. It seems to be using up all of my ram (and the same is happening on gitpod). I tried doing leanproject build (after doing get-mathlib-cache) or lean -- make my_file and also tried splitting some of the content into another file but its still not working. Any ideas on how to fix this?

[Riccardo Brasca]

I am not sure, but you can try to bisect the file to see where the the problem is

[Chris Birkbeck]

Hmm well its seems to magically be working now, so let me see if the problem comes back.

[Alex J. Best]

Splitting definitely seems helpful anyways, I started PRing a few basic lemmas from absolute value to mathlib so we can separate out the parts of these files that may need changing more easily

[Alex J. Best]

I think some of the stuff in rat was giving me issues too

[Riccardo Brasca]

@Chris Birkbeck I was looking at equiv_alg in number_theory/cyclotomic/number_field_embeddings (git blame says you wrote it). I think you can golf it, and probably save some time, using docs#ring_hom.to_rat_alg_hom and the results there.

[Chris Birkbeck]

Oh no I didn't write it, I just moved it there from Alex's stuff

[Chris Birkbeck]

Sorry I split things up, trying to keep it organised, but in the process may have made the PR attributions a pain!

[Chris Birkbeck]

That said, I'm happy to try and golf it :) But I won't able to do much today or tomorrow on this :(

[Riccardo Brasca]

Splitting files it's always a good thing :)

[Riccardo Brasca]

And it's impossible to keep track of who exactly did what, so I don't care

[Alex J. Best]

Those lemmas /defs look helpful yeah, I used library search to end up with the only nontrivial parts of that proof. Certainly that equiv is a good candidate for mathlib inclusion when suitably golfed and generalized

[Alex J. Best]

It does raise the question of whether we should use ring homs at all for embeddings or only algebra homs

[Alex J. Best]

Algebra homs seems to be the better way to go to me for the project to link up better with the Galois theory and maybe be more general?

[Riccardo Brasca]

For the general results I think we need alg_hom. A lot of them should generalize without effort to any fields tower $E/L/K$ with $E$ algebraically closed.

[Chris Birkbeck]

Alex J. Best said:

I think some of the stuff in rat was giving me issues too

So I split the unit lemma into a new file and it seems to not use up all of my ram now. I'm just playing around with this to see if some quick coe lemmas can at least prove more of it (before trying to do Kevin's suggestion of using scalar_towers which sounds a bit scary to me at the moment)