Contributing to the project

Stream: FLT-regular

[Xavier Roblot]

Hi, I am Xavier Roblot. I am a number theorist in Lyon (and thus a colleague of @Filippo A. E. Nuccio who introduced me to Lean). I saw @Riccardo Brasca's talk about this project at the "Lean in Lyon" workshop and I would really like to contribute if I can. I have been learning to work with Lean during the last few weeks and I am still very far for being proficient with it, but I hope I can be of some help.

[Riccardo Brasca]

Hi Xavier! Thanks for your message, and welcome to the Lean community!
I was very busy recently, so I have to sit down and think about a reasonable plan for the next weeks, but I will try to do as soon as possible.

[Riccardo Brasca]

You can have a look at our blueprint. The links are not updated, but essentially everything in section 2 is in mathlib

[Riccardo Brasca]

3.1 and 3.2 are also done

[Riccardo Brasca]

We have to think a little bit about 3.3, even to state it

[Chris Birkbeck]

We have some stuff for 3.3 but it still needs some annoying lemmas

[Riccardo Brasca]

But I would say that lemmas 3.3-3.7 are more or less what we should concentrate now

[Chris Birkbeck]

Ive also been very bad at updating links on the blueprint. I'll try and do that tomorrow

[Riccardo Brasca]

@Xavier Roblot if you want to have a look at the project just use leanproject get flt-regular, but a lot of results are already in mathlib, in the number_theory/cyclotomic folder.

[Xavier Roblot]

Actually, I have been working on some version of 3.3 in the last few days as a pet project. But I am very far from a complete proof . Basically, I just (almost) proved so far that bounded roots give bounded coefficients, that might be already in mathlib... (Sorry posted in the wrong streams)

[Xavier Roblot]

I have downloaded the project. I'll have a closer look tomorrow.

[Riccardo Brasca]

What is you github username?

[Chris Birkbeck]

I've been slowly working on 3.4 in the unit_lemmas.lean file, but we need some more facts about totient functions which could also be a fun place to start

[Xavier Roblot]

My GitHub username is xroblot

[Riccardo Brasca]

I've sent you an invitation to the project. Feel free to push all sort of code to master, but try to avoid errors (sorry is of course totally fine).

[Riccardo Brasca]

Let me know if you are also interested in contributing to mathlib

[Alex J. Best]

I thought that I did bounded roots gives bounded coeffs, and that all roots abs val one implies root of unity in the project a while ago, but I'm not sure now, I'll try and find it later.

[Chris Birkbeck]

Yeah you did, it's somewhere in the repo

[Eric Rodriguez]

I always saw that stuff and got a bit worried because it looked dissimilar to the galois stuff I did but it's probably likely I did stuff wrong

[Filippo A. E. Nuccio]

Hi Xavier, I am happy to see you here. Welcome! I am sure that @Riccardo Brasca will have a lot of things to pass over to you, you won't be left without work :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

Hi Xavier!

[Chris Birkbeck]

Alex J. Best said:

I thought that I did bounded roots gives bounded coeffs, and that all roots abs val one implies root of unity in the project a while ago, but I'm not sure now, I'll try and find it later.

its mem_roots_of_unity_of_abs_eq_one which is in number_theory/cyclotomic/absolute_value.lean

[Riccardo Brasca]

I've missed this one, nice!! Killing the two remaining sorry in that file would be very nice

[Riccardo Brasca]

One has the rather scary comment

-- this goal isn't true as stated right now, the rhs could be a power of the lhs

:sweat_smile:

[Riccardo Brasca]

Is someone interested in finishing this? I think it's a nice piece of math, and it definitely deserves to be put in mathlib.

[Chris Birkbeck]

By this do you mean lemma 3.3 from the blueprint? i.e mem_roots_of_unity_of_abs_eq_one?

[Riccardo Brasca]

Yes, sorry

[Xavier Roblot]

I guess I can try to finish it if @Alex J. Best does not want to finish it himself. However, it will probably take me some time and I might need some help along the way :sweat_smile:

[Riccardo Brasca]

If you need some advice just ask!

[Alex J. Best]

I'm happy to help you help me! It's not so much that I don't want to finish it, just that I have a stack of other half finished Lean projects, and only so much time to devote to them. Its a very cool theorem and I definitely agree it belongs in mathlib, so if you'd like to finish it off that's great, thanks @Xavier Roblot. I'm happy to try and explain any of the choices I made, or things that I think can be improved from what I originally wrote.

[Xavier Roblot]

Ok, thanks for the answers. I'll try to finish it and I'll come back to you guys if I need help.

[Riccardo Brasca]

Something we also want is Lemma 3.7 in the blueprint. It shouldn't be difficult is anyone wants to try (I didn't check, it can somehow be already in mathlib).

[Ruben Van de Velde]

Not sure if this is the cleanest approach, and not sure it's true for b=0, but:

variables {α : Type*} [comm_ring α] [is_domain α] [is_dedekind_domain α]

example (p : nat) (a b c : ideal α) (cp : is_coprime a b) (h : a*b = c^p) (hb : b ≠ 0) :
  ∃ d : ideal α, a = d ^ p :=
begin
  classical,
  obtain rfl|ha := eq_or_ne a 0,
  { use 0, apply (zero_pow _).symm, contrapose! h,
    rw le_zero_iff at h, rw [h, pow_zero, zero_mul], exact zero_ne_one },
  let fa := unique_factorization_monoid.normalized_factors a,
  let fb := unique_factorization_monoid.normalized_factors b,
  let fc := unique_factorization_monoid.normalized_factors c,
  have : ∀ d ∈ fa, d ∉ fb,
  { intros d ha hb,
    have := unique_factorization_monoid.irreducible_of_normalized_factor _ ha,
    apply irreducible.not_unit this,
    apply is_coprime.is_unit_of_dvd' cp;
    apply unique_factorization_monoid.dvd_of_mem_normalized_factors;
    assumption },
  suffices : ∃ f : multiset (ideal α), fa = p • f,
  { obtain ⟨f, hf⟩ := this,
    refine ⟨f.prod, _⟩ ,
    have := unique_factorization_monoid.normalized_factors_prod ha,
    rw associated_eq_eq at this,
    rw [←this, ←multiset.prod_nsmul, ←hf] },
  refine multiset.exists_smul_of_dvd_count _ (λ x hx, _),
  have hxb := this x hx,
  convert dvd_mul_right p (fc.count x),
  rw [←multiset.count_nsmul, ←unique_factorization_monoid.normalized_factors_pow, ←h,
    unique_factorization_monoid.normalized_factors_mul ha hb],
  rw multiset.count_add,
  convert (add_zero _).symm,
  apply multiset.count_eq_zero_of_not_mem hxb,
end

[Riccardo Brasca]

Very nice! Would you mind to push it to master in the flt-regular repository? You can create a new file in the ready_for_mathlib folder

[Riccardo Brasca]

And of course if you want to PR it you're welcome!

[Riccardo Brasca]

I've sent you an invitation

[Ruben Van de Velde]

I'm not sure I have all the right imports, so I made a pr: https://github.com/leanprover-community/flt-regular/pull/61

[Ruben Van de Velde]

Need to check where it goes wrong for plain ufds instead of ideals of Dedekind domains, though

[Riccardo Brasca]

For the project if it compiles then it's OK for master :)

[Eric Rodriguez]

this is symmetric in a+b, right? so it should work for b=0? especially as you don't use hb in the subproof

[Eric Rodriguez]

oh, I see that as usual my reading abilities drop to zero when I'm reading other people's code

[Eric Rodriguez]

thankfully the statement is true for b zero, proof pushed

[Riccardo Brasca]

You're faster than me!

[Eric Rodriguez]

I generalised is_unit_iff' to comm_semirings, because of what Ruben said about ufds, but not sure how this could hold in UFDs; are UFDs' ideals atomic?

[Riccardo Brasca]

I wouldn't care about UFD, and it wouldn't be a generalization

[Riccardo Brasca]

Most Dedekind domains are not UFD

[Eric Rodriguez]

Right, fair, no big deal then

[Riccardo Brasca]

Of course for UFD the corresponding relevant statement is about elements, and it should be easy

[Alex J. Best]

Well I guess the generalization would be to unique factorization monoids rather than ideals of Dedekind domains

[Riccardo Brasca]

The trick for b=0 won't work in general I think (since there can be units that are not p-powers), but the rest should be the same.

[Ruben Van de Velde]

I've got some pretty awful code up at https://gist.github.com/Ruben-VandeVelde/d82c653a8cc2315a3985e60ed4637346 - might try to make something of it later

[Ruben Van de Velde]

Sorry-free at least, but still hairy

[Riccardo Brasca]

Feel free to push it to flt-regular if you want, don't worry about names and similar stuff (and in exchange someone will fix any problem arising from mathlib bumps).

[Xavier Roblot]

I am sorry but I am making very slow progress. I have a lot of difficulties figuring out even very easy things. For example, I have a number_field K, number_field L and algebra K L. So I should be able to see K as having type intermediate_fields ℚ L, but I cannot just figure out how to say to Lean to do that. Any help would be very welcome.

[Ruben Van de Velde]

Ruben Van de Velde said:

I've got some pretty awful code up at https://gist.github.com/Ruben-VandeVelde/d82c653a8cc2315a3985e60ed4637346 - might try to make something of it later

In the end it turns out my generalization wasn't quite a generalization: I required comm_ring and ideals of Dedekind domains seem to only be a comm_semiring. Maybe https://github.com/leanprover-community/mathlib/pull/14423 will help, we'll see. Got some interesting lemmas out of it, in any case

[Kevin Buzzard]

Xavier Roblot said:

I am sorry but I am making very slow progress. I have a lot of difficulties figuring out even very easy things. For example, I have a number_field K, number_field L and algebra K L. So I should be able to see K as having type intermediate_fields ℚ L, but I cannot just figure out how to say to Lean to do that. Any help would be very welcome.

@Xavier Roblot a more effective way to ask questions is to give a #mwe , for example

import number_theory.number_field

variables (K L : Type) [field K] [number_field K] [field L] [number_field L]
[algebra K L]

example : intermediate_field ℚ L := sorry

That way I don't have to figure out imports myself or start guessing that you probably mean intermediate_field not intermediate_fields.

Here's a partial solution:

import number_theory.number_field

variables (K L : Type) [field K] [number_field K] [field L] [number_field L]
[algebra K L]

-- To make an intermediate field you need to give
-- (1) the subset, (called `carrier`)
-- (2) a proof that the subset contains ℚ, (called `algebra_map_mem'`)
-- (3) a proof of all the axioms for a subfield.

example : intermediate_field ℚ L :=
  -- The subset is the image of the canonical map K → L
{ carrier := set.range (algebra_map K L),
    -- this is a fairly incomprehensible proof
    -- that the image of the map from K to L
    -- must contain the image of the rationals.
  algebra_map_mem' := λ r, ⟨r, begin
    rw [map_rat_cast],
    convert (map_rat_cast (algebra_map ℚ L) r).symm,
    exact congr_arg _ r.cast_id.symm,
  end⟩,
  -- A ring homomorphism maps 0 to 0 so
  -- 0 is in the subset
  zero_mem' := ⟨0, map_zero _⟩,
  -- Same story for 1; `map_one` says a ring hom maps
  -- 1 to 1.
  one_mem' := ⟨1, map_one _⟩,
  -- This next begin/end block is a proof that the product
  -- of two things in the subset is in the subset. It uses
  -- the theorem that ring homomorphisms commute with
  -- multiplication, which is called `map_mul`.
  -- It also uses the `rintro rfl` trick.
  mul_mem' := begin
    rintro - - ⟨s, rfl⟩ ⟨t, rfl⟩,
    exact ⟨s * t, map_mul _ _ _⟩,
  end,
  -- Exercise for the reader.
  add_mem' := begin sorry end,
  neg_mem' := begin sorry end,
  inv_mem' := begin sorry end,
  }

[Xavier Roblot]

Kevin, thanks (again) for helping me. Sorry about the lack of #mwe. I'll remember to add one next time.
Somehow, I thought there was a quick way to solve the problem, but I see that one has to construct the intermediate_field from the definition... Anyway, back to work

[Riccardo Brasca]

In your example K is not literally an intermediate_field (this is false even mathematically, K is not a subset of L. Of course there is the image, but still...). The best question is probably why you want an intermediate field.

[Riccardo Brasca]

Ruben Van de Velde said:

Ruben Van de Velde said:

I've got some pretty awful code up at https://gist.github.com/Ruben-VandeVelde/d82c653a8cc2315a3985e60ed4637346 - might try to make something of it later

In the end it turns out my generalization wasn't quite a generalization: I required comm_ring and ideals of Dedekind domains seem to only be a comm_semiring. Maybe https://github.com/leanprover-community/mathlib/pull/14423 will help, we'll see. Got some interesting lemmas out of it, in any case

This

variables {β : Type*} [comm_ring β] [is_domain β] [unique_factorization_monoid β]

lemma exists_associated_pow_of_mul_eq_pow (p : nat) (a b c : β) (cp : is_coprime a b) (h : a*b = c^p) (hb : b ≠ 0) :
  ∃ d : β, associated a (d ^ p) :=

looks a good generalization, ideals of a Dedekind domain are a unique_factorization_monoid, and in this case associated means equal (do we have this lemma?).

[Yaël Dillies]

docs#associated_iff_eq ?

[Yaël Dillies]

Sorry, you accidentally triggered yael_search!

[Riccardo Brasca]

Yes, that's probably it (I am still having my coffee, to early on Saturday morning to check if we have unique...)

[Riccardo Brasca]

Riccardo Brasca said:

Ruben Van de Velde said:

Ruben Van de Velde said:

I've got some pretty awful code up at https://gist.github.com/Ruben-VandeVelde/d82c653a8cc2315a3985e60ed4637346 - might try to make something of it later

In the end it turns out my generalization wasn't quite a generalization: I required comm_ring and ideals of Dedekind domains seem to only be a comm_semiring. Maybe https://github.com/leanprover-community/mathlib/pull/14423 will help, we'll see. Got some interesting lemmas out of it, in any case

This

variables {β : Type*} [comm_ring β] [is_domain β] [unique_factorization_monoid β]

lemma exists_associated_pow_of_mul_eq_pow (p : nat) (a b c : β) (cp : is_coprime a b) (h : a*b = c^p) (hb : b ≠ 0) :
  ∃ d : β, associated a (d ^ p) :=

looks a good generalization, ideals of a Dedekind domain are a unique_factorization_monoid, and in this case associated means equal (do we have this lemma?).

Ah, you have variables {β : Type*} [comm_ring β] [is_domain β] [unique_factorization_monoid β], that's too much! β should only be a monoid.

[Riccardo Brasca]

I see is_coprime is defined via Bezout, so it wants a semiring.

[Riccardo Brasca]

I've asked a related question here

[Xavier Roblot]

Riccardo Brasca said:

In your example K is not literally an intermediate_field (this is false even mathematically, K is not a subset of L. Of course there is the image, but still...). The best question is probably why you want an intermediate field.

I need to prove that any embedding $K \to \mathbb{C}$ can be lifted to an embedding $L \to \mathbb{C}$. This should follow from the intermediate_field.lifts machinery using the primitive element theorem.

[Riccardo Brasca]

We have docs#is_alg_closed.lift

[Riccardo Brasca]

In general it is a little tricky to decide if one wants to work with substuff of not. substuff has the advantage that you can literally prove that two things are equal by ext, you can take intersections and so on. But usually at some point you discover that something is not literally a subset and then you regret your choice. I suggest to try to avoid it if possible.

[Xavier Roblot]

Riccardo, thanks for the advice. I wished I found out about is_alg_closed.lift sooner. I guess I am still not skilled enough at searching the library :sweat_smile:

[Riccardo Brasca]

I found it as follows: the reason why this is true is that C is algebraically closed, and I randomly tried is_alg_closed.lift. I would have been very surprised if we had it only for intermediate_field.

[Kevin Buzzard]

@Xavier Roblot there could well be an easier way -- it wouldn't surprise me if for a large class of morphisms (group homomorphisms, ring homomorphisms etc) there's a function already there which gives the construction of an image subobject. I was too lazy to look for it.

[Xavier Roblot]

Kevin Buzzard said:

Xavier Roblot there could well be an easier way -- it wouldn't surprise me if for a large class of morphisms (group homomorphisms, ring homomorphisms etc) there's a function already there which gives the construction of an image subobject. I was too lazy to look for it.

Well, I was able to get a nice short proof with is_alg_closed.lift so I am happy with that.

[Kevin Buzzard]

By the way I totally agree that as a relative newcomer it's very hard to guess what the best way of implementing the data of a question should be. The Artin-Tate lemma (according to Atiyah--Macdonald, at least) is a statement involving three commutative rings $A\subseteq B\subseteq C$ and in the proof you build a 4th ring $B\subseteq D\subseteq C$. Are you supposed to let $A,B,C$ be types and give them [ring] instances, or should $C$ be the ring (the type) and $A$ and $B$ be subrings, or should $B$ be the ring, $A$ a subring and $C$ a $B$-algebra? Then all the same questions for $D$. Questions like this are rather delicate. In the old days your decisions would be influenced by questions such as "do we have more API for subring or algebra" but nowadays we have lots of API for both so in some sense it's probably true that whatever decision you make, you'll be able to get the proof out in the end. But bad design decisions might mean that constructing the proof is painful. In the case of the Artin-Tate lemma we eventually let all the rings be types and used algebra to glue everything together, and also is_scalar_tower (this is a statement that a triangle commutes).

[Riccardo Brasca]

I noticed we need

lemma totient_super_multiplicative (a b : ℕ) : a.totient * b.totient ≤ (a * b).totient

this should be easy and it can go directly to mathlib. So if someone is looking for a place to start this looks like a nice small lemma.

[Chris Birkbeck]

Riccardo Brasca said:

I noticed we need

lemma totient_super_multiplicative (a b : ℕ) : a.totient * b.totient ≤ (a * b).totient

this should be easy and it can go directly to mathlib. So if someone is looking for a place to start this looks like a nice small lemma.

I'm actually working on this now. Actually, I'm proving that totient is is_gcd_mult (which is a made up name)

[Chris Birkbeck]

We also need

lemma contains_two_primitive_roots (p q : ℕ)
(x y : K) (hx : is_primitive_root x p) (hy : is_primitive_root y q): (lcm p q ).totient ≤
(finite_dimensional.finrank ℚ K) :=

But this might be harder/more annoying

[Eric Rodriguez]

can't we just create the explicit element of order ф(lcm p q) and then that gives us a bound on the finrank?

[Eric Rodriguez]

not order... my words are vanishing in my head

[Eric Rodriguez]

I think we have that K + a primitive root is a cyclotomic extension somewhere

[Chris Birkbeck]

Eric Rodriguez said:

can't we just create the explicit element of order ф(lcm p q) and then that gives us a bound on the finrank?

Yeah thats the idea. I guess I don't know how easy it is at the moment to go from knowing we have some root of unity in the field, to giving a lower bound on the degree.

[Chris Birkbeck]

But I've not yet looked into the API for this, so maybe its easy

[Eric Rodriguez]

docs#is_cyclotomic_extension.finrank, docs#is_primitive_root.adjoin_is_cyclotomic_extension

[Eric Rodriguez]

I think we don't have that if A C S is a cycl extension, and A B K is one, then B C (S / K) is but maybe that follows from something like is_cyclotomic_extension.trans

[Eric Rodriguez]

and also I don't think we can turn for example is_cycl_ext A B {p, q} into is_cycl_ext A B {lcm p q} or for a nice challenge is_cycl_ext A B S to is_cycl_extension A B {S.lcm id}

[Chris Birkbeck]

Riccardo Brasca said:

I noticed we need

lemma totient_super_multiplicative (a b : ℕ) : a.totient * b.totient ≤ (a * b).totient

this should be easy and it can go directly to mathlib. So if someone is looking for a place to start this looks like a nice small lemma.

Alright, this is done, but its still a mess. I'll golf and look to PR it next week.

[Riccardo Brasca]

I've made some progress in contains_two_primitive_roots. It's quite annoying, but I've constructed an element of order lcm p q (modulo the fact that the order doesn't change under a coercion, this is an independent result that I don't find). I will not work on this for a couple of days, if someone wants to finish from here no problems.

[Riccardo Brasca]

The two sorry about the order are done.

[Riccardo Brasca]

I guess we need to generalize docs#is_cyclotomic_extension.finrank to the case L is domain. It should be very easy.

[Eric Rodriguez]

I'm not sure how easy that is with the current proof

[Riccardo Brasca]

I think there is simply nothing to do. Note that I don't want to generalize the base ring, just the big one.

[Riccardo Brasca]

I've tested docs#is_primitive_root.power_basis and it's OK

[Riccardo Brasca]

I mean like in #14550. I have to stop now, but docs#is_cyclotomic_extension.finrank is OK in that PR. Something broke later, but I think it is just because C is implicit/explicit or something similar. If you have time and want to finish it feel free to work on it :grinning_face_with_smiling_eyes:

[Eric Rodriguez]

I'll have a try when I get to the airport and have some time :)

[Riccardo Brasca]

I am officially late for my lunch, but it should work now.

[Riccardo Brasca]

I didn't touch docs#is_primitive_root.embeddings_equiv_primitive_roots (because I am lazy) but it should be generalizable too.

[Eric Rodriguez]

sorry, I had a hectic while, I think I should've fixed it now

[Eric Rodriguez]

I wonder if this is a Lean change more than anything, I assume that if you have a cycl extension over a field (apart from the fact that unit is the {}th cyclotomic extension) then we have that it is also a field though

[Eric Rodriguez]

but if it helps it helps!

[Eric Rodriguez]

if anyone is reading this stream, reviews on #14463 would be good! (this is another one, changing the defn of is_cyclotomic_extension)

[Xavier Roblot]

I have finished the proof of lemma 3.3: mem_roots_of_unity_of_abs_eq_one. I am going to take a few days to polish and clean the proof, but I should have something ready soon. What should I do when it's ready? should I just do a git push origin of my local branch?

[Ruben Van de Velde]

Yeah - though feel free to push your branch before polishing as well

[Riccardo Brasca]

Eric Rodriguez said:

I wonder if this is a Lean change more than anything, I assume that if you have a cycl extension over a field (apart from the fact that unit is the {}th cyclotomic extension) then we have that it is also a field though

Yes, a domain that is a finite extension of a field is a field (multiplication by an element is injective, hence surjective). I guess this is somewhere with is_field.

[Eric Rodriguez]

I guess this doesn't hold for something like {3,9,27,...} though, although maybe it holds for deeper reasons

[Riccardo Brasca]

It holds (assuming it is a domain, I don't know whether this is automatic): take x in the extension. It is algebraic, so the subextension generated by it it's finite and so it contains an inverse of x.

[Riccardo Brasca]

docs#is_integral.is_field_iff_is_field

[Xavier Roblot]

Well, I pushed my changes to the project. I hope I didn't break anything...

[Eric Rodriguez]

Riccardo Brasca said:

docs#is_integral.is_field_iff_is_field

indeed, right below integral, this works:

lemma is_field (C) [comm_ring C] [is_domain C] [algebra K C] [fintype S]
  [is_cyclotomic_extension S K C] : is_field C :=
(is_integral.is_field_iff_is_field (integral S K C) $ (algebra_map K C).injective).mp $
  field.to_is_field K

I'll PR a fix to dot notation on that lemma, and when I get some actual time I'll try extend the proof to non-finite S for fun

[Eric Rodriguez]

I'll have a look at why your thing isn't building, Xavier! seems to just be a small namespace thing so apart from that it looks good

[Riccardo Brasca]

Thanks for working on #14550! Do you think it is ready for review?

[Eric Rodriguez]

oh, it compiled! yes, it is :)

[Riccardo Brasca]

Xavier Roblot said:

I have finished the proof of lemma 3.3: mem_roots_of_unity_of_abs_eq_one. I am going to take a few days to polish and clean the proof, but I should have something ready soon. What should I do when it's ready? should I just do a git push origin of my local branch?

I've missed this message, great job!

[Xavier Roblot]

Thanks. But now I am hooked :sweat_smile: Is there any thing else I can work on?

[Riccardo Brasca]

Well, following the philosophy of the project I think you should PR this!

[Kevin Buzzard]

Do you have a roadmap for this project or some kind of plan? I'm hard at work with LTE now but when it's done I'd like to join the Fermat project too.

[Eric Rodriguez]

https://leanprover-community.github.io/flt-regular/

[Riccardo Brasca]

We are almost ready to attack case I, right? I will check this tomorrow

[Riccardo Brasca]

I think the next boss is the unit lemma. We have a draft version here but we should probably refactor some definition/results. I have time now to produce a reasonable statement.

[Chris Birkbeck]

Yeah I agree. One think to fix is the Galois action on these things. I think at the moment it's probably a bit to hacky

[Riccardo Brasca]

Do we have somewhere that the conjugate of a complex number of norm 1 is its inverse? It should be easy anyway

[Riccardo Brasca]

it is essentially docs#complex.norm_sq_eq_conj_mul_self

[Riccardo Brasca]

So I propose to redefine is_gal_conj_real in terms of the Galois group, connect it with ℝ in some way, and prove the unit lemma using this new "is real" notion.

[Chris Birkbeck]

Do we need to connect it to ℝ? If I remember correctly the proofs only ever use that things are fixed by complex conjugation.

[Riccardo Brasca]

Probably not, but it seems a reasonable thing to have. And it should be a couple of lines

[Chris Birkbeck]

Fair enough, I thought linking things to ℝ would make things more annoying because of extra coe maps. But maybe this is fine/you have something else in mind

[Riccardo Brasca]

I am not saying we should use ℝ anywhere in the project. Just the fact that is_gal_conj_real x is equivalent to x ∈ ℝ (strictly speaking this doesn't make sense), but this is useful only to explain what is_gal_conj_real x means, not to actually work with it.

[Chris Birkbeck]

Oh ok I get you! Yes then I agree

[Riccardo Brasca]

I mean, if I see this in a PR I would immediately ask for it, even if mathematically it's not needed.

[Xavier Roblot]

Riccardo Brasca said:

Well, following the philosophy of the project I think you should PR this!

Ok. Can you please give me access to push to mathlib?
Also, there are some choices that need to be discussed. I'll create a new thread for that.

[Riccardo Brasca]

You should have an invitation

[Xavier Roblot]

Got it. Thanks!

[Riccardo Brasca]

Having a PR accepted can be a little frustrating, so don't be afraid of asking questions, and be patient :grinning:

[Riccardo Brasca]

Thanks to #14550 contains_two_primitive_roots is now proved. I am not sure I have time today, but we need a small refactor of number_theory/cyclotomic/Unit_lemmas, replacing KK by a generic cyclotomic extension.

[Riccardo Brasca]

@Xavier Roblot do you mind moving the material you PRed to the ready_for_mathlib folder? Just to keep track of what we are adding to mathlib. (And I will have a look at you PR today)

[Xavier Roblot]

I moved the things already PRed in a previous commit named PR #14749. I am still working on the other PRs.

Thanks for the taking the time to look at my PR!

[Riccardo Brasca]

I've added a "From flt-regular" at the end of the description of the PR.

[Riccardo Brasca]

I've also left a couple of comments. I think a lot of the results you prove in your specific case are already somewhere in mathlib (in greater generality). It can be tricky to find them, but don't hesitate to ask here!

[Riccardo Brasca]

There is unit_inv_conj_not_neg_zeta_runity in src/number_theory/cyclotomic/Unit_lemmas.lean that is the last sorry in the file. If someone wants to try it please go ahead.

[Eric Rodriguez]

is docs#smodeq the correct way to talk about things being equal up to an ideal?

[Eric Rodriguez]

I don't really want to develop new API unless necessary but I know some people don't like the ideal/submodule R R defeq too much

[Riccardo Brasca]

Mathematically I would just work in the quotient, in mathlib I am not sure.

[Eric Rodriguez]

We don't actually have that docs#is_primitive_root.power_basis is a Z-basis of (OK/docs#cyclotomic_ring), right? I guess we should also make the equiv to polynomial K / (X ^ k - 1), which I dont think we have

[Riccardo Brasca]

I am afraid we don't have a lot about power basis over rings that are not fields. We know that that O_K is Z[zeta] (I am on mobile, sorry)

[Eric Rodriguez]

don't worry! O_K is Z[zeta] how? I see docs#cyclotomic_ring but not the "classic" Z[zeta]

[Eric Rodriguez]

ah, if we have it as an adjoin_root * then we get docs#adjoin_root.power_basis'. I'll try see if this is workable

[Riccardo Brasca]

I mean docs#is_cyclotomic_extension.rat.is_integral_closure_adjoing_singleton_of_prime_pow for prime powers. The general case requires more work.

[Eric Rodriguez]

should be good enough for the last sorry, the prime assumption is missing right now but I don't think it's relevant to have it without, anyways

[Eric Rodriguez]

I guess what we really need is something like

example {K L M} [comm_ring K] [comm_ring L] [comm_ring M] [algebra K L] [algebra K M]
  {S} [is_cyclotomic_extension S K L] [is_cyclotomic_extension S K M] : L ≃ₐ[K] M :=

(I mean, I think for what we need domains is fine, and obviously singleton extensions). I'm going to try work on it, but not too sure it'll work too well!

[Riccardo Brasca]

The case of field follows from docs#is_cyclotomic_extension.splitting_field_X_pow_sub_one

[Riccardo Brasca]

I am not sure what to do with domains

[Riccardo Brasca]

Are you working on unit_inv_conj_not_neg_zeta_runity?

[Eric Rodriguez]

yeah, exactly the idea

[Eric Rodriguez]

not super actively though, just bits and bobs when I can find some spare time

[Riccardo Brasca]

Let me see if we can somehow produce a power basis over something it is not a field.

[Eric Rodriguez]

that's the hope with the equiv + adjoin_root, but I think actually this is just loops around the most important idea of getting the basis over not-a-field; this isn't "free" though, wasn't this something like a lattice or such? it's been a while since i've seen the standard texts

[Riccardo Brasca]

Yes, we cannot have this completely for free. For example if you take $R = \mathbb{Z}[\sqrt{-3}]$ and $x = \frac{1+\sqrt{-3}}{2}$, then $R[x]$ (the extension inside $K(x)$ where $K = \mathrm{Frac}(R)$) is not free over $R$, even if $x$ has minimal polynomial $x^2-x+1$.

[Riccardo Brasca]

The point is that $R$ is not integrally closed.

[Riccardo Brasca]

OK, I have a strategy. Let R be an integrally closed domain (for the mathlib proof we will need more, see below) with field of fraction K. Let L be an extension of K (probably very few assumption on L are needed, not even a field I think) and let x : L integral over R, and let f := minpoly R x. We construct an isomorphism adjoin_root f ≃ₐ[R] adjoin R x as follows:

• the morphism is given by docs#adjoin_root.lift_hom;
• x is in the image, so it is surjective (I didn't check the details, but everything is surely already in mathlib);
• injectivity is the interesting part. Let P1 : adjoin_root f be in the kernel. This gives via docs#adjoin_root.lift_hom_mk a polynomial P that has x as root. Now, f divides P! This is in general false without some assumption on R, but true if R is integrally closed. In mathlib the best result we have is docs#minpoly.gcd_domain_dvd, that is good enough for R = ℤ (the assumption that P is primitive is harmless). Since f divides P, by definition P1 = 0 and we're done.

[Riccardo Brasca]

Now one can use docs#adjoin_root.power_basis' to get the power basis of adjoin R x.

[Riccardo Brasca]

I think this is a really nice result we absolutely want in mathlib (maybe with also a version for fields, even if this one can be obtained using an easier strategy).

[Eric Rodriguez]

the field one already exists, docs#algebra.adjoin.power_basis

[Riccardo Brasca]

I mean the iso, but yes, it can be produced using this kind of results.

[Eric Rodriguez]

ah, right, I see

[Eric Rodriguez]

found this whilst looking for the surjectiveness: docs#alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly. I'm not so sure the surjectiveness is in, but it's not too bad so I'll try make it.

[Riccardo Brasca]

Yep the point is exactly to generalize this from field F to gcd_monoid F

[Eric Rodriguez]

this all comes back to #11523, I guess this is what you were thinking about back then!

[Riccardo Brasca]

Note that we don't need #11523 in flt-regular, we want to apply this in the case R = ℤ, so the current docs#minpoly.gcd_domain_dvd is enough. It should be really easy, I can write down a proof today.

[Eric Rodriguez]

I pushed what I had to a file called z_basis.lean. I'm not sure how much time I'll have further today, but I left some comments about what are the "obvious" sticking points; hopefully I get to sit down and work through them more methodically later.

[Riccardo Brasca]

I've added a new file src/ready_for_mathlib/adjoin_root.lean with

def minpoly.to_adjoin_equiv (hx : is_integral R x) :
  adjoin_root (minpoly R x) ≃ₐ[R] adjoin R ({x} : set A)

[Riccardo Brasca]

It is already sorry free. Now the idea is to transport docs#adjoin_root.power_basis' via this equiv, to get a power basis pb of adjoin R ({x} : set A) such that pb.gen = x.

[Riccardo Brasca]

This is also done.

[Riccardo Brasca]

@Eric Rodriguez do you agree that docs#cyclotomic_ring.eq_adjoin_primitive_root is evil? It is stated as an equality of types, but I think it should an iso of algebras, or whatever.

[Kevin Buzzard]

Yes that's definitely evil! It will be hard to use

[Eric Rodriguez]

yeah, do we have eq_to_equiv or sth somewhere?

[Junyan Xu]

You should copy the subalgebra if you want to transfer results between LHS/RHS, right? Subalgebra equality is unproblematic. (Maybe no need to copy, just use the subalgebra equality.)

[Eric Rodriguez]

cyclotomic_ring is the subalgebra with everything automatically coerced: def cyclotomic_ring : Type w := adjoin A { b : (cyclotomic_field n K) | b ^ (n : ℕ) = 1 }

[Eric Rodriguez]

it may be worth undoing that

[Riccardo Brasca]

I am not sure I follow your strategy. I just added to your file the following

variables {p : ℕ+} {k : ℕ} {K : Type*} [field K] [char_zero K] {ζ : K} [fact (p : ℕ).prime]

noncomputable
def power_basis_int [hcycl : is_cyclotomic_extension {p ^ k} ℚ K]
  (hζ : is_primitive_root ζ ↑(p ^ k)) : power_basis ℤ (𝓞 K) :=
let _ := is_integral_closure_adjoing_singleton_of_prime_pow hζ in by exactI
  (adjoin.power_basis' ℚ (hζ.is_integral (p ^ k).pos)).map
  (is_integral_closure.equiv ℤ (adjoin ℤ ({ζ} : set K)) K (𝓞 K))

@[simp] lemma power_basis_int_gen [hcycl : is_cyclotomic_extension {p ^ k} ℚ K]
  (hζ : is_primitive_root ζ ↑(p ^ k)) : (power_basis_int hζ).gen = ⟨ζ, hζ.is_integral (p ^ k).pos⟩ :=
sorry

[Riccardo Brasca]

This is what we want, right? I don't think there is a need to speak about cyclotomic_ring. The real object is 𝓞 K (that in this case is the same as cyclotomic_ring, but we can forget about it)

[Eric Rodriguez]

I'm suggesting we change cyclotomic_ring to subalgebra A (cyclotomic_field n K), and whenever it needs to be coerced then so be it

[Eric Rodriguez]

but yes, I think this is what we want!

[Riccardo Brasca]

I've proved power_basis_int_gen, so we now have a ℤ-power basis of the ring of integers of a cyclotomic extensions of ℚ whose generator is any given primitive root of unity (in the p^k-case).

[Riccardo Brasca]

This completely characterize the ring structure of 𝓞 K and since the API for power_basis is pretty complete, and we know everything about the minimal polynomial of the generator, nothing else should be needed to study 𝓞 K.

[Riccardo Brasca]

I suggest to avoid cyclotomic_ringas much as possible, I am wondering if we shouldn't have defined it, but anyway

[Eric Rodriguez]

I have pushed some work to unit_inv_conj_not_neg_zeta_runity (and, sadly, a power_basis_int' because x^1 is not defeq to x :[) some of it is an easy sorry (conj ζⁿ = ζ⁻ⁿ modulo coercions and whether we want to go into zpow or not) and the rest is the deciding how we're dealing with equality mod $(1 - \zeta)$ - this could be trivial or fairly hard, I'm not sure. We'll also end up needing that ζⁿ ∈ (1 - ζ), but I think we had that somewhere!

[Riccardo Brasca]

The need for power_basis_int' makes me a little sad, but that's like I guess.

[Riccardo Brasca]

I've never really thought about the math proof of unit_inv_conj_not_neg_zeta_runity. Which strategy are you following?

[Chris Birkbeck]

There is a proof in Washingtons book (if I remember correctly)

[Riccardo Brasca]

I will have a look, but it is not trivial, right?

[Chris Birkbeck]

I thought you needed to use the basis for the ring of integers, but I'm not 100% sure. I'm on mobile right now, but I can check when I get home

[Eric Rodriguez]

Yes, I'm following that proof. The idea is that you have a unit u and that is equal to sum a_iz^i, módulo the ideal it's sum a_i. The conjugate has a similar representation, and so 2u is in the ideal; but it's prime, and 2 is not in (1-z) and clearly neither is u.

[Riccardo Brasca]

Ah yes, I've found it. OK, it's not trivial but nothing specially difficult

[Riccardo Brasca]

You may want to modify what I did today to obtain a power basis whose generator is ζ - 1.

[Riccardo Brasca]

Hmm, no, that's OK.

[Riccardo Brasca]

In any case we need that $(ζ - 1)$ is a prime ideal.

[Riccardo Brasca]

This follows from the fact that the norm is p, but we need to know that an algebraic integer with norm 1 is a unit.

[Riccardo Brasca]

Which in turn follows from the fact that the Galois conjugate of an algebraic integer are algebraic integers.

[Eric Rodriguez]

some more boring stuff been done, mostly on fleshing out galois_action_on_cyclo so it's not littered with zeros. I like my proof for gal_conj_idempotent:)

[Eric Rodriguez]

on a serious note, I'm not sure what to do about embedding_conj: can we get things as ℚ-alg homs for free somehow?

[Eric Rodriguez]

then we can use power_basis.alg_hom_ext to make things nice

[Eric Rodriguez]

aha, I found docs#ring_hom.to_rat_alg_hom, but both have := φ.to_rat_alg_hom and have := (conj : ℂ →+* ℂ).to_rat_alg_hom get into TC loops :/ is this to do with qsmul and such?

[Eric Rodriguez]

ok, I figured out a workaround anyways. something is weird with the instance caches in that file.

[Eric Rodriguez]

galois_action_on_cyclo is now sorry-free, and Unit_lemmas is only waiting on finishing off this step.

[Riccardo Brasca]

Note that in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Embeddings.20of.20a.20.20number.20field we decided to use ring hom for number fields, rather than Q-alg hom, so we should follow that decision.

[Eric Rodriguez]

Yeah, it was just to use some results temporarily. See the top of galois_action_on_cyclo

[Eric Rodriguez]

Riccardo Brasca said:

Which in turn follows from the fact that the Galois conjugate of an algebraic integer are algebraic integers.

where do you want to put this? may have some time to work on this all today

[Riccardo Brasca]

In the project you can just create a new file, who cares. In mathlib it can go in the same file where is_integral is defined, it doesn't require any Galois theory. If σ : B →ₐ[A] B, where you have an algebra tower R/A/B and x : B is integral over R, then σ x is integral over R. It should be immediate, the minimal polynomial is the same.

[Riccardo Brasca]

Then I think the morally correct thing to do is define a function norm' : 𝓞 K →* 𝓞 K (it follows immediately from docs#algebra.is_integral_norm, but it is annoying to write obtain ... all the time) and prove that x ∈ (𝓞 K)ˣ iff norm' x ∈ (𝓞 K)ˣ.

[Eric Rodriguez]

do we have algebra.norm in terms of the galois group or do I have to write it? there's docs#algebra.norm_eq_prod_embeddings but that doesn't work because that all ends up in a larger extension

[Riccardo Brasca]

I just delegated a PR that does that for the trace

[Riccardo Brasca]

It should be easy to adapt to the norm

[Riccardo Brasca]

I am on mobile, but check the running PR

[Riccardo Brasca]

Or use the product of the roots of the minimal polynomial

[Riccardo Brasca]

#14523

[Eric Rodriguez]

thanks, I'll have a look at this

[Riccardo Brasca]

I've asked to do it for the norm. It should be really the same proof

[Xavier Roblot]

So there is at the moment an ongoing discussion on the best way to prove the formula for the coefficients of a polynomial in terms of its roots from the results in ring_theory.polynomia.vieta (see #1408). Until it is resolved, my PR of mem_roots_of_unity_of_abs_eq_one is on hold.
So is there anything else I can work on in the meantime? I see you guys have been quite busy lately and made some significant progress.

[Riccardo Brasca]

You can coordinate with @Eric Rodriguez to finish the proof of unit_inv_conj_not_neg_zeta_runity. We need that ζ - 1 is prime and it does not divide 2 (both are computation with the norm, we already have docs#is_primitive_root.sub_one_norm_prime_ne_two but we are mising some glue to obtain the two results).

Looking at the blueprint it seems that the only other missing result in sections 1-2-3 is Lemma 3.8, I think we don't even have the statement.

[Riccardo Brasca]

Note that #14523 will be in mathlib in a few hours, with the result about the norm.

[Eric Rodriguez]

Thanks @Iván Sadofschi Costa! I am working on showing (1 - z) is prime, im away from a computer right now but I should push a proof for that by ~ 2022-06-24T16:00:00+01:00

[Eric Rodriguez]

So Xavier, feel free to work on the other stuff (for now, just put it as a sorry that the ideal is prime)

[Eric Rodriguez]

i've finally pushed the unit stuff, sorry!

[Eric Rodriguez]

Riccardo Brasca said:

This follows from the fact that the norm is p, but we need to know that an algebraic integer with norm 1 is a unit.

how does this proof work? I had to return all my paper books now :(

[Riccardo Brasca]

The fact that I = (z-1) is prime? The math proof is that the norm (of the ideal) is p, so if I = AB then the norm of, say, A must be 1. Now I have to think how to prove that this implies that A` is trivial. The point is that ideals are not necessarily principal

[Riccardo Brasca]

It can be possible to avoid speaking of ideals but I have to think about it

[Riccardo Brasca]

Mmm, do we want to develop the theory of the norm of an ideal? Maybe we want

[Kevin Buzzard]

z-1 is prime because if you quotient out by it then you get Z/pZ

[Riccardo Brasca]

Do you have an elementary proof?

[Riccardo Brasca]

Ok, I see

[Kevin Buzzard]

The ideal z-1 can't be trivial because the norm of z-1 is p. In particular p is in the ideal (z-1). Now I claim that every element of Z[z] is of the form a+b(z-1) with a in {0,1,2,..,.p-1}, and the proof is...maybe you see :-)

[Kevin Buzzard]

z^n maps to 1 and p maps to 0 and it's game over.

[Riccardo Brasca]

Yes yes that's what I wanted to say but you're too fast

[Kevin Buzzard]

Still might be a slight challenge to formalise and to be honest I think your ideal argument is better because it's more conceptual so probably will have other uses.

[Kevin Buzzard]

If your definition of norm(I) is "size of R/I" then I think norm(I)=1 implies I=1, but maybe life is not so easy?

[Kevin Buzzard]

I should say that once LTE is out of the way I am looking forward to joining this project. But of course you should all stop working on this project and come and help us finish LTE, all we have left is about 60 statements about abelian categories and they're quite good fun to prove :-)

[Riccardo Brasca]

We have only the norm of an element, with all the basic property

[Riccardo Brasca]

And we know that the norm of 1-z is p

[Riccardo Brasca]

So p is in the ideal

[Riccardo Brasca]

I will try to formalize this tomorrow

[Eric Rodriguez]

Kevin Buzzard said:

I should say that once LTE is out of the way I am looking forward to joining this project. But of course you should all stop working on this project and come and help us finish LTE, all we have left is about 60 statements about abelian categories and they're quite good fun to prove :-)

I tried doing some of the self contained ones once and noped out very hard :b

[Eric Rodriguez]

I think doing the norm of an ideal is a good idea, I thought we had that but maybe we just have that it's finite because of Anne&co's work

[Riccardo Brasca]

I am giving a try to prove that 1-z is prime. It's maybe possible to do it rather directly, so let me see.

[Kevin Buzzard]

Norm prime implies prime of course

[Riccardo Brasca]

Yes, but that requires the norm of an ideal, that we don't have, right? If the norm of an element is prime that the element is irreducible, this is very easy, but primality seems to require a little bit of work.

[Kevin Buzzard]

We need (norm x) = ideal.norm (x)

[Riccardo Brasca]

What I mean is that there is no ideal.norm at all at the moment, unless I missed it.

[Chris Birkbeck]

Is there not? If that's the case maybe I'll try and add that next. It feels like something we should have

[Yaël Dillies]

Can you reuse docs#has_norm?

[Chris Birkbeck]

Or at least start on it

[Riccardo Brasca]

@Yaël Dillies It's called norm but it's a rather different concept, for example it takes value in Z, or even better in the set of ideals.

[Riccardo Brasca]

it's related to docs#algebra.norm

[Eric Rodriguez]

How can the norm take value in the set of ideals? Also I thought it was N-valued (the defn I know is |Z/I|)

[Kevin Buzzard]

There's a "relative" norm on elements N: A -> R for any finite locally free R-algebra A I guess. If R is Noetherian then I guess this is the same as finite flat R-algebra. But for ideal norms I'm a bit more hazy about what's going on.

[Kevin Buzzard]

The example I've taught is this absolute norm which Eric is talking about but this is specific to orders in integers of number fields or function fields

[Riccardo Brasca]

I think I have a Lean proof that 1-z is prime, avoiding the ideal norm. I will finish it after dinner

[Alex J. Best]

I have some work on a definition of the ideal norm, the absolute one at least. So if anyone else wants this we should coordinate a little!

[Riccardo Brasca]

I've proved here that if the norm (@Eric Rodriguez version taking values in the ring of integers) of the generator of an intgral power basis pb of a Galois extension of number fields is prime, then pb.gen is prime.

[Riccardo Brasca]

We need a little bit of glue to prove that z-1 is prime, since we have the integral power basis given by z, not by z-1. Constructing this one only require that the ring of integers is Z[z-1], that should be really easy given that we know it is Z[z].

[Riccardo Brasca]

In any case the proof of prime_of_norm_prime is a nice detour to avoid the ideal norm.

[Riccardo Brasca]

I am done for today, but here is something to do if you're annoyed tonight.

• Prove thatadjoin R {x+a} = adjoin R {x} if a : R.
• Prove the results in docs#number_theory.cyclotomic.rat with ζ replaced by ζ - 1.
• Construct the power_basis ℤ (𝓞 K) given by ζ - 1 as it's done here for ζ (this file should be moved).
• Prove that norm' K (ζ - 1) = (rat.ring_of_integers_equiv.symm p) using docs#is_primitive_root.sub_one_norm_prime.
• Finish the proof that ζ - 1 is prime using prime_of_norm_prime.

[Alex J. Best]

I guess we should have some more general operations on power bases by appropriate affine transformations?

[Riccardo Brasca]

We have docs#power_basis.of_gen_mem_adjoin that is very general. It works for fields, but it is possible that is generalizes more or less automatically.

[Riccardo Brasca]

Mmm, no, it uses docs#algebra.adjoin.power_basis that is false in general.

[Riccardo Brasca]

lemma zeta_sub_one_prime [is_cyclotomic_extension {p ^ (k + 1)} ℚ K]
  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) (hodd : p ≠ 2) :
  prime (⟨ζ - 1, hζ.sub_one_mem_ring_of_integers⟩ : R)

is sorry free.

[Riccardo Brasca]

The simps here is very slow... does anyone know to speed it up?

[Kevin Buzzard]

Did you try the now-standard technique of using simps? to find out what it's doing and then just doing it manually yourself? :-)

[Kevin Buzzard]

I have no idea why simps is sometimes randomly super-slow but you're not the first person to notice it recently.

[Yaël Dillies]

Because simps lemmas have to be in simp normal form, simps calls simp (or just dsimp?) on the LHS, but this sometimes results in oversimplified statements.

[Riccardo Brasca]

Yeah, adding it by hand seems faster.

[Riccardo Brasca]

#14979 and #14981 If someone wants to have a look.

[Riccardo Brasca]

I will very little time this week, but I will try to follow any progress.

[Chris Birkbeck]

Riccardo Brasca said:

You can coordinate with Eric Rodriguez to finish the proof of unit_inv_conj_not_neg_zeta_runity. We need that ζ - 1 is prime and it does not divide 2 (both are computation with the norm, we already have docs#is_primitive_root.sub_one_norm_prime_ne_two but we are mising some glue to obtain the two results).

Looking at the blueprint it seems that the only other missing result in sections 1-2-3 is Lemma 3.8, I think we don't even have the statement.

I don't think we actually need 3.8, we basically need something slightly easier, so I've updated this on the blueprint.

[Chris Birkbeck]

I'll add the statement in Lean as well.

[Riccardo Brasca]

@Chris Birkbeck have you added Lean statement? It seems something we can prove very quickly

[Chris Birkbeck]

Yes I added both the statement and proved it. Although the statement isnt quite the one I proved, but its the one we need,

[Riccardo Brasca]

Ah sorry, didn't see it. It's not in the graph right?

[Chris Birkbeck]

Ah maybe not. I'll check that!

[Eric Rodriguez]

I've finished unit_inv_conj_not_neg_zeta_runity and therefore unit_lemma_gal_conj is now sorry free. We are in the endgame!

[Chris Birkbeck]

Great! I think we just need to assemble these results into a proof of case 1!

[Riccardo Brasca]

Great job!!

[Riccardo Brasca]

I will write down what exactly is missing this week.

[Eric Rodriguez]

I do think we should try tidy some things before we do that, and try and agree in quite what form we want to state theorems; we have lots of cyclotomic_ring, adjoin ... mixed about everywhere; I think there's probably about 5 different ways we state $\mathcal{O} \left( \mathbb{Q}(\zeta) \right) = \mathbb{Z}[\zeta]$ and it makes shuffling things about painful

[Xavier Roblot]

Hi, I am Xavier Roblot. I am a number theorist in Lyon (and thus a colleague of @Filippo A. E. Nuccio who introduced me to Lean). I saw @Riccardo Brasca's talk about this project at the "Lean in Lyon" workshop and I would really like to contribute if I can. I have been learning to work with Lean during the last few weeks and I am still very far for being proficient with it, but I hope I can be of some help.

[Riccardo Brasca]

Hi Xavier! Thanks for your message, and welcome to the Lean community!
I was very busy recently, so I have to sit down and think about a reasonable plan for the next weeks, but I will try to do as soon as possible.

[Riccardo Brasca]

You can have a look at our blueprint. The links are not updated, but essentially everything in section 2 is in mathlib

[Riccardo Brasca]

3.1 and 3.2 are also done

[Riccardo Brasca]

We have to think a little bit about 3.3, even to state it

[Chris Birkbeck]

We have some stuff for 3.3 but it still needs some annoying lemmas

[Riccardo Brasca]

But I would say that lemmas 3.3-3.7 are more or less what we should concentrate now

[Chris Birkbeck]

Ive also been very bad at updating links on the blueprint. I'll try and do that tomorrow

[Riccardo Brasca]

@Xavier Roblot if you want to have a look at the project just use leanproject get flt-regular, but a lot of results are already in mathlib, in the number_theory/cyclotomic folder.

[Xavier Roblot]

Actually, I have been working on some version of 3.3 in the last few days as a pet project. But I am very far from a complete proof . Basically, I just (almost) proved so far that bounded roots give bounded coefficients, that might be already in mathlib... (Sorry posted in the wrong streams)

[Xavier Roblot]

I have downloaded the project. I'll have a closer look tomorrow.

[Riccardo Brasca]

What is you github username?

[Chris Birkbeck]

I've been slowly working on 3.4 in the unit_lemmas.lean file, but we need some more facts about totient functions which could also be a fun place to start

[Xavier Roblot]

My GitHub username is xroblot

[Riccardo Brasca]

I've sent you an invitation to the project. Feel free to push all sort of code to master, but try to avoid errors (sorry is of course totally fine).

[Riccardo Brasca]

Let me know if you are also interested in contributing to mathlib

[Alex J. Best]

I thought that I did bounded roots gives bounded coeffs, and that all roots abs val one implies root of unity in the project a while ago, but I'm not sure now, I'll try and find it later.

[Chris Birkbeck]

Yeah you did, it's somewhere in the repo

[Eric Rodriguez]

I always saw that stuff and got a bit worried because it looked dissimilar to the galois stuff I did but it's probably likely I did stuff wrong

[Filippo A. E. Nuccio]

Hi Xavier, I am happy to see you here. Welcome! I am sure that @Riccardo Brasca will have a lot of things to pass over to you, you won't be left without work :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

Hi Xavier!

[Chris Birkbeck]

Alex J. Best said:

I thought that I did bounded roots gives bounded coeffs, and that all roots abs val one implies root of unity in the project a while ago, but I'm not sure now, I'll try and find it later.

its mem_roots_of_unity_of_abs_eq_one which is in number_theory/cyclotomic/absolute_value.lean

[Riccardo Brasca]

I've missed this one, nice!! Killing the two remaining sorry in that file would be very nice

[Riccardo Brasca]

One has the rather scary comment

-- this goal isn't true as stated right now, the rhs could be a power of the lhs

:sweat_smile:

[Riccardo Brasca]

Is someone interested in finishing this? I think it's a nice piece of math, and it definitely deserves to be put in mathlib.

[Chris Birkbeck]

By this do you mean lemma 3.3 from the blueprint? i.e mem_roots_of_unity_of_abs_eq_one?

[Riccardo Brasca]

Yes, sorry

[Xavier Roblot]

I guess I can try to finish it if @Alex J. Best does not want to finish it himself. However, it will probably take me some time and I might need some help along the way :sweat_smile:

[Riccardo Brasca]

If you need some advice just ask!

[Alex J. Best]

I'm happy to help you help me! It's not so much that I don't want to finish it, just that I have a stack of other half finished Lean projects, and only so much time to devote to them. Its a very cool theorem and I definitely agree it belongs in mathlib, so if you'd like to finish it off that's great, thanks @Xavier Roblot. I'm happy to try and explain any of the choices I made, or things that I think can be improved from what I originally wrote.

[Xavier Roblot]

Ok, thanks for the answers. I'll try to finish it and I'll come back to you guys if I need help.

[Riccardo Brasca]

Something we also want is Lemma 3.7 in the blueprint. It shouldn't be difficult is anyone wants to try (I didn't check, it can somehow be already in mathlib).

[Ruben Van de Velde]

Not sure if this is the cleanest approach, and not sure it's true for b=0, but:

variables {α : Type*} [comm_ring α] [is_domain α] [is_dedekind_domain α]

example (p : nat) (a b c : ideal α) (cp : is_coprime a b) (h : a*b = c^p) (hb : b ≠ 0) :
  ∃ d : ideal α, a = d ^ p :=
begin
  classical,
  obtain rfl|ha := eq_or_ne a 0,
  { use 0, apply (zero_pow _).symm, contrapose! h,
    rw le_zero_iff at h, rw [h, pow_zero, zero_mul], exact zero_ne_one },
  let fa := unique_factorization_monoid.normalized_factors a,
  let fb := unique_factorization_monoid.normalized_factors b,
  let fc := unique_factorization_monoid.normalized_factors c,
  have : ∀ d ∈ fa, d ∉ fb,
  { intros d ha hb,
    have := unique_factorization_monoid.irreducible_of_normalized_factor _ ha,
    apply irreducible.not_unit this,
    apply is_coprime.is_unit_of_dvd' cp;
    apply unique_factorization_monoid.dvd_of_mem_normalized_factors;
    assumption },
  suffices : ∃ f : multiset (ideal α), fa = p • f,
  { obtain ⟨f, hf⟩ := this,
    refine ⟨f.prod, _⟩ ,
    have := unique_factorization_monoid.normalized_factors_prod ha,
    rw associated_eq_eq at this,
    rw [←this, ←multiset.prod_nsmul, ←hf] },
  refine multiset.exists_smul_of_dvd_count _ (λ x hx, _),
  have hxb := this x hx,
  convert dvd_mul_right p (fc.count x),
  rw [←multiset.count_nsmul, ←unique_factorization_monoid.normalized_factors_pow, ←h,
    unique_factorization_monoid.normalized_factors_mul ha hb],
  rw multiset.count_add,
  convert (add_zero _).symm,
  apply multiset.count_eq_zero_of_not_mem hxb,
end

[Riccardo Brasca]

Very nice! Would you mind to push it to master in the flt-regular repository? You can create a new file in the ready_for_mathlib folder

[Riccardo Brasca]

And of course if you want to PR it you're welcome!

[Riccardo Brasca]

I've sent you an invitation

[Ruben Van de Velde]

I'm not sure I have all the right imports, so I made a pr: https://github.com/leanprover-community/flt-regular/pull/61

[Ruben Van de Velde]

Need to check where it goes wrong for plain ufds instead of ideals of Dedekind domains, though

[Riccardo Brasca]

For the project if it compiles then it's OK for master :)

[Eric Rodriguez]

this is symmetric in a+b, right? so it should work for b=0? especially as you don't use hb in the subproof

[Eric Rodriguez]

oh, I see that as usual my reading abilities drop to zero when I'm reading other people's code

[Eric Rodriguez]

thankfully the statement is true for b zero, proof pushed

[Riccardo Brasca]

You're faster than me!

[Eric Rodriguez]

I generalised is_unit_iff' to comm_semirings, because of what Ruben said about ufds, but not sure how this could hold in UFDs; are UFDs' ideals atomic?

[Riccardo Brasca]

I wouldn't care about UFD, and it wouldn't be a generalization

[Riccardo Brasca]

Most Dedekind domains are not UFD

[Eric Rodriguez]

Right, fair, no big deal then

[Riccardo Brasca]

Of course for UFD the corresponding relevant statement is about elements, and it should be easy

[Alex J. Best]

Well I guess the generalization would be to unique factorization monoids rather than ideals of Dedekind domains

[Riccardo Brasca]

The trick for b=0 won't work in general I think (since there can be units that are not p-powers), but the rest should be the same.

[Ruben Van de Velde]

I've got some pretty awful code up at https://gist.github.com/Ruben-VandeVelde/d82c653a8cc2315a3985e60ed4637346 - might try to make something of it later

[Ruben Van de Velde]

Sorry-free at least, but still hairy

[Riccardo Brasca]

Feel free to push it to flt-regular if you want, don't worry about names and similar stuff (and in exchange someone will fix any problem arising from mathlib bumps).

[Xavier Roblot]

I am sorry but I am making very slow progress. I have a lot of difficulties figuring out even very easy things. For example, I have a number_field K, number_field L and algebra K L. So I should be able to see K as having type intermediate_fields ℚ L, but I cannot just figure out how to say to Lean to do that. Any help would be very welcome.

[Ruben Van de Velde]

Ruben Van de Velde said:

I've got some pretty awful code up at https://gist.github.com/Ruben-VandeVelde/d82c653a8cc2315a3985e60ed4637346 - might try to make something of it later

In the end it turns out my generalization wasn't quite a generalization: I required comm_ring and ideals of Dedekind domains seem to only be a comm_semiring. Maybe https://github.com/leanprover-community/mathlib/pull/14423 will help, we'll see. Got some interesting lemmas out of it, in any case

[Kevin Buzzard]

Xavier Roblot said:

I am sorry but I am making very slow progress. I have a lot of difficulties figuring out even very easy things. For example, I have a number_field K, number_field L and algebra K L. So I should be able to see K as having type intermediate_fields ℚ L, but I cannot just figure out how to say to Lean to do that. Any help would be very welcome.

@Xavier Roblot a more effective way to ask questions is to give a #mwe , for example

import number_theory.number_field

variables (K L : Type) [field K] [number_field K] [field L] [number_field L]
[algebra K L]

example : intermediate_field ℚ L := sorry

That way I don't have to figure out imports myself or start guessing that you probably mean intermediate_field not intermediate_fields.

Here's a partial solution:

import number_theory.number_field

variables (K L : Type) [field K] [number_field K] [field L] [number_field L]
[algebra K L]

-- To make an intermediate field you need to give
-- (1) the subset, (called `carrier`)
-- (2) a proof that the subset contains ℚ, (called `algebra_map_mem'`)
-- (3) a proof of all the axioms for a subfield.

example : intermediate_field ℚ L :=
  -- The subset is the image of the canonical map K → L
{ carrier := set.range (algebra_map K L),
    -- this is a fairly incomprehensible proof
    -- that the image of the map from K to L
    -- must contain the image of the rationals.
  algebra_map_mem' := λ r, ⟨r, begin
    rw [map_rat_cast],
    convert (map_rat_cast (algebra_map ℚ L) r).symm,
    exact congr_arg _ r.cast_id.symm,
  end⟩,
  -- A ring homomorphism maps 0 to 0 so
  -- 0 is in the subset
  zero_mem' := ⟨0, map_zero _⟩,
  -- Same story for 1; `map_one` says a ring hom maps
  -- 1 to 1.
  one_mem' := ⟨1, map_one _⟩,
  -- This next begin/end block is a proof that the product
  -- of two things in the subset is in the subset. It uses
  -- the theorem that ring homomorphisms commute with
  -- multiplication, which is called `map_mul`.
  -- It also uses the `rintro rfl` trick.
  mul_mem' := begin
    rintro - - ⟨s, rfl⟩ ⟨t, rfl⟩,
    exact ⟨s * t, map_mul _ _ _⟩,
  end,
  -- Exercise for the reader.
  add_mem' := begin sorry end,
  neg_mem' := begin sorry end,
  inv_mem' := begin sorry end,
  }

[Xavier Roblot]

Kevin, thanks (again) for helping me. Sorry about the lack of #mwe. I'll remember to add one next time.
Somehow, I thought there was a quick way to solve the problem, but I see that one has to construct the intermediate_field from the definition... Anyway, back to work

[Riccardo Brasca]

In your example K is not literally an intermediate_field (this is false even mathematically, K is not a subset of L. Of course there is the image, but still...). The best question is probably why you want an intermediate field.

[Riccardo Brasca]

Ruben Van de Velde said:

Ruben Van de Velde said:

I've got some pretty awful code up at https://gist.github.com/Ruben-VandeVelde/d82c653a8cc2315a3985e60ed4637346 - might try to make something of it later

In the end it turns out my generalization wasn't quite a generalization: I required comm_ring and ideals of Dedekind domains seem to only be a comm_semiring. Maybe https://github.com/leanprover-community/mathlib/pull/14423 will help, we'll see. Got some interesting lemmas out of it, in any case

This

variables {β : Type*} [comm_ring β] [is_domain β] [unique_factorization_monoid β]

lemma exists_associated_pow_of_mul_eq_pow (p : nat) (a b c : β) (cp : is_coprime a b) (h : a*b = c^p) (hb : b ≠ 0) :
  ∃ d : β, associated a (d ^ p) :=

looks a good generalization, ideals of a Dedekind domain are a unique_factorization_monoid, and in this case associated means equal (do we have this lemma?).

[Yaël Dillies]

docs#associated_iff_eq ?

[Yaël Dillies]

Sorry, you accidentally triggered yael_search!

[Riccardo Brasca]

Yes, that's probably it (I am still having my coffee, to early on Saturday morning to check if we have unique...)

[Riccardo Brasca]

Riccardo Brasca said:

Ruben Van de Velde said:

Ruben Van de Velde said:

I've got some pretty awful code up at https://gist.github.com/Ruben-VandeVelde/d82c653a8cc2315a3985e60ed4637346 - might try to make something of it later

In the end it turns out my generalization wasn't quite a generalization: I required comm_ring and ideals of Dedekind domains seem to only be a comm_semiring. Maybe https://github.com/leanprover-community/mathlib/pull/14423 will help, we'll see. Got some interesting lemmas out of it, in any case

This

variables {β : Type*} [comm_ring β] [is_domain β] [unique_factorization_monoid β]

lemma exists_associated_pow_of_mul_eq_pow (p : nat) (a b c : β) (cp : is_coprime a b) (h : a*b = c^p) (hb : b ≠ 0) :
  ∃ d : β, associated a (d ^ p) :=

looks a good generalization, ideals of a Dedekind domain are a unique_factorization_monoid, and in this case associated means equal (do we have this lemma?).

Ah, you have variables {β : Type*} [comm_ring β] [is_domain β] [unique_factorization_monoid β], that's too much! β should only be a monoid.

[Riccardo Brasca]

I see is_coprime is defined via Bezout, so it wants a semiring.

[Riccardo Brasca]

I've asked a related question here

[Xavier Roblot]

Riccardo Brasca said:

In your example K is not literally an intermediate_field (this is false even mathematically, K is not a subset of L. Of course there is the image, but still...). The best question is probably why you want an intermediate field.

I need to prove that any embedding $K \to \mathbb{C}$ can be lifted to an embedding $L \to \mathbb{C}$. This should follow from the intermediate_field.lifts machinery using the primitive element theorem.

[Riccardo Brasca]

We have docs#is_alg_closed.lift

[Riccardo Brasca]

In general it is a little tricky to decide if one wants to work with substuff of not. substuff has the advantage that you can literally prove that two things are equal by ext, you can take intersections and so on. But usually at some point you discover that something is not literally a subset and then you regret your choice. I suggest to try to avoid it if possible.

[Xavier Roblot]

Riccardo, thanks for the advice. I wished I found out about is_alg_closed.lift sooner. I guess I am still not skilled enough at searching the library :sweat_smile:

[Riccardo Brasca]

I found it as follows: the reason why this is true is that C is algebraically closed, and I randomly tried is_alg_closed.lift. I would have been very surprised if we had it only for intermediate_field.

[Kevin Buzzard]

@Xavier Roblot there could well be an easier way -- it wouldn't surprise me if for a large class of morphisms (group homomorphisms, ring homomorphisms etc) there's a function already there which gives the construction of an image subobject. I was too lazy to look for it.

[Xavier Roblot]

Kevin Buzzard said:

Xavier Roblot there could well be an easier way -- it wouldn't surprise me if for a large class of morphisms (group homomorphisms, ring homomorphisms etc) there's a function already there which gives the construction of an image subobject. I was too lazy to look for it.

Well, I was able to get a nice short proof with is_alg_closed.lift so I am happy with that.

[Kevin Buzzard]

By the way I totally agree that as a relative newcomer it's very hard to guess what the best way of implementing the data of a question should be. The Artin-Tate lemma (according to Atiyah--Macdonald, at least) is a statement involving three commutative rings $A\subseteq B\subseteq C$ and in the proof you build a 4th ring $B\subseteq D\subseteq C$. Are you supposed to let $A,B,C$ be types and give them [ring] instances, or should $C$ be the ring (the type) and $A$ and $B$ be subrings, or should $B$ be the ring, $A$ a subring and $C$ a $B$-algebra? Then all the same questions for $D$. Questions like this are rather delicate. In the old days your decisions would be influenced by questions such as "do we have more API for subring or algebra" but nowadays we have lots of API for both so in some sense it's probably true that whatever decision you make, you'll be able to get the proof out in the end. But bad design decisions might mean that constructing the proof is painful. In the case of the Artin-Tate lemma we eventually let all the rings be types and used algebra to glue everything together, and also is_scalar_tower (this is a statement that a triangle commutes).

[Riccardo Brasca]

I noticed we need

lemma totient_super_multiplicative (a b : ℕ) : a.totient * b.totient ≤ (a * b).totient

this should be easy and it can go directly to mathlib. So if someone is looking for a place to start this looks like a nice small lemma.

[Chris Birkbeck]

Riccardo Brasca said:

I noticed we need

lemma totient_super_multiplicative (a b : ℕ) : a.totient * b.totient ≤ (a * b).totient

this should be easy and it can go directly to mathlib. So if someone is looking for a place to start this looks like a nice small lemma.

I'm actually working on this now. Actually, I'm proving that totient is is_gcd_mult (which is a made up name)

[Chris Birkbeck]

We also need

lemma contains_two_primitive_roots (p q : ℕ)
(x y : K) (hx : is_primitive_root x p) (hy : is_primitive_root y q): (lcm p q ).totient ≤
(finite_dimensional.finrank ℚ K) :=

But this might be harder/more annoying

[Eric Rodriguez]

can't we just create the explicit element of order ф(lcm p q) and then that gives us a bound on the finrank?

[Eric Rodriguez]

not order... my words are vanishing in my head

[Eric Rodriguez]

I think we have that K + a primitive root is a cyclotomic extension somewhere

[Chris Birkbeck]

Eric Rodriguez said:

can't we just create the explicit element of order ф(lcm p q) and then that gives us a bound on the finrank?

Yeah thats the idea. I guess I don't know how easy it is at the moment to go from knowing we have some root of unity in the field, to giving a lower bound on the degree.

[Chris Birkbeck]

But I've not yet looked into the API for this, so maybe its easy

[Eric Rodriguez]

docs#is_cyclotomic_extension.finrank, docs#is_primitive_root.adjoin_is_cyclotomic_extension

[Eric Rodriguez]

I think we don't have that if A C S is a cycl extension, and A B K is one, then B C (S / K) is but maybe that follows from something like is_cyclotomic_extension.trans

[Eric Rodriguez]

and also I don't think we can turn for example is_cycl_ext A B {p, q} into is_cycl_ext A B {lcm p q} or for a nice challenge is_cycl_ext A B S to is_cycl_extension A B {S.lcm id}

[Chris Birkbeck]

Riccardo Brasca said:

I noticed we need

lemma totient_super_multiplicative (a b : ℕ) : a.totient * b.totient ≤ (a * b).totient

this should be easy and it can go directly to mathlib. So if someone is looking for a place to start this looks like a nice small lemma.

Alright, this is done, but its still a mess. I'll golf and look to PR it next week.

[Riccardo Brasca]

I've made some progress in contains_two_primitive_roots. It's quite annoying, but I've constructed an element of order lcm p q (modulo the fact that the order doesn't change under a coercion, this is an independent result that I don't find). I will not work on this for a couple of days, if someone wants to finish from here no problems.

[Riccardo Brasca]

The two sorry about the order are done.

[Riccardo Brasca]

I guess we need to generalize docs#is_cyclotomic_extension.finrank to the case L is domain. It should be very easy.

[Eric Rodriguez]

I'm not sure how easy that is with the current proof

[Riccardo Brasca]

I think there is simply nothing to do. Note that I don't want to generalize the base ring, just the big one.

[Riccardo Brasca]

I've tested docs#is_primitive_root.power_basis and it's OK

[Riccardo Brasca]

I mean like in #14550. I have to stop now, but docs#is_cyclotomic_extension.finrank is OK in that PR. Something broke later, but I think it is just because C is implicit/explicit or something similar. If you have time and want to finish it feel free to work on it :grinning_face_with_smiling_eyes:

[Eric Rodriguez]

I'll have a try when I get to the airport and have some time :)

[Riccardo Brasca]

I am officially late for my lunch, but it should work now.

[Riccardo Brasca]

I didn't touch docs#is_primitive_root.embeddings_equiv_primitive_roots (because I am lazy) but it should be generalizable too.

[Eric Rodriguez]

sorry, I had a hectic while, I think I should've fixed it now

[Eric Rodriguez]

I wonder if this is a Lean change more than anything, I assume that if you have a cycl extension over a field (apart from the fact that unit is the {}th cyclotomic extension) then we have that it is also a field though

[Eric Rodriguez]

but if it helps it helps!

[Eric Rodriguez]

if anyone is reading this stream, reviews on #14463 would be good! (this is another one, changing the defn of is_cyclotomic_extension)

[Xavier Roblot]

I have finished the proof of lemma 3.3: mem_roots_of_unity_of_abs_eq_one. I am going to take a few days to polish and clean the proof, but I should have something ready soon. What should I do when it's ready? should I just do a git push origin of my local branch?

[Ruben Van de Velde]

Yeah - though feel free to push your branch before polishing as well

[Riccardo Brasca]

Eric Rodriguez said:

I wonder if this is a Lean change more than anything, I assume that if you have a cycl extension over a field (apart from the fact that unit is the {}th cyclotomic extension) then we have that it is also a field though

Yes, a domain that is a finite extension of a field is a field (multiplication by an element is injective, hence surjective). I guess this is somewhere with is_field.

[Eric Rodriguez]

I guess this doesn't hold for something like {3,9,27,...} though, although maybe it holds for deeper reasons

[Riccardo Brasca]

It holds (assuming it is a domain, I don't know whether this is automatic): take x in the extension. It is algebraic, so the subextension generated by it it's finite and so it contains an inverse of x.

[Riccardo Brasca]

docs#is_integral.is_field_iff_is_field

[Xavier Roblot]

Well, I pushed my changes to the project. I hope I didn't break anything...

[Eric Rodriguez]

Riccardo Brasca said:

docs#is_integral.is_field_iff_is_field

indeed, right below integral, this works:

lemma is_field (C) [comm_ring C] [is_domain C] [algebra K C] [fintype S]
  [is_cyclotomic_extension S K C] : is_field C :=
(is_integral.is_field_iff_is_field (integral S K C) $ (algebra_map K C).injective).mp $
  field.to_is_field K

I'll PR a fix to dot notation on that lemma, and when I get some actual time I'll try extend the proof to non-finite S for fun

[Eric Rodriguez]

I'll have a look at why your thing isn't building, Xavier! seems to just be a small namespace thing so apart from that it looks good

[Riccardo Brasca]

Thanks for working on #14550! Do you think it is ready for review?

[Eric Rodriguez]

oh, it compiled! yes, it is :)

[Riccardo Brasca]

Xavier Roblot said:

I have finished the proof of lemma 3.3: mem_roots_of_unity_of_abs_eq_one. I am going to take a few days to polish and clean the proof, but I should have something ready soon. What should I do when it's ready? should I just do a git push origin of my local branch?

I've missed this message, great job!

[Xavier Roblot]

Thanks. But now I am hooked :sweat_smile: Is there any thing else I can work on?

[Riccardo Brasca]

Well, following the philosophy of the project I think you should PR this!

[Kevin Buzzard]

Do you have a roadmap for this project or some kind of plan? I'm hard at work with LTE now but when it's done I'd like to join the Fermat project too.

[Eric Rodriguez]

https://leanprover-community.github.io/flt-regular/

[Riccardo Brasca]

We are almost ready to attack case I, right? I will check this tomorrow

[Riccardo Brasca]

I think the next boss is the unit lemma. We have a draft version here but we should probably refactor some definition/results. I have time now to produce a reasonable statement.

[Chris Birkbeck]

Yeah I agree. One think to fix is the Galois action on these things. I think at the moment it's probably a bit to hacky

[Riccardo Brasca]

Do we have somewhere that the conjugate of a complex number of norm 1 is its inverse? It should be easy anyway

[Riccardo Brasca]

it is essentially docs#complex.norm_sq_eq_conj_mul_self

[Riccardo Brasca]

So I propose to redefine is_gal_conj_real in terms of the Galois group, connect it with ℝ in some way, and prove the unit lemma using this new "is real" notion.

[Chris Birkbeck]

Do we need to connect it to ℝ? If I remember correctly the proofs only ever use that things are fixed by complex conjugation.

[Riccardo Brasca]

Probably not, but it seems a reasonable thing to have. And it should be a couple of lines

[Chris Birkbeck]

Fair enough, I thought linking things to ℝ would make things more annoying because of extra coe maps. But maybe this is fine/you have something else in mind

[Riccardo Brasca]

I am not saying we should use ℝ anywhere in the project. Just the fact that is_gal_conj_real x is equivalent to x ∈ ℝ (strictly speaking this doesn't make sense), but this is useful only to explain what is_gal_conj_real x means, not to actually work with it.

[Chris Birkbeck]

Oh ok I get you! Yes then I agree

[Riccardo Brasca]

I mean, if I see this in a PR I would immediately ask for it, even if mathematically it's not needed.

[Xavier Roblot]

Riccardo Brasca said:

Well, following the philosophy of the project I think you should PR this!

Ok. Can you please give me access to push to mathlib?
Also, there are some choices that need to be discussed. I'll create a new thread for that.

[Riccardo Brasca]

You should have an invitation

[Xavier Roblot]

Got it. Thanks!

[Riccardo Brasca]

Having a PR accepted can be a little frustrating, so don't be afraid of asking questions, and be patient :grinning:

[Riccardo Brasca]

Thanks to #14550 contains_two_primitive_roots is now proved. I am not sure I have time today, but we need a small refactor of number_theory/cyclotomic/Unit_lemmas, replacing KK by a generic cyclotomic extension.

[Riccardo Brasca]

@Xavier Roblot do you mind moving the material you PRed to the ready_for_mathlib folder? Just to keep track of what we are adding to mathlib. (And I will have a look at you PR today)

[Xavier Roblot]

I moved the things already PRed in a previous commit named PR #14749. I am still working on the other PRs.

Thanks for the taking the time to look at my PR!

[Riccardo Brasca]

I've added a "From flt-regular" at the end of the description of the PR.

[Riccardo Brasca]

I've also left a couple of comments. I think a lot of the results you prove in your specific case are already somewhere in mathlib (in greater generality). It can be tricky to find them, but don't hesitate to ask here!

[Riccardo Brasca]

There is unit_inv_conj_not_neg_zeta_runity in src/number_theory/cyclotomic/Unit_lemmas.lean that is the last sorry in the file. If someone wants to try it please go ahead.

[Eric Rodriguez]

is docs#smodeq the correct way to talk about things being equal up to an ideal?

[Eric Rodriguez]

I don't really want to develop new API unless necessary but I know some people don't like the ideal/submodule R R defeq too much

[Riccardo Brasca]

Mathematically I would just work in the quotient, in mathlib I am not sure.

[Eric Rodriguez]

We don't actually have that docs#is_primitive_root.power_basis is a Z-basis of (OK/docs#cyclotomic_ring), right? I guess we should also make the equiv to polynomial K / (X ^ k - 1), which I dont think we have

[Riccardo Brasca]

I am afraid we don't have a lot about power basis over rings that are not fields. We know that that O_K is Z[zeta] (I am on mobile, sorry)

[Eric Rodriguez]

don't worry! O_K is Z[zeta] how? I see docs#cyclotomic_ring but not the "classic" Z[zeta]

[Eric Rodriguez]

ah, if we have it as an adjoin_root * then we get docs#adjoin_root.power_basis'. I'll try see if this is workable

[Riccardo Brasca]

I mean docs#is_cyclotomic_extension.rat.is_integral_closure_adjoing_singleton_of_prime_pow for prime powers. The general case requires more work.

[Eric Rodriguez]

should be good enough for the last sorry, the prime assumption is missing right now but I don't think it's relevant to have it without, anyways

[Eric Rodriguez]

I guess what we really need is something like

example {K L M} [comm_ring K] [comm_ring L] [comm_ring M] [algebra K L] [algebra K M]
  {S} [is_cyclotomic_extension S K L] [is_cyclotomic_extension S K M] : L ≃ₐ[K] M :=

(I mean, I think for what we need domains is fine, and obviously singleton extensions). I'm going to try work on it, but not too sure it'll work too well!

[Riccardo Brasca]

The case of field follows from docs#is_cyclotomic_extension.splitting_field_X_pow_sub_one

[Riccardo Brasca]

I am not sure what to do with domains

[Riccardo Brasca]

Are you working on unit_inv_conj_not_neg_zeta_runity?

[Eric Rodriguez]

yeah, exactly the idea

[Eric Rodriguez]

not super actively though, just bits and bobs when I can find some spare time

[Riccardo Brasca]

Let me see if we can somehow produce a power basis over something it is not a field.

[Eric Rodriguez]

that's the hope with the equiv + adjoin_root, but I think actually this is just loops around the most important idea of getting the basis over not-a-field; this isn't "free" though, wasn't this something like a lattice or such? it's been a while since i've seen the standard texts

[Riccardo Brasca]

Yes, we cannot have this completely for free. For example if you take $R = \mathbb{Z}[\sqrt{-3}]$ and $x = \frac{1+\sqrt{-3}}{2}$, then $R[x]$ (the extension inside $K(x)$ where $K = \mathrm{Frac}(R)$) is not free over $R$, even if $x$ has minimal polynomial $x^2-x+1$.

[Riccardo Brasca]

The point is that $R$ is not integrally closed.

[Riccardo Brasca]

OK, I have a strategy. Let R be an integrally closed domain (for the mathlib proof we will need more, see below) with field of fraction K. Let L be an extension of K (probably very few assumption on L are needed, not even a field I think) and let x : L integral over R, and let f := minpoly R x. We construct an isomorphism adjoin_root f ≃ₐ[R] adjoin R x as follows:

• the morphism is given by docs#adjoin_root.lift_hom;
• x is in the image, so it is surjective (I didn't check the details, but everything is surely already in mathlib);
• injectivity is the interesting part. Let P1 : adjoin_root f be in the kernel. This gives via docs#adjoin_root.lift_hom_mk a polynomial P that has x as root. Now, f divides P! This is in general false without some assumption on R, but true if R is integrally closed. In mathlib the best result we have is docs#minpoly.gcd_domain_dvd, that is good enough for R = ℤ (the assumption that P is primitive is harmless). Since f divides P, by definition P1 = 0 and we're done.

[Riccardo Brasca]

Now one can use docs#adjoin_root.power_basis' to get the power basis of adjoin R x.

[Riccardo Brasca]

I think this is a really nice result we absolutely want in mathlib (maybe with also a version for fields, even if this one can be obtained using an easier strategy).

[Eric Rodriguez]

the field one already exists, docs#algebra.adjoin.power_basis

[Riccardo Brasca]

I mean the iso, but yes, it can be produced using this kind of results.

[Eric Rodriguez]

ah, right, I see

[Eric Rodriguez]

found this whilst looking for the surjectiveness: docs#alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly. I'm not so sure the surjectiveness is in, but it's not too bad so I'll try make it.

[Riccardo Brasca]

Yep the point is exactly to generalize this from field F to gcd_monoid F

[Eric Rodriguez]

this all comes back to #11523, I guess this is what you were thinking about back then!

[Riccardo Brasca]

Note that we don't need #11523 in flt-regular, we want to apply this in the case R = ℤ, so the current docs#minpoly.gcd_domain_dvd is enough. It should be really easy, I can write down a proof today.

[Eric Rodriguez]

I pushed what I had to a file called z_basis.lean. I'm not sure how much time I'll have further today, but I left some comments about what are the "obvious" sticking points; hopefully I get to sit down and work through them more methodically later.

[Riccardo Brasca]

I've added a new file src/ready_for_mathlib/adjoin_root.lean with

def minpoly.to_adjoin_equiv (hx : is_integral R x) :
  adjoin_root (minpoly R x) ≃ₐ[R] adjoin R ({x} : set A)

[Riccardo Brasca]

It is already sorry free. Now the idea is to transport docs#adjoin_root.power_basis' via this equiv, to get a power basis pb of adjoin R ({x} : set A) such that pb.gen = x.

[Riccardo Brasca]

This is also done.

[Riccardo Brasca]

@Eric Rodriguez do you agree that docs#cyclotomic_ring.eq_adjoin_primitive_root is evil? It is stated as an equality of types, but I think it should an iso of algebras, or whatever.

[Kevin Buzzard]

Yes that's definitely evil! It will be hard to use

[Eric Rodriguez]

yeah, do we have eq_to_equiv or sth somewhere?

[Junyan Xu]

You should copy the subalgebra if you want to transfer results between LHS/RHS, right? Subalgebra equality is unproblematic. (Maybe no need to copy, just use the subalgebra equality.)

[Eric Rodriguez]

cyclotomic_ring is the subalgebra with everything automatically coerced: def cyclotomic_ring : Type w := adjoin A { b : (cyclotomic_field n K) | b ^ (n : ℕ) = 1 }

[Eric Rodriguez]

it may be worth undoing that

[Riccardo Brasca]

I am not sure I follow your strategy. I just added to your file the following

variables {p : ℕ+} {k : ℕ} {K : Type*} [field K] [char_zero K] {ζ : K} [fact (p : ℕ).prime]

noncomputable
def power_basis_int [hcycl : is_cyclotomic_extension {p ^ k} ℚ K]
  (hζ : is_primitive_root ζ ↑(p ^ k)) : power_basis ℤ (𝓞 K) :=
let _ := is_integral_closure_adjoing_singleton_of_prime_pow hζ in by exactI
  (adjoin.power_basis' ℚ (hζ.is_integral (p ^ k).pos)).map
  (is_integral_closure.equiv ℤ (adjoin ℤ ({ζ} : set K)) K (𝓞 K))

@[simp] lemma power_basis_int_gen [hcycl : is_cyclotomic_extension {p ^ k} ℚ K]
  (hζ : is_primitive_root ζ ↑(p ^ k)) : (power_basis_int hζ).gen = ⟨ζ, hζ.is_integral (p ^ k).pos⟩ :=
sorry

[Riccardo Brasca]

This is what we want, right? I don't think there is a need to speak about cyclotomic_ring. The real object is 𝓞 K (that in this case is the same as cyclotomic_ring, but we can forget about it)

[Eric Rodriguez]

I'm suggesting we change cyclotomic_ring to subalgebra A (cyclotomic_field n K), and whenever it needs to be coerced then so be it

[Eric Rodriguez]

but yes, I think this is what we want!

[Riccardo Brasca]

I've proved power_basis_int_gen, so we now have a ℤ-power basis of the ring of integers of a cyclotomic extensions of ℚ whose generator is any given primitive root of unity (in the p^k-case).

[Riccardo Brasca]

This completely characterize the ring structure of 𝓞 K and since the API for power_basis is pretty complete, and we know everything about the minimal polynomial of the generator, nothing else should be needed to study 𝓞 K.

[Riccardo Brasca]

I suggest to avoid cyclotomic_ringas much as possible, I am wondering if we shouldn't have defined it, but anyway

[Eric Rodriguez]

I have pushed some work to unit_inv_conj_not_neg_zeta_runity (and, sadly, a power_basis_int' because x^1 is not defeq to x :[) some of it is an easy sorry (conj ζⁿ = ζ⁻ⁿ modulo coercions and whether we want to go into zpow or not) and the rest is the deciding how we're dealing with equality mod $(1 - \zeta)$ - this could be trivial or fairly hard, I'm not sure. We'll also end up needing that ζⁿ ∈ (1 - ζ), but I think we had that somewhere!

[Riccardo Brasca]

The need for power_basis_int' makes me a little sad, but that's like I guess.

[Riccardo Brasca]

I've never really thought about the math proof of unit_inv_conj_not_neg_zeta_runity. Which strategy are you following?

[Chris Birkbeck]

There is a proof in Washingtons book (if I remember correctly)

[Riccardo Brasca]

I will have a look, but it is not trivial, right?

[Chris Birkbeck]

I thought you needed to use the basis for the ring of integers, but I'm not 100% sure. I'm on mobile right now, but I can check when I get home

[Eric Rodriguez]

Yes, I'm following that proof. The idea is that you have a unit u and that is equal to sum a_iz^i, módulo the ideal it's sum a_i. The conjugate has a similar representation, and so 2u is in the ideal; but it's prime, and 2 is not in (1-z) and clearly neither is u.

[Riccardo Brasca]

Ah yes, I've found it. OK, it's not trivial but nothing specially difficult

[Riccardo Brasca]

You may want to modify what I did today to obtain a power basis whose generator is ζ - 1.

[Riccardo Brasca]

Hmm, no, that's OK.

[Riccardo Brasca]

In any case we need that $(ζ - 1)$ is a prime ideal.

[Riccardo Brasca]

This follows from the fact that the norm is p, but we need to know that an algebraic integer with norm 1 is a unit.

[Riccardo Brasca]

Which in turn follows from the fact that the Galois conjugate of an algebraic integer are algebraic integers.

[Eric Rodriguez]

some more boring stuff been done, mostly on fleshing out galois_action_on_cyclo so it's not littered with zeros. I like my proof for gal_conj_idempotent:)

[Eric Rodriguez]

on a serious note, I'm not sure what to do about embedding_conj: can we get things as ℚ-alg homs for free somehow?

[Eric Rodriguez]

then we can use power_basis.alg_hom_ext to make things nice

[Eric Rodriguez]

aha, I found docs#ring_hom.to_rat_alg_hom, but both have := φ.to_rat_alg_hom and have := (conj : ℂ →+* ℂ).to_rat_alg_hom get into TC loops :/ is this to do with qsmul and such?

[Eric Rodriguez]

ok, I figured out a workaround anyways. something is weird with the instance caches in that file.

[Eric Rodriguez]

galois_action_on_cyclo is now sorry-free, and Unit_lemmas is only waiting on finishing off this step.

[Riccardo Brasca]

Note that in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Embeddings.20of.20a.20.20number.20field we decided to use ring hom for number fields, rather than Q-alg hom, so we should follow that decision.

[Eric Rodriguez]

Yeah, it was just to use some results temporarily. See the top of galois_action_on_cyclo

[Eric Rodriguez]

Riccardo Brasca said:

Which in turn follows from the fact that the Galois conjugate of an algebraic integer are algebraic integers.

where do you want to put this? may have some time to work on this all today

[Riccardo Brasca]

In the project you can just create a new file, who cares. In mathlib it can go in the same file where is_integral is defined, it doesn't require any Galois theory. If σ : B →ₐ[A] B, where you have an algebra tower R/A/B and x : B is integral over R, then σ x is integral over R. It should be immediate, the minimal polynomial is the same.

[Riccardo Brasca]

Then I think the morally correct thing to do is define a function norm' : 𝓞 K →* 𝓞 K (it follows immediately from docs#algebra.is_integral_norm, but it is annoying to write obtain ... all the time) and prove that x ∈ (𝓞 K)ˣ iff norm' x ∈ (𝓞 K)ˣ.

[Eric Rodriguez]

do we have algebra.norm in terms of the galois group or do I have to write it? there's docs#algebra.norm_eq_prod_embeddings but that doesn't work because that all ends up in a larger extension

[Riccardo Brasca]

I just delegated a PR that does that for the trace

[Riccardo Brasca]

It should be easy to adapt to the norm

[Riccardo Brasca]

I am on mobile, but check the running PR

[Riccardo Brasca]

Or use the product of the roots of the minimal polynomial

[Riccardo Brasca]

#14523

[Eric Rodriguez]

thanks, I'll have a look at this

[Riccardo Brasca]

I've asked to do it for the norm. It should be really the same proof

[Xavier Roblot]

So there is at the moment an ongoing discussion on the best way to prove the formula for the coefficients of a polynomial in terms of its roots from the results in ring_theory.polynomia.vieta (see #1408). Until it is resolved, my PR of mem_roots_of_unity_of_abs_eq_one is on hold.
So is there anything else I can work on in the meantime? I see you guys have been quite busy lately and made some significant progress.

[Riccardo Brasca]

You can coordinate with @Eric Rodriguez to finish the proof of unit_inv_conj_not_neg_zeta_runity. We need that ζ - 1 is prime and it does not divide 2 (both are computation with the norm, we already have docs#is_primitive_root.sub_one_norm_prime_ne_two but we are mising some glue to obtain the two results).

Looking at the blueprint it seems that the only other missing result in sections 1-2-3 is Lemma 3.8, I think we don't even have the statement.

[Riccardo Brasca]

Note that #14523 will be in mathlib in a few hours, with the result about the norm.

[Eric Rodriguez]

Thanks @Iván Sadofschi Costa! I am working on showing (1 - z) is prime, im away from a computer right now but I should push a proof for that by ~ 2022-06-24T16:00:00+01:00

[Eric Rodriguez]

So Xavier, feel free to work on the other stuff (for now, just put it as a sorry that the ideal is prime)

[Eric Rodriguez]

i've finally pushed the unit stuff, sorry!

[Eric Rodriguez]

Riccardo Brasca said:

This follows from the fact that the norm is p, but we need to know that an algebraic integer with norm 1 is a unit.

how does this proof work? I had to return all my paper books now :(

[Riccardo Brasca]

The fact that I = (z-1) is prime? The math proof is that the norm (of the ideal) is p, so if I = AB then the norm of, say, A must be 1. Now I have to think how to prove that this implies that A` is trivial. The point is that ideals are not necessarily principal

[Riccardo Brasca]

It can be possible to avoid speaking of ideals but I have to think about it

[Riccardo Brasca]

Mmm, do we want to develop the theory of the norm of an ideal? Maybe we want

[Kevin Buzzard]

z-1 is prime because if you quotient out by it then you get Z/pZ

[Riccardo Brasca]

Do you have an elementary proof?

[Riccardo Brasca]

Ok, I see

[Kevin Buzzard]

The ideal z-1 can't be trivial because the norm of z-1 is p. In particular p is in the ideal (z-1). Now I claim that every element of Z[z] is of the form a+b(z-1) with a in {0,1,2,..,.p-1}, and the proof is...maybe you see :-)

[Kevin Buzzard]

z^n maps to 1 and p maps to 0 and it's game over.

[Riccardo Brasca]

Yes yes that's what I wanted to say but you're too fast

[Kevin Buzzard]

Still might be a slight challenge to formalise and to be honest I think your ideal argument is better because it's more conceptual so probably will have other uses.

[Kevin Buzzard]

If your definition of norm(I) is "size of R/I" then I think norm(I)=1 implies I=1, but maybe life is not so easy?

[Kevin Buzzard]

I should say that once LTE is out of the way I am looking forward to joining this project. But of course you should all stop working on this project and come and help us finish LTE, all we have left is about 60 statements about abelian categories and they're quite good fun to prove :-)

[Riccardo Brasca]

We have only the norm of an element, with all the basic property

[Riccardo Brasca]

And we know that the norm of 1-z is p

[Riccardo Brasca]

So p is in the ideal

[Riccardo Brasca]

I will try to formalize this tomorrow

[Eric Rodriguez]

Kevin Buzzard said:

I should say that once LTE is out of the way I am looking forward to joining this project. But of course you should all stop working on this project and come and help us finish LTE, all we have left is about 60 statements about abelian categories and they're quite good fun to prove :-)

I tried doing some of the self contained ones once and noped out very hard :b

[Eric Rodriguez]

I think doing the norm of an ideal is a good idea, I thought we had that but maybe we just have that it's finite because of Anne&co's work

[Riccardo Brasca]

I am giving a try to prove that 1-z is prime. It's maybe possible to do it rather directly, so let me see.

[Kevin Buzzard]

Norm prime implies prime of course

[Riccardo Brasca]

Yes, but that requires the norm of an ideal, that we don't have, right? If the norm of an element is prime that the element is irreducible, this is very easy, but primality seems to require a little bit of work.

[Kevin Buzzard]

We need (norm x) = ideal.norm (x)

[Riccardo Brasca]

What I mean is that there is no ideal.norm at all at the moment, unless I missed it.

[Chris Birkbeck]

Is there not? If that's the case maybe I'll try and add that next. It feels like something we should have

[Yaël Dillies]

Can you reuse docs#has_norm?

[Chris Birkbeck]

Or at least start on it

[Riccardo Brasca]

@Yaël Dillies It's called norm but it's a rather different concept, for example it takes value in Z, or even better in the set of ideals.

[Riccardo Brasca]

it's related to docs#algebra.norm

[Eric Rodriguez]

How can the norm take value in the set of ideals? Also I thought it was N-valued (the defn I know is |Z/I|)

[Kevin Buzzard]

There's a "relative" norm on elements N: A -> R for any finite locally free R-algebra A I guess. If R is Noetherian then I guess this is the same as finite flat R-algebra. But for ideal norms I'm a bit more hazy about what's going on.

[Kevin Buzzard]

The example I've taught is this absolute norm which Eric is talking about but this is specific to orders in integers of number fields or function fields

[Riccardo Brasca]

I think I have a Lean proof that 1-z is prime, avoiding the ideal norm. I will finish it after dinner

[Alex J. Best]

I have some work on a definition of the ideal norm, the absolute one at least. So if anyone else wants this we should coordinate a little!

[Riccardo Brasca]

I've proved here that if the norm (@Eric Rodriguez version taking values in the ring of integers) of the generator of an intgral power basis pb of a Galois extension of number fields is prime, then pb.gen is prime.

[Riccardo Brasca]

We need a little bit of glue to prove that z-1 is prime, since we have the integral power basis given by z, not by z-1. Constructing this one only require that the ring of integers is Z[z-1], that should be really easy given that we know it is Z[z].

[Riccardo Brasca]

In any case the proof of prime_of_norm_prime is a nice detour to avoid the ideal norm.

[Riccardo Brasca]

I am done for today, but here is something to do if you're annoyed tonight.

• Prove thatadjoin R {x+a} = adjoin R {x} if a : R.
• Prove the results in docs#number_theory.cyclotomic.rat with ζ replaced by ζ - 1.
• Construct the power_basis ℤ (𝓞 K) given by ζ - 1 as it's done here for ζ (this file should be moved).
• Prove that norm' K (ζ - 1) = (rat.ring_of_integers_equiv.symm p) using docs#is_primitive_root.sub_one_norm_prime.
• Finish the proof that ζ - 1 is prime using prime_of_norm_prime.

[Alex J. Best]

I guess we should have some more general operations on power bases by appropriate affine transformations?

[Riccardo Brasca]

We have docs#power_basis.of_gen_mem_adjoin that is very general. It works for fields, but it is possible that is generalizes more or less automatically.

[Riccardo Brasca]

Mmm, no, it uses docs#algebra.adjoin.power_basis that is false in general.

[Riccardo Brasca]

lemma zeta_sub_one_prime [is_cyclotomic_extension {p ^ (k + 1)} ℚ K]
  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) (hodd : p ≠ 2) :
  prime (⟨ζ - 1, hζ.sub_one_mem_ring_of_integers⟩ : R)

is sorry free.

[Riccardo Brasca]

The simps here is very slow... does anyone know to speed it up?

[Kevin Buzzard]

Did you try the now-standard technique of using simps? to find out what it's doing and then just doing it manually yourself? :-)

[Kevin Buzzard]

I have no idea why simps is sometimes randomly super-slow but you're not the first person to notice it recently.

[Yaël Dillies]

Because simps lemmas have to be in simp normal form, simps calls simp (or just dsimp?) on the LHS, but this sometimes results in oversimplified statements.

[Riccardo Brasca]

Yeah, adding it by hand seems faster.

[Riccardo Brasca]

#14979 and #14981 If someone wants to have a look.

[Riccardo Brasca]

I will have very little time this week, but I will try to follow any progress.

[Chris Birkbeck]

Riccardo Brasca said:

You can coordinate with Eric Rodriguez to finish the proof of unit_inv_conj_not_neg_zeta_runity. We need that ζ - 1 is prime and it does not divide 2 (both are computation with the norm, we already have docs#is_primitive_root.sub_one_norm_prime_ne_two but we are mising some glue to obtain the two results).

Looking at the blueprint it seems that the only other missing result in sections 1-2-3 is Lemma 3.8, I think we don't even have the statement.

I don't think we actually need 3.8, we basically need something slightly easier, so I've updated this on the blueprint.

[Chris Birkbeck]

I'll add the statement in Lean as well.

[Riccardo Brasca]

@Chris Birkbeck have you added Lean statement? It seems something we can prove very quickly

[Chris Birkbeck]

Yes I added both the statement and proved it. Although the statement isnt quite the one I proved, but its the one we need,

[Riccardo Brasca]

Ah sorry, didn't see it. It's not in the graph right?

[Chris Birkbeck]

Ah maybe not. I'll check that!

[Eric Rodriguez]

I've finished unit_inv_conj_not_neg_zeta_runity and therefore unit_lemma_gal_conj is now sorry free. We are in the endgame!

[Chris Birkbeck]

Great! I think we just need to assemble these results into a proof of case 1!

[Riccardo Brasca]

Great job!!

[Riccardo Brasca]

I will write down what exactly is missing this week.

[Eric Rodriguez]

I do think we should try tidy some things before we do that, and try and agree in quite what form we want to state theorems; we have lots of cyclotomic_ring, adjoin ... mixed about everywhere; I think there's probably about 5 different ways we state $\mathcal{O} \left( \mathbb{Q}(\zeta) \right) = \mathbb{Z}[\zeta]$ and it makes shuffling things about painful