Project status

Stream: FLT-regular

[Riccardo Brasca]

I think it's time to do a recap of the status of the project.

• The definition and the basic properties of cyclotomic extensions (in full generality) is in mathlib.
• The definition of cyclotomic_fied and cyclotomic_ring is in mathlib.
• The definition ofzeta and its basic properties are in mathlib.
• The structure of the Galois group is PRed.
• The discriminant of $\mathbb{Q}(\zeta_p)$ is PRed.
• I will take care of $\mathcal{O}_{\mathbb{Q}(\zeta_p)} = \mathbb{Z}[\zeta_p]$: the math is almost done in the project, and I already started PRing preliminary results, but just consider this as done.

What should we do next? I am not sure, but suggestions are welcome!

[Chris Birkbeck]

Oh this is great, I just trying to catch up with what's been done. I guess the next big bits are results about elements in the ring of integers, such as these unit lemmas. This should almost be enough for case one.

[Chris Birkbeck]

I was just looking at this and we have things like zeta_unit and zeta_runity . What is the plan for these things? will this be added to the zeta PR eventually, or are we going to remove them completely and work with zeta only? (I've not seen whats in the PR, so maybe this is already all in there)

[Eric Rodriguez]

I think it may be good to start sorrying the full outline of the proof, so we can literally just jump in and solve a sorry. We can certainly start doing this for case I - I still haven't seen a full proof of case II, I'm going to try and grab a copy of Borevich and Shafarevich this weekend and see how close we are now.

[Eric Rodriguez]

zeta_unit, zeta_runity I thought were basically conveniences so we can change/rw them whenever needed - for example, in the Galois group computation I often had to change into ↑↑(root of unity) so that I could apply group lemmas. Now, I'm not sure how much either of them are needed - I'm 99% sure that zeta_unit isn't, and maybe zeta_runity can be replaced by (zeta_primitive_root ...).to_roots_of_unity in most places (and indeed, this is what I did for the galois group, even when using ζ as opposed to a general root of unity)

[Chris Birkbeck]

Eric Rodriguez said:

I think it may be good to start sorrying the full outline of the proof, so we can literally just jump in and solve a sorry. We can certainly start doing this for case I - I still haven't seen a full proof of case II, I'm going to try and grab a copy of Borevich and Shafarevich this weekend and see how close we are now.

There is also a full proof in Washington's book. It does seem like a lot of fiddly lemmas are required.

[Eric Rodriguez]

which one is Washington? if you guys are using that probably easier we grab the same source, and I'm a real sucker for irl books so I'll try grab it at the library

[Chris Birkbeck]

Introduction to Cyclotomic fields by Lawrence Washington. Its what I mainly used for the outline of case 1

[Chris Birkbeck]

But it might not be the best for case II. I'm still looking at several places to see which looks to be the lean-easiest

[Riccardo Brasca]

Case II is far more complicated, we should focus on case I.

[Chris Birkbeck]

There are also these notes by Keith Conrad (https://kconrad.math.uconn.edu/blurbs/gradnumthy/kummer.pdf) which are quite nice.

[Chris Birkbeck]

Riccardo Brasca said:

Case II is far more complicated, we should focus on case I.

Yes I agree. We will need it for case II anyways, so may as well wait.

[Riccardo Brasca]

The problem with Conrad's notes is the he uses the Bernoulli def, and I don't think it's reasonable to have the class number formula in less than a year.

[Chris Birkbeck]

Yeah agreed. I dont think its the lean-easy version we want. Borevich and Shafarevich might be the way to go

[Eric Rodriguez]

I just checked and both B/S and Washington both need the Bernoulli condition, although I think Washington uses some stronger results

[Eric Rodriguez]

Washington seems to use Herbrand-Ribet

[Riccardo Brasca]

For case II you mean?

[Eric Rodriguez]

And I think the case I proof will be the same almost everywhere...

[Riccardo Brasca]

Case II is much complicated than I thought. This is why I think we should concentrate on case I, that is interesting and needed anyway. For case II the most reasonable thing to do seems to be to assume Kummer's lemma (so defining something like "strong regularity"), and proving the theorem. Having Kummer's lemma, the proof can avoid completely Bernoulli numbers I think.

[Riccardo Brasca]

Proving that regularity implies strong regularity is in some sense another project.

[Riccardo Brasca]

In my opinion projects like these one are just an excuse to put stuff into mathlib, so we should not rush towards the result. Sooner or later we will have CFT, L-functions and so on.

[Chris Birkbeck]

Riccardo Brasca said:

Case II is much complicated than I thought. This is why I think we should concentrate on case I, that is interesting and needed anyway. For case II the most reasonable thing to do seems to be to assume Kummer's lemma (so defining something like "strong regularity"), and proving the theorem. Having Kummer's lemma, the proof can avoid completely Bernoulli numbers I think.

Yes the Bernoulli condition is just for Kummer's lemma really. If we assumed this, then we'd get case two with the current definition of regular.

[Riccardo Brasca]

The downside is that we will have zero examples of (strongly) regular primes...

[Riccardo Brasca]

Maybe p=3 is doable, since the ring is norm euclidean

[Chris Birkbeck]

Don't we already have FLT for p=3?

[Riccardo Brasca]

I don't think so. We have it for n=4, that it's easier.

[Riccardo Brasca]

Let me check

[Yaël Dillies]

docs#fermat_42 for reference

[Chris Birkbeck]

p=3 in usually dealt with differently than the other regular primes if I remember correctly. In Washington, its done directly looking modulo 9 I think.

[Riccardo Brasca]

Really? I only know a proof using the 3-rd cyclotomic field (that of course it's a quadratic extension in this case, and even a PID)

[Chris Birkbeck]

(in case I at least)

[Chris Birkbeck]

Sorry, I meant, case I for p=3 isnt hard. Case II for p=3 might well be harder

[Eric Rodriguez]

even if we don't have it, @Ruben Van de Velde has it in his flt repo (I just checked it's sorry-free)

[Riccardo Brasca]

Ah yes, case I can very well be elementary

[Chris Birkbeck]

Ok yeah, case II for p=3 is a long exercise in Washingtons book. But it maybe doesnt need the full machinery that the others do.

[Chris Birkbeck]

Eric Rodriguez said:

even if we don't have it, Ruben Van de Velde has it in his flt repo (I just checked it's sorry-free)

Oh yes nice!

[Ruben Van de Velde]

I was wondering if it was still worth trying to land with your work coming up, but it sounds like maybe it is?

[Eric Rodriguez]

I'd think this is helpful, for sure

[Chris Birkbeck]

Yeah definitely. Some proofs of the regular case assume that p>3 to simplify some things. Although the proof in BS works for any regular prime it seems.

[Riccardo Brasca]

Absolutely! Applying our result to p=3 requires proving that 3 is regular, and even if not very difficult this is not trivial.

[Chris Birkbeck]

Eric Rodriguez said:

I think it may be good to start sorrying the full outline of the proof, so we can literally just jump in and solve a sorry. We can certainly start doing this for case I - I still haven't seen a full proof of case II, I'm going to try and grab a copy of Borevich and Shafarevich this weekend and see how close we are now.

Going back to this, I think this is a good idea. Getting the skeleton of the proof would seem like a good next step.

[Kevin Buzzard]

The n=3 case is done in Hardy and Wright via a descent. They actually prove the rank is 0 over Q(zeta_3) which is easier because then you can do a descent via an isogeny of degree 3 which is defined over this field (the Fermat cubic has CM over this field)

[Kevin Buzzard]

I agree that case 1 would be a really nice milestone. It would prove that lean can actually do basic algebraic number theory and it's already way beyond what is done in any other prover as far as I know

[Riccardo Brasca]

An analogue of Lemma 2.13 of the blueprint is now sorry free.

variables {R : Type u} {S : Type w} {K : Type v} {L : Type z} {p : R}
variables [comm_ring R] [comm_ring S] [algebra R S] [field K] [field L]
variables [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L]

lemma eiseinstein_integral [is_domain R] [normalized_gcd_monoid R] [is_fraction_ring R K]
  [is_integrally_closed R] [is_separable K L] {B : power_basis K L} (hp : prime p)
  (hei : (minpoly R B.gen).is_eisenstein_at 𝓟) (hBint : is_integral R B.gen)
  {z : L} (hzint : is_integral R z) (hz : p • z ∈ adjoin R ({B.gen} : set L)) :
  z ∈ adjoin R ({B.gen} : set L)

Lemma 2.12 is already in mathlib. The final computation about the ring of integer should be quite close now.

[Eric Rodriguez]

I've tried getting started on an outline, but have no more time today to finish it: it's here, and I decided to try and sugar it with as much mathematician-friendly notation as possible :)

[Eric Rodriguez]

Because so little is done, I was more wondering whether people would find this style of file helpful?

[Riccardo Brasca]

I surely like the math-friendly notation!

Concerning is_dedekind_domain ℤ[ζₚ] if someone wants to prove it, just go ahead. What I am proving at the moment is

instance : is_integral_closure (cyclotomic_ring n ℤ ℚ) ℤ (cyclotomic_field n ℚ) := sorry

The Dedekind domain instance should follows easily (the required math is in mathlib).

[Chris Birkbeck]

I also like the notation, it makes to easier to follow!

[Riccardo Brasca]

I will be a little busy tomorrow, but I hope to break the last bit in several small sorrys on Thursday

[Eric Rodriguez]

Oh, the other thing I should flag up is that I'm using an invisible space for the pnat to nat coe, kinda like what LTE does for by exactI.

[Riccardo Brasca]

I am afraid I need at one point the power basis given by zeta - 1. @Eric Rodriguez do you see a way of quickly obtaining it (I only need its existence, and that the generator is zeta - 1) or I have to copy what you did for zeta? It's not that much, but it would be nice to avoid it.

[Riccardo Brasca]

(we need both because using zeta we can compute the discriminant, and zeta - 1 has eisenstein minimal polynomial).

[Riccardo Brasca]

And we also need that the two discriminant are the same.. time to prove it in general for Z I think

[Alex J. Best]

I'm not a huge fan of invisible spaces tbh, is the up arrow or type ascription so bad? It just seems destined to end up confusing someone

[Eric Rodriguez]

Alex, I'm happy to just use some other arrow too, but the normal coe arrow usually gets confused about what I want the coe to go to

[Eric Rodriguez]

And I don't think so Riccardo, they're not conjugates... But maybe the correct generality is some method that adds the basis of something with a power basis + algebra_map t? That should work, I think

[Riccardo Brasca]

The math reason is that they "clearly" generate the same subalgebra. But of course Lean is not very smart :D But no problem I will do it. Maybe making them private or whatever, zeta - 1 is a little less natural than zeta.

[Eric Rodriguez]

I agree, just thought that a power basis for b + algebra_map A B a from a power-basis for b is the correct generality for this, which also gives you your thing

[Alex J. Best]

Eric Rodriguez said:

Alex, I'm happy to just use some other arrow too, but the normal coe arrow usually gets confused about what I want the coe to go to

Yeah that's why type ascriptions are normally better, I can see why doing (n : ℕ) isn't super readable to outsiders

[Kevin Buzzard]

Isn't there going to be some general lemma that if powers of x are a power basis for S/R then so are powers of x + r for r in R?

[Eric Rodriguez]

I think that's missing right now, Kevin

[Kevin Buzzard]

Right -- I'm just suggesting that this is the thing to prove, not that zeta - 1 gives a power basis

[Damiano Testa]

This is only partly related, but something along the lines of what Kevin says is probably not far off from ˋpolynomial.taylor_stuffˋ. Quite a bit of the API is already available and it may be very little work to prove that "taylor of a basis is a basis".

[Riccardo Brasca]

If I am not too tired the right result is the following: if B is a power basis and adjoin R B.gen = adjoin R x then x gives a power basis.

[Riccardo Brasca]

So section 3 of the blueprint is done.

[Riccardo Brasca]

The next thing to do is flt_fact_2

[Chris Birkbeck]

Section 3 I guess you mean

[Riccardo Brasca]

:grinning_face_with_smiling_eyes: yes

[Riccardo Brasca]

But I like @Eric Rodriguez's idea of cleaning up some stuff. I propose to essentially avoid cyclotomic_ring, and just use adjoin

[Riccardo Brasca]

Even better than adjoin we have 𝓞 K. If I am not confused the statement 𝓞 K = adjoin ℤ {ζ} is OK, since both are a ℤ-subalgebra of a given ℚ-cyclotomic extension K.

[Eric Rodriguez]

yes, I think we should definitely just use both! we can maybe have some nice notation for the RHS and then we're all good

[Eric Rodriguez]

I just had to undelete a file whose changes got deleted by accident (note that this commit doesn't show in the master file history) - please all take care with merge commits, it seems to be really easy to hide an important change with them!

[Eric Rodriguez]

it may be good to wait for the big algebra_rat refactor until we carry on with this - there's a lot of rat diamonds lurking in all the stuff we're doing

[Eric Rodriguez]

especially now that we're having to specialize to ℚ more

[Anne Baanen]

I'd be happy to help update to the algebra rat refactor, by the way. Happily, on our quadratic rings project, this was straightforward enough.

[Eric Rodriguez]

that would be super helpful, many thanks!

[Riccardo Brasca]

I am going to remove any mention of cyclotomic_ring from the project, using 𝓞 K everywhere.

[Riccardo Brasca]

@Eric Rodriguez now that the algebra_rat diamond should be fixed, can you have a look at this proof? Thanks!

[Eric Rodriguez]

as far as I understand, actually, there's one more step I over-looked at the time. We have to change one of the field definitions so that the qsmul is convenient (I'm guessing we can't use @[derive field] for cyclotomic_field anymore). Is this correct, @Anne Baanen ?

[Anne Baanen]

If you don't define any has_smul ℚ instances (or module ℚ, algebra ℚ, etc.) on your fields, then you can leave qsmul alone. Otherwise just define the has_smul instance before field and then set qsmul := has_smul.smul and the diamond should be solved.

[Eric Rodriguez]

The qsmul we're worried about is I think the one coming from the splttting field algebra. Let me try this out.

[Eric Rodriguez]

hold up, I'm now a bit confused. The problematic qsmul arises when cyclotomic_field is specialized to ℚ, and so then aren't we creating diamonds in the field instances? Because I don't see any way to set the smul to the correct thing apart from creating another field instance

[Eric Rodriguez]

e.g. this:

@[derive [comm_ring, algebra K, inhabited]]
def cyclotomic_field : Type w := (cyclotomic n K).splitting_field

namespace cyclotomic_field

@[priority 10000] instance field' : field (cyclotomic_field n ℚ) :=
{ qsmul := (•),
  qsmul_eq_mul' := λ a x, sorry,
  .. splitting_field.field (cyclotomic n ℚ) }

[Riccardo Brasca]

I will on holiday for about 10 days, with almost no internet connection, so I am not going to work on the project. In any case now cyclotomic_ring is gone, and also cyclotomic_field is almost gone (it is still there in some proof, and that's OK, but in no statement. We should never have a statement abut cyclotomic_field, only about is_cyclotomic_extension).

[Riccardo Brasca]

Something very easy to do: I see in the graph that flt_fact_4 has green border (that means the statement has been formalized), but there is no link to the Lean code. Is the statement really somewhere or should we make the border blue?

[Ruben Van de Velde]

4 is in mathlib proper, might just need a link

[Anne Baanen]

Eric Rodriguez said:

hold up, I'm now a bit confused. The problematic qsmul arises when cyclotomic_field is specialized to ℚ, and so then aren't we creating diamonds in the field instances? Because I don't see any way to set the smul to the correct thing apart from creating another field instance

Aha, so if the field instance derives from docs#polynomial.splitting_field, then we'll have to fix it in mathlib.

[Anne Baanen]

Indeed docs#polynomial.splitting_field.algebra' already has a comment that we need to fix that instance to avoid diamonds :P

[Eric Wieser]

From what I remember docs#polynomial.splitting_field is pretty cursed, and fixing it is pretty hard

[Riccardo Brasca]

Ruben Van de Velde said:

4 is in mathlib proper, might just need a link

We need better names... flt_fact_4 is not FLT for n=4...

[Anne Baanen]

Eric Wieser said:

From what I remember docs#polynomial.splitting_field is pretty cursed, and fixing it is pretty hard

Because of the recursive construction by induction on the degree?

[Eric Wieser]

Wait, how does rat_algebra even apply to splitting_field? I can't see the char_zero instance

[Anne Baanen]

docs#cyclotomic_field.char_zero

[Anne Baanen]

Ah I see, the problem is like with docs#zmod that the induction should happen per-field, not all at once for the whole structure.

[Eric Wieser]

The induction needs a field structure at each step I think though (the inductive step is docs#adjoin_root.field)

[Eric Wieser]

I just made #15620 to bring the documentation slightly more up to date

[Eric Wieser]

(updated)

[Anne Baanen]

It's time for dinner, and I won't have time to work this weekend. My result up to now is branch#splitting_field-diamond. Bad news is that the diamond is not fixed yet, good news is that it is doable to get rid of all the defeq hacks in docs#polynomial.splitting_field_aux

[Eric Rodriguez]

I'll try have a look in the weekend and see if this is possible, it would be nice to fix this wholly. With luck this is solvable before lean4's eta improvements

[Eric Rodriguez]

I proved the is_scalar_tower instance you had sorried; there seems to be some very weird defeq problems later on in the file that I'm 1000% unqualified to solve alone

[Anne Baanen]

I'm back, let's see how far I get!

[Anne Baanen]

The defeq problems are because we want to construct a has_smul (splitting_field_aux n f) instance recursively, assuming is_scalar_tower + distrib_mul_action on the predecessor (which depends on add_monoid). So first I'll define an add_comm_group instance, then the is_scalar_tower and distrib_mul_action instances, then we should be able to get the recursion going.

[Anne Baanen]

Ah right, we don't have a distrib_mul_action ℚ K if K doesn't have characteristic zero...

[Anne Baanen]

Okay, I'm nearly there. I ended up defining a new typeclass distrib_smul that states smul a distributes over + and 0 on the right hand side.

[Anne Baanen]

This is enough to define polynomial.has_smul and is satisfied by the ℚ-action on any division ring.

[Yaël Dillies]

Let me mention #9123

[Anne Baanen]

I need a weaker form of distrib_mul_action, this one is too strong! :)

[Anne Baanen]

Namely, mul_smul : (a * b : ℚ) \bu x = a \bu x + b \bu x doesn't hold outside of characteristic 0.

[Yaël Dillies]

I'm just mentioning in case you're making it a mixin, because then that would solve my problem too!

[Anne Baanen]

Alright, pushed a fix for the diamonds in splitting_field_aux scalar diamonds, let's see what breaks...

[Eric Rodriguez]

thanks so much for all this work!

[Anne Baanen]

The algebra instances still aren't quite right...

[Anne Baanen]

It's dinner time and I haven't figured out how to solve the algebra diamond yet... The definition of lift should work for the {nat,int,rat}_cast fields but the induction works with an accumulating parameter so it's hard to prove anything about it.

[Anne Baanen]

I've been thinking about this a bit more, the right solution for the algebra_map diamond is probably as follows:

• define lift : K → splitting_field_aux n f by recursion
• define {nat,int,rat}_cast n as lift (↑n)
• define lift_hom as lift bundled into a ring hom
• define algebra'.to_fun as lift_hom \circ algebra_map

[Anne Baanen]

I don't have more than a few hours to work on this in the coming 2 weeks, so hopefully someone else manages to use this plan to fix the diamonds.

[Kevin Buzzard]

I don't think splitting fields are used to define algebraic closures (at least I think I know a way to do alg closures which avoids them), so why not just redefine splitting fields to be a subfield of the algebraic closure?

[Anne Baanen]

The file defining algebraic closures definitely imports splitting_field.

[Anne Baanen]

But indeed it looks like the definition of docs#algebraic_closure currently doesn't directly rely on splitting_field. (It does however do the same kind of recursive definition that will lead to diamonds if we're not careful.)

[Kevin Buzzard]

Aah yes the definition I was thinking of is definitely recursive :-/

[Thomas Browning]

Kevin Buzzard said:

I don't think splitting fields are used to define algebraic closures (at least I think I know a way to do alg closures which avoids them), so why not just redefine splitting fields to be a subfield of the algebraic closure?

Actually, I was wondering the same thing. I recently proved that if a polynomial splits, then intermediate_field.adjoining all of its roots satisfies is_splitting_field (not PRed yet due to dependencies). And if the algebraic closure doesn't depend on splitting field, then this redefinition of splitting field could clean up splitting_field.lean a lot.

[Junyan Xu]

The algebraic closure in mathlib is constructed by adjoining one root $r_f$ of each monic irreducible polynomial $f$ in F[X], quotienting out a maximal ideal to get a field, repeating the above construction, and taking the direct limit. In order for the maximal ideal to exist, the ring obtained by adjoining the roots needs to be nontrivial. And here is where the splitting field comes in: adjoining roots just means taking the mv_polynomial ring on variables $r_f$ and quotienting out by relations $f(r_f)=0$. For any finitely set of relations $f(r_f)=0$, there is a F-alg_hom from the mv_polynomial ring to the splitting field of the product of the $f$'s, whose image is nontrivial (contains F), so the ideal generated by any finitely many relations doesn't contain 1, which implies the ideal generated by all relations is not the whole mv_polynomial ring. For this argument, you can also adjoin one root at a time and use the injectivity of the inclusion of the base ring into adjoin_root f, where you need a generalized version of docs#adjoin_root.coe_injective' for arbitrary comm_ring instead of field but with an additional monic assumption (because after the first step the base ring may no longer be a field, though you can also quotient by a maximal ideal to get a field). This is still an inductive construction, but slightly simpler than splitting_field (no need of factoring out linear factors and taking an irreducible factor).

In fact, one step is enough; there is no need to repeat the "adjoin one root for each monic irreducible polynomial" construction and take the direct limit: if K/F contains one root for each monic irreducible polynomial in F[X], K is already algebraically closed, but the proof uses docs#field.exists_primitive_element and splitting_field as well.

There is another similar construction where instead of adjoining one root, you effectively adjoin all roots of each monic irreducible polynomial in the base field. For this construction, it's easy to prove that one step is enough, since it's easy to show if every monic irreducible polynomial in F[X] splits into linear factors in K/F, then K is algebraically closed; it suffices to use docs#algebra.is_algebraic_trans. However, to show the ideal generated by relations is not the unit ideal for this construction, we really need splitting_field, and the iterative adjoin_root argument doesn't apply.

An option of different flavor is to get an algebraic closure directly by Zorn's lemma. I imagine it would be easier to formalize in Lean, as we have global choice and hence "global Zorn's lemma"; I think the cardinality argument is unnecessary, and you just need to show a field is algebraically closed iff it has no nontrivial algebraic extension in the same universe, which is provided by adjoin_root.

So the conclusion is that if you want to ditch the current splitting_field construction, you need to either use a "totally nonconstructive" proof using Zorn's lemma, or you need to use a weaker iterated adjoin_root construction (and your algebraic closure needs to be an inductive + direct limit construction). I have been thinking about generalizing splitting_field to the "splitting ring" of a monic polynomial over an arbitrary comm_ring, which is useful in https://mathoverflow.net/a/123526/3332 (see (1)=>(2)), so if we decided to use algebraic closure to construct splitting field, we'd better think about how to generalize algebraic closure to comm_ring as well.

[Junyan Xu]

Hmm, it seems it's still necessary to use a cardinality argument; to show that any chain of field extensions has an upper bound, we need to take a direct limit, and that could cause a universe bump, so we need to restrict to field structures on subsets of a fixed type. So the Zorn's lemma argument isn't that simpler after all.

[Kevin Buzzard]

OK then how about renaming current splitting field into splitting_field_really_annoying_to_use_version and then defining splitting field as subfield of alg closure afterwards?

[Eric Rodriguez]

I should have some time today maybe I can try both of these approaches and seeing if any works better with the defeqs or not.

[Eric Rodriguez]

well, this magical "time" I was meant to have evaporated, but there's some stuff I found

[Eric Rodriguez]

image.png firstly this definitely isn't helping

[Eric Rodriguez]

I'll see if I can fix that at that end but I assume this is a problem that requires a similar solution to this one

[Eric Rodriguez]

(thankfully the ℚ instance works, as can also be seen)

[Eric Rodriguez]

this ℤ cast issue goes really far down, because the comm_ring instance is for example defined using docs#ideal.quotient.comm_ring; I guess I have to fix this at the source?

[Eric Rodriguez]

sorry, I'm still figuring this out little by little

[Eric Rodriguez]

okay, final thoughts - the fact that docs#adjoin_root.has_coe_t.has_coe_t ◌nat.cast : ℕ → K isn't defeq to nat.cast : ℕ → adjoin_root fis really annoying. I would appreciate helps on the tips to fix this, because I think if this _was_ true then Anne's proof should work pretty verbatim.

[Eric Rodriguez]

I've pushed some ugly workaround for now, in case this isn't doable and we need to make lemmata for this instead.

[Eric Rodriguez]

(and PS: yes, that name is bad, there's a PR fixing it already)

[Eric Rodriguez]

with much help from @Eric Wieser , I identified some subsidiary diamonds that were making this proof much much harder than it had any right to be. the ℕ one is being fixed in #15778 and the ℤ one is upcoming - merging both of these should make work on this a lit easier!

[Riccardo Brasca]

I am still on holiday, but I promise I will read all your messages on Thursday :smile:

[Eric Rodriguez]

Anne Baanen said:

I've been thinking about this a bit more, the right solution for the algebra_map diamond is probably as follows:

• define lift : K → splitting_field_aux n f by recursion
• define {nat,int,rat}_cast n as lift (↑n)
• define lift_hom as lift bundled into a ring hom
• define algebra'.to_fun as lift_hom \circ algebra_map

update: the branch now has all up to field working. I'm having to make several PRs to fix diamonds that were found along the way + adding casts to everything that's needed. Could you spell out a bit more clearly what you want for the two steps? I think my brain is too much on "fixing code" mode and too little on maths mode to understand what's needed.

[Junyan Xu]

I started doing the Zorn's lemma proof just for fun. Now I've completed half of the proof, namely showing that a maximal element in the preorder of algebraic extensions is algebraically closed. I'm careful not to use the splitting field construction, and it's a bit tricky to show that there can't be any inclusion of a field inside itself that isn't surjective (edit: the inclusion needs to be an alg_hom over a base field over which the field is algebraic); it ends up depending on two missing lemmas that belong to ring_division.lean that I've long thought about adding.

lemma map_roots_le (f : R →+* S) (p : R[X]) (h : p.map f ≠ 0) :
  p.roots.map f ≤ (p.map f).roots := sorry
lemma card_roots_le_map (f : R →+* S) (p : R[X]) (h : p.map f ≠ 0) :
  p.roots.card ≤ (p.map f).roots.card := sorry

See this gist for the WIP so far.

[Kevin Buzzard]

@Sebastian Monnet did you prove this at some stage? IIRC you needed that if $L/K$ was algebraic then any $K$-linear map $L\to L$ was bijective.

[Junyan Xu]

K-linear is not enough (if infinite extension), but K-alg_hom should do.

[Kevin Buzzard]

Yeah I meant K-linear ring hom :-)

[Junyan Xu]

My proof is basically this (though I didn't prove exactly this result): if a K-alg_hom f : L → L is not surjective, take the minimal polynomial p over K of an element a that is not in the image (using algebraicity), which has the minpoly q of a over L as a factor. q has no roots in L, but q.map f has at least one root a. On the other hand, (p/q).map f has at least as many roots (counting multiplicity) in L as p/q (this is true for any ring_hom). So adding them up, p.map f has more roots than p in L. But p.map f = p because f is a K-alg_hom, contradiction.

[Junyan Xu]

Okay I have now completed the Zorn's lemma proof of existence of algebraic closure at https://gist.github.com/alreadydone/daa9760056383d31669755bbb41e2695 It's 334 lines including comments, about the same as file#field_theory/is_alg_closed/algebraic_closure, but some lemmas should go into other files.

It turns out my previous approach doesn't work; it defines the preorder using nonempty (K₁ →ₐ[k] K₂) which is bad, because to take a direct limit you need triangles of k-alg_homs to commute, so they can't be arbitrarily chosen, and there do exist non-identity K ≃ₐ[k] K, for example.

However if you take the underlying types of the extensions to be subsets of a fixed type (coerced to types), then inclusion between subsets gives rise to canonical maps between the subtypes, and you can take the direct limit (which is just a union, but the direct limit API is convenient). And it's really crucial to use a cardinality argument to show a non-algebraically-closed algebraic extension of k carried by a subset of a big enough type big k can be extended to an algebraic extension of k carried by a (strict) superset.

This approach doesn't use splitting field at all, but since the field and algebra instances are obtained by choice, it will require some work to fix the defeq if we want to use it in mathlib.

[Junyan Xu]

Kevin Buzzard said:

Sebastian Monnet did you prove this at some stage? IIRC you needed that if $L/K$ was algebraic then any $K$-linear map $L\to L$ was bijective.

Junyan Xu said:

My proof is basically this (though I didn't prove exactly this result): if a K-alg_hom f : L → L is not surjective, take the minimal polynomial p over K of an element a that is not in the image (using algebraicity), which has the minpoly q of a over L as a factor. q has no roots in L, but q.map f has at least one root a. On the other hand, (p/q).map f has at least as many roots (counting multiplicity) in L as p/q (this is true for any ring_hom). So adding them up, p.map f has more roots than p in L. But p.map f = p because f is a K-alg_hom, contradiction.

There is a much easier proof for this fact and my formalization is under 30 lines; will submit a PR.

[Kevin Buzzard]

Do you end up with a universe bump? Is the algebraic closure in the same universe as the field you started with?

[Junyan Xu]

It's in the same universe, and this is a perfectly valid ZFC proof.
def algebraic_closure : Type u := (exists_alg_closure k).some.carrier

Even if you end up in a higher universe, as long as there's an equiv with some type in the original universe (which exists by cardinality reason), you can transfer the instances (which is done twice in the gist above, but both in the same universe). There's docs#small API to show the existence of an equiv with some type in a certain universe.

[Junyan Xu]

btw I PR'd some lemmas about algebraicity #15873

[Thomas Browning]

@Junyan Xu Let me know if you end up PRing the new algebraic closure construction, because then it would make sense to clean up the splitting field construction.

[Eric Rodriguez]

I don't think we're far from fixing the splitting field construction, I just need to sit down and work on it some day

[Eric Rodriguez]

there's plenty of other issues in the file that need to be fixed, but as far as I can see the diamonds are FINALLY GONE!

[Eric Rodriguez]

if anyone wants to figure out some of them as I'm really tired right now: branch#splitting_field-diamond

[Eric Rodriguez]

thanks for your roadmap @Anne Baanen, it pretty much worked perfectly as described

[Eric Rodriguez]

oh, the file is fixed, I forgot to change the algebra instance from a def to an instance lol. yay! we can finally do flt-regular stuff again

[Eric Rodriguez]

I assume this is going to take a while to get into mathlib, so I suggest instead to run flt-regular off this branch until we merge everything.

[Riccardo Brasca]

I agree, this is much better. We will have time to catch up with new mathlib stuff later on

[Anne Baanen]

Thank you very much @Eric Rodriguez for putting in the work and finishing it!

[Eric Rodriguez]

this is all working super well! if anyone wants to see good signs please look at https://github.com/leanprover-community/mathlib/commit/84e8946a86375e925d0f6bab319b845bbec375ba

[Eric Rodriguez]

I have not yet made this work with cyclotomic_ring but that should likely die in a nice fire

[Eric Rodriguez]

the flt-regular bump will probably also go this way, with removing many converts and such like

[Eric Rodriguez]

thanks to @Bhavik Mehta who suggested a further refactor to Anne's ideas, instead of making lift : (a -> K) -> a -> splitting_field (f : K[X]) we instead have mk : K -> splitting_field (f :K[X]) and then composing with any required a -> Ks. I thought this was required to fix some issues, in the end it wasn't, but it fixed issues that I wasn't expecting, so I think it's probably the correct thing to do.

[Eric Rodriguez]

I've bumped flt_regular to use this branch of mathlib on the branch no_diamonds; it was very easy. I also finished the proof that 2 was regular :)

[Riccardo Brasca]

Feel free to the branch even on master. I don't know how this will interact with the automatic update

[Alex J. Best]

I think the automatic update will just fail and therefore not update, which is fine, we just have to remember to update the no_diamonds branch whenever we want anything new in it until it gets into master

[Eric Rodriguez]

if anyone would like to PR parts of the branch to master I'd really appreciate it, I'm not so sure I will have time to do it. distrib_smul I think is the first thing that should be done there

[Kevin Buzzard]

Eric Rodriguez said:

I've bumped flt_regular to use this branch of mathlib on the branch no_diamonds; it was very easy. I also finished the proof that 2 was regular :)

Wait what's your definition of regular? It's not the conjunction of about 37 things?

[Eric Rodriguez]

class number defn; we'll have to work on the bernoulli one later but we don't need that yet as we're in case 1

[Riccardo Brasca]

The idea is to introduce "strongly regular primes" and prove flt for them. Maybe in 3 years we will know that a prime is regular iff it is strongly regular

[Riccardo Brasca]

@Eric Rodriguez are you trying to PR your work?

[Eric Rodriguez]

I've been busy and computer-less for about a week, hopefully I'll get some time soon :)

[Patrick Johnson]

Regarding the literature: if anyone who wants to work on this project can't proceed due to lacking access to scientific material, please let me know. I have unlimited access to scientific books, papers and journals. I will be happy to share any pdf you need.

[Riccardo Brasca]

I've thought a little bit about what is better to do now, and I think that the fact the port to mathlib4 is really starting and we've just finished caseI is a nice coincidence.

In my (personal) opinion the port is the most important Lean project now, and I will try to spend much of me Lean-time on it. What we can do with our project is try to PR (to mathlib3 of course) as much material as possible. This is surely less fun and interesting than formalizing new mathematics, but it has to be done.

[Chris Birkbeck]

I think this is reasonable. I guess we need to decide what bits we should try to PR

[Riccardo Brasca]

@Eric Rodriguez If you agree I am going to PR what you did about norm' (the norm as an element of the ring of integers). It's a useful notion and it should be in mathlib anyway. Then I think we can simplify certain proofs using the ideal norm that Anne is PRing.

[Eric Rodriguez]

for sure it's okay, sorry i've not done much PRing

[Riccardo Brasca]

Don't worry, it's very low priority stuff.

[Riccardo Brasca]

@Alex J. Best I forgot what your tactic may_assume does. I think we are not using it.

[Alex J. Best]

its a version of wlog that lets you add assumptions like that the numbers giving a solution of the fermat equation are coprime, I think someone rewrote the main file not to use it at some point

[Riccardo Brasca]

Yes, I did it. The tactic was for ℕ instead of ℤ, or something like that, and I felt like a general lemma was better. I am checking if we still use it somewhere.

[Alex J. Best]

Sorry I don't understand, how could a tactic be for N and not Z? Maybe you had some other reason for removing it but that cant be it

[Riccardo Brasca]

Mmm, maybe it worked for ℕ but not for ℤ, I don't remember exactly.

[Alex J. Best]

I just tried a simple example and it works in the same way for the integers as naturals, the internals really don't depend on the type of the expressions involved, its just shuffling goals around

[Riccardo Brasca]

I think it's time to do a recap of the status of the project.

• The definition and the basic properties of cyclotomic extensions (in full generality) is in mathlib.
• The definition of cyclotomic_fied and cyclotomic_ring is in mathlib.
• The definition ofzeta and its basic properties are in mathlib.
• The structure of the Galois group is PRed.
• The discriminant of $\mathbb{Q}(\zeta_p)$ is PRed.
• I will take care of $\mathcal{O}_{\mathbb{Q}(\zeta_p)} = \mathbb{Z}[\zeta_p]$: the math is almost done in the project, and I already started PRing preliminary results, but just consider this as done.

What should we do next? I am not sure, but suggestions are welcome!

[Chris Birkbeck]

Oh this is great, I just trying to catch up with what's been done. I guess the next big bits are results about elements in the ring of integers, such as these unit lemmas. This should almost be enough for case one.

[Chris Birkbeck]

I was just looking at this and we have things like zeta_unit and zeta_runity . What is the plan for these things? will this be added to the zeta PR eventually, or are we going to remove them completely and work with zeta only? (I've not seen whats in the PR, so maybe this is already all in there)

[Eric Rodriguez]

I think it may be good to start sorrying the full outline of the proof, so we can literally just jump in and solve a sorry. We can certainly start doing this for case I - I still haven't seen a full proof of case II, I'm going to try and grab a copy of Borevich and Shafarevich this weekend and see how close we are now.

[Eric Rodriguez]

zeta_unit, zeta_runity I thought were basically conveniences so we can change/rw them whenever needed - for example, in the Galois group computation I often had to change into ↑↑(root of unity) so that I could apply group lemmas. Now, I'm not sure how much either of them are needed - I'm 99% sure that zeta_unit isn't, and maybe zeta_runity can be replaced by (zeta_primitive_root ...).to_roots_of_unity in most places (and indeed, this is what I did for the galois group, even when using ζ as opposed to a general root of unity)

[Chris Birkbeck]

Eric Rodriguez said:

I think it may be good to start sorrying the full outline of the proof, so we can literally just jump in and solve a sorry. We can certainly start doing this for case I - I still haven't seen a full proof of case II, I'm going to try and grab a copy of Borevich and Shafarevich this weekend and see how close we are now.

There is also a full proof in Washington's book. It does seem like a lot of fiddly lemmas are required.

[Eric Rodriguez]

which one is Washington? if you guys are using that probably easier we grab the same source, and I'm a real sucker for irl books so I'll try grab it at the library

[Chris Birkbeck]

Introduction to Cyclotomic fields by Lawrence Washington. Its what I mainly used for the outline of case 1

[Chris Birkbeck]

But it might not be the best for case II. I'm still looking at several places to see which looks to be the lean-easiest

[Riccardo Brasca]

Case II is far more complicated, we should focus on case I.

[Chris Birkbeck]

There are also these notes by Keith Conrad (https://kconrad.math.uconn.edu/blurbs/gradnumthy/kummer.pdf) which are quite nice.

[Chris Birkbeck]

Riccardo Brasca said:

Case II is far more complicated, we should focus on case I.

Yes I agree. We will need it for case II anyways, so may as well wait.

[Riccardo Brasca]

The problem with Conrad's notes is the he uses the Bernoulli def, and I don't think it's reasonable to have the class number formula in less than a year.

[Chris Birkbeck]

Yeah agreed. I dont think its the lean-easy version we want. Borevich and Shafarevich might be the way to go

[Eric Rodriguez]

I just checked and both B/S and Washington both need the Bernoulli condition, although I think Washington uses some stronger results

[Eric Rodriguez]

Washington seems to use Herbrand-Ribet

[Riccardo Brasca]

For case II you mean?

[Eric Rodriguez]

And I think the case I proof will be the same almost everywhere...

[Riccardo Brasca]

Case II is much complicated than I thought. This is why I think we should concentrate on case I, that is interesting and needed anyway. For case II the most reasonable thing to do seems to be to assume Kummer's lemma (so defining something like "strong regularity"), and proving the theorem. Having Kummer's lemma, the proof can avoid completely Bernoulli numbers I think.

[Riccardo Brasca]

Proving that regularity implies strong regularity is in some sense another project.

[Riccardo Brasca]

In my opinion projects like these one are just an excuse to put stuff into mathlib, so we should not rush towards the result. Sooner or later we will have CFT, L-functions and so on.

[Chris Birkbeck]

Riccardo Brasca said:

Case II is much complicated than I thought. This is why I think we should concentrate on case I, that is interesting and needed anyway. For case II the most reasonable thing to do seems to be to assume Kummer's lemma (so defining something like "strong regularity"), and proving the theorem. Having Kummer's lemma, the proof can avoid completely Bernoulli numbers I think.

Yes the Bernoulli condition is just for Kummer's lemma really. If we assumed this, then we'd get case two with the current definition of regular.

[Riccardo Brasca]

The downside is that we will have zero examples of (strongly) regular primes...

[Riccardo Brasca]

Maybe p=3 is doable, since the ring is norm euclidean

[Chris Birkbeck]

Don't we already have FLT for p=3?

[Riccardo Brasca]

I don't think so. We have it for n=4, that it's easier.

[Riccardo Brasca]

Let me check

[Yaël Dillies]

docs#fermat_42 for reference

[Chris Birkbeck]

p=3 in usually dealt with differently than the other regular primes if I remember correctly. In Washington, its done directly looking modulo 9 I think.

[Riccardo Brasca]

Really? I only know a proof using the 3-rd cyclotomic field (that of course it's a quadratic extension in this case, and even a PID)

[Chris Birkbeck]

(in case I at least)

[Chris Birkbeck]

Sorry, I meant, case I for p=3 isnt hard. Case II for p=3 might well be harder

[Eric Rodriguez]

even if we don't have it, @Ruben Van de Velde has it in his flt repo (I just checked it's sorry-free)

[Riccardo Brasca]

Ah yes, case I can very well be elementary

[Chris Birkbeck]

Ok yeah, case II for p=3 is a long exercise in Washingtons book. But it maybe doesnt need the full machinery that the others do.

[Chris Birkbeck]

Eric Rodriguez said:

even if we don't have it, Ruben Van de Velde has it in his flt repo (I just checked it's sorry-free)

Oh yes nice!

[Ruben Van de Velde]

I was wondering if it was still worth trying to land with your work coming up, but it sounds like maybe it is?

[Eric Rodriguez]

I'd think this is helpful, for sure

[Chris Birkbeck]

Yeah definitely. Some proofs of the regular case assume that p>3 to simplify some things. Although the proof in BS works for any regular prime it seems.

[Riccardo Brasca]

Absolutely! Applying our result to p=3 requires proving that 3 is regular, and even if not very difficult this is not trivial.

[Chris Birkbeck]

Eric Rodriguez said:

I think it may be good to start sorrying the full outline of the proof, so we can literally just jump in and solve a sorry. We can certainly start doing this for case I - I still haven't seen a full proof of case II, I'm going to try and grab a copy of Borevich and Shafarevich this weekend and see how close we are now.

Going back to this, I think this is a good idea. Getting the skeleton of the proof would seem like a good next step.

[Kevin Buzzard]

The n=3 case is done in Hardy and Wright via a descent. They actually prove the rank is 0 over Q(zeta_3) which is easier because then you can do a descent via an isogeny of degree 3 which is defined over this field (the Fermat cubic has CM over this field)

[Kevin Buzzard]

I agree that case 1 would be a really nice milestone. It would prove that lean can actually do basic algebraic number theory and it's already way beyond what is done in any other prover as far as I know

[Riccardo Brasca]

An analogue of Lemma 2.13 of the blueprint is now sorry free.

variables {R : Type u} {S : Type w} {K : Type v} {L : Type z} {p : R}
variables [comm_ring R] [comm_ring S] [algebra R S] [field K] [field L]
variables [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L]

lemma eiseinstein_integral [is_domain R] [normalized_gcd_monoid R] [is_fraction_ring R K]
  [is_integrally_closed R] [is_separable K L] {B : power_basis K L} (hp : prime p)
  (hei : (minpoly R B.gen).is_eisenstein_at 𝓟) (hBint : is_integral R B.gen)
  {z : L} (hzint : is_integral R z) (hz : p • z ∈ adjoin R ({B.gen} : set L)) :
  z ∈ adjoin R ({B.gen} : set L)

Lemma 2.12 is already in mathlib. The final computation about the ring of integer should be quite close now.

[Eric Rodriguez]

I've tried getting started on an outline, but have no more time today to finish it: it's here, and I decided to try and sugar it with as much mathematician-friendly notation as possible :)

[Eric Rodriguez]

Because so little is done, I was more wondering whether people would find this style of file helpful?

[Riccardo Brasca]

I surely like the math-friendly notation!

Concerning is_dedekind_domain ℤ[ζₚ] if someone wants to prove it, just go ahead. What I am proving at the moment is

instance : is_integral_closure (cyclotomic_ring n ℤ ℚ) ℤ (cyclotomic_field n ℚ) := sorry

The Dedekind domain instance should follows easily (the required math is in mathlib).

[Chris Birkbeck]

I also like the notation, it makes to easier to follow!

[Riccardo Brasca]

I will be a little busy tomorrow, but I hope to break the last bit in several small sorrys on Thursday

[Eric Rodriguez]

Oh, the other thing I should flag up is that I'm using an invisible space for the pnat to nat coe, kinda like what LTE does for by exactI.

[Riccardo Brasca]

I am afraid I need at one point the power basis given by zeta - 1. @Eric Rodriguez do you see a way of quickly obtaining it (I only need its existence, and that the generator is zeta - 1) or I have to copy what you did for zeta? It's not that much, but it would be nice to avoid it.

[Riccardo Brasca]

(we need both because using zeta we can compute the discriminant, and zeta - 1 has eisenstein minimal polynomial).

[Riccardo Brasca]

And we also need that the two discriminant are the same.. time to prove it in general for Z I think

[Alex J. Best]

I'm not a huge fan of invisible spaces tbh, is the up arrow or type ascription so bad? It just seems destined to end up confusing someone

[Eric Rodriguez]

Alex, I'm happy to just use some other arrow too, but the normal coe arrow usually gets confused about what I want the coe to go to

[Eric Rodriguez]

And I don't think so Riccardo, they're not conjugates... But maybe the correct generality is some method that adds the basis of something with a power basis + algebra_map t? That should work, I think

[Riccardo Brasca]

The math reason is that they "clearly" generate the same subalgebra. But of course Lean is not very smart :D But no problem I will do it. Maybe making them private or whatever, zeta - 1 is a little less natural than zeta.

[Eric Rodriguez]

I agree, just thought that a power basis for b + algebra_map A B a from a power-basis for b is the correct generality for this, which also gives you your thing

[Alex J. Best]

Eric Rodriguez said:

Alex, I'm happy to just use some other arrow too, but the normal coe arrow usually gets confused about what I want the coe to go to

Yeah that's why type ascriptions are normally better, I can see why doing (n : ℕ) isn't super readable to outsiders

[Kevin Buzzard]

Isn't there going to be some general lemma that if powers of x are a power basis for S/R then so are powers of x + r for r in R?

[Eric Rodriguez]

I think that's missing right now, Kevin

[Kevin Buzzard]

Right -- I'm just suggesting that this is the thing to prove, not that zeta - 1 gives a power basis

[Damiano Testa]

This is only partly related, but something along the lines of what Kevin says is probably not far off from ˋpolynomial.taylor_stuffˋ. Quite a bit of the API is already available and it may be very little work to prove that "taylor of a basis is a basis".

[Riccardo Brasca]

If I am not too tired the right result is the following: if B is a power basis and adjoin R B.gen = adjoin R x then x gives a power basis.

[Riccardo Brasca]

So section 3 of the blueprint is done.

[Riccardo Brasca]

The next thing to do is flt_fact_2

[Chris Birkbeck]

Section 3 I guess you mean

[Riccardo Brasca]

:grinning_face_with_smiling_eyes: yes

[Riccardo Brasca]

But I like @Eric Rodriguez's idea of cleaning up some stuff. I propose to essentially avoid cyclotomic_ring, and just use adjoin

[Riccardo Brasca]

Even better than adjoin we have 𝓞 K. If I am not confused the statement 𝓞 K = adjoin ℤ {ζ} is OK, since both are a ℤ-subalgebra of a given ℚ-cyclotomic extension K.

[Eric Rodriguez]

yes, I think we should definitely just use both! we can maybe have some nice notation for the RHS and then we're all good

[Eric Rodriguez]

I just had to undelete a file whose changes got deleted by accident (note that this commit doesn't show in the master file history) - please all take care with merge commits, it seems to be really easy to hide an important change with them!

[Eric Rodriguez]

it may be good to wait for the big algebra_rat refactor until we carry on with this - there's a lot of rat diamonds lurking in all the stuff we're doing

[Eric Rodriguez]

especially now that we're having to specialize to ℚ more

[Anne Baanen]

I'd be happy to help update to the algebra rat refactor, by the way. Happily, on our quadratic rings project, this was straightforward enough.

[Eric Rodriguez]

that would be super helpful, many thanks!

[Riccardo Brasca]

I am going to remove any mention of cyclotomic_ring from the project, using 𝓞 K everywhere.

[Riccardo Brasca]

@Eric Rodriguez now that the algebra_rat diamond should be fixed, can you have a look at this proof? Thanks!

[Eric Rodriguez]

as far as I understand, actually, there's one more step I over-looked at the time. We have to change one of the field definitions so that the qsmul is convenient (I'm guessing we can't use @[derive field] for cyclotomic_field anymore). Is this correct, @Anne Baanen ?

[Anne Baanen]

If you don't define any has_smul ℚ instances (or module ℚ, algebra ℚ, etc.) on your fields, then you can leave qsmul alone. Otherwise just define the has_smul instance before field and then set qsmul := has_smul.smul and the diamond should be solved.

[Eric Rodriguez]

The qsmul we're worried about is I think the one coming from the splttting field algebra. Let me try this out.

[Eric Rodriguez]

hold up, I'm now a bit confused. The problematic qsmul arises when cyclotomic_field is specialized to ℚ, and so then aren't we creating diamonds in the field instances? Because I don't see any way to set the smul to the correct thing apart from creating another field instance

[Eric Rodriguez]

e.g. this:

@[derive [comm_ring, algebra K, inhabited]]
def cyclotomic_field : Type w := (cyclotomic n K).splitting_field

namespace cyclotomic_field

@[priority 10000] instance field' : field (cyclotomic_field n ℚ) :=
{ qsmul := (•),
  qsmul_eq_mul' := λ a x, sorry,
  .. splitting_field.field (cyclotomic n ℚ) }

[Riccardo Brasca]

I will on holiday for about 10 days, with almost no internet connection, so I am not going to work on the project. In any case now cyclotomic_ring is gone, and also cyclotomic_field is almost gone (it is still there in some proof, and that's OK, but in no statement. We should never have a statement abut cyclotomic_field, only about is_cyclotomic_extension).

[Riccardo Brasca]

Something very easy to do: I see in the graph that flt_fact_4 has green border (that means the statement has been formalized), but there is no link to the Lean code. Is the statement really somewhere or should we make the border blue?

[Ruben Van de Velde]

4 is in mathlib proper, might just need a link

[Anne Baanen]

Eric Rodriguez said:

hold up, I'm now a bit confused. The problematic qsmul arises when cyclotomic_field is specialized to ℚ, and so then aren't we creating diamonds in the field instances? Because I don't see any way to set the smul to the correct thing apart from creating another field instance

Aha, so if the field instance derives from docs#polynomial.splitting_field, then we'll have to fix it in mathlib.

[Anne Baanen]

Indeed docs#polynomial.splitting_field.algebra' already has a comment that we need to fix that instance to avoid diamonds :P

[Eric Wieser]

From what I remember docs#polynomial.splitting_field is pretty cursed, and fixing it is pretty hard

[Riccardo Brasca]

Ruben Van de Velde said:

4 is in mathlib proper, might just need a link

We need better names... flt_fact_4 is not FLT for n=4...

[Anne Baanen]

Eric Wieser said:

From what I remember docs#polynomial.splitting_field is pretty cursed, and fixing it is pretty hard

Because of the recursive construction by induction on the degree?

[Eric Wieser]

Wait, how does rat_algebra even apply to splitting_field? I can't see the char_zero instance

[Anne Baanen]

docs#cyclotomic_field.char_zero

[Anne Baanen]

Ah I see, the problem is like with docs#zmod that the induction should happen per-field, not all at once for the whole structure.

[Eric Wieser]

The induction needs a field structure at each step I think though (the inductive step is docs#adjoin_root.field)

[Eric Wieser]

I just made #15620 to bring the documentation slightly more up to date

[Eric Wieser]

(updated)

[Anne Baanen]

It's time for dinner, and I won't have time to work this weekend. My result up to now is branch#splitting_field-diamond. Bad news is that the diamond is not fixed yet, good news is that it is doable to get rid of all the defeq hacks in docs#polynomial.splitting_field_aux

[Eric Rodriguez]

I'll try have a look in the weekend and see if this is possible, it would be nice to fix this wholly. With luck this is solvable before lean4's eta improvements

[Eric Rodriguez]

I proved the is_scalar_tower instance you had sorried; there seems to be some very weird defeq problems later on in the file that I'm 1000% unqualified to solve alone

[Anne Baanen]

I'm back, let's see how far I get!

[Anne Baanen]

The defeq problems are because we want to construct a has_smul (splitting_field_aux n f) instance recursively, assuming is_scalar_tower + distrib_mul_action on the predecessor (which depends on add_monoid). So first I'll define an add_comm_group instance, then the is_scalar_tower and distrib_mul_action instances, then we should be able to get the recursion going.

[Anne Baanen]

Ah right, we don't have a distrib_mul_action ℚ K if K doesn't have characteristic zero...

[Anne Baanen]

Okay, I'm nearly there. I ended up defining a new typeclass distrib_smul that states smul a distributes over + and 0 on the right hand side.

[Anne Baanen]

This is enough to define polynomial.has_smul and is satisfied by the ℚ-action on any division ring.

[Yaël Dillies]

Let me mention #9123

[Anne Baanen]

I need a weaker form of distrib_mul_action, this one is too strong! :)

[Anne Baanen]

Namely, mul_smul : (a * b : ℚ) \bu x = a \bu x + b \bu x doesn't hold outside of characteristic 0.

[Yaël Dillies]

I'm just mentioning in case you're making it a mixin, because then that would solve my problem too!

[Anne Baanen]

Alright, pushed a fix for the diamonds in splitting_field_aux scalar diamonds, let's see what breaks...

[Eric Rodriguez]

thanks so much for all this work!

[Anne Baanen]

The algebra instances still aren't quite right...

[Anne Baanen]

It's dinner time and I haven't figured out how to solve the algebra diamond yet... The definition of lift should work for the {nat,int,rat}_cast fields but the induction works with an accumulating parameter so it's hard to prove anything about it.

[Anne Baanen]

I've been thinking about this a bit more, the right solution for the algebra_map diamond is probably as follows:

• define lift : K → splitting_field_aux n f by recursion
• define {nat,int,rat}_cast n as lift (↑n)
• define lift_hom as lift bundled into a ring hom
• define algebra'.to_fun as lift_hom \circ algebra_map

[Anne Baanen]

I don't have more than a few hours to work on this in the coming 2 weeks, so hopefully someone else manages to use this plan to fix the diamonds.

[Kevin Buzzard]

I don't think splitting fields are used to define algebraic closures (at least I think I know a way to do alg closures which avoids them), so why not just redefine splitting fields to be a subfield of the algebraic closure?

[Anne Baanen]

The file defining algebraic closures definitely imports splitting_field.

[Anne Baanen]

But indeed it looks like the definition of docs#algebraic_closure currently doesn't directly rely on splitting_field. (It does however do the same kind of recursive definition that will lead to diamonds if we're not careful.)

[Kevin Buzzard]

Aah yes the definition I was thinking of is definitely recursive :-/

[Thomas Browning]

Kevin Buzzard said:

I don't think splitting fields are used to define algebraic closures (at least I think I know a way to do alg closures which avoids them), so why not just redefine splitting fields to be a subfield of the algebraic closure?

Actually, I was wondering the same thing. I recently proved that if a polynomial splits, then intermediate_field.adjoining all of its roots satisfies is_splitting_field (not PRed yet due to dependencies). And if the algebraic closure doesn't depend on splitting field, then this redefinition of splitting field could clean up splitting_field.lean a lot.

[Junyan Xu]

The algebraic closure in mathlib is constructed by adjoining one root $r_f$ of each monic irreducible polynomial $f$ in F[X], quotienting out a maximal ideal to get a field, repeating the above construction, and taking the direct limit. In order for the maximal ideal to exist, the ring obtained by adjoining the roots needs to be nontrivial. And here is where the splitting field comes in: adjoining roots just means taking the mv_polynomial ring on variables $r_f$ and quotienting out by relations $f(r_f)=0$. For any finitely set of relations $f(r_f)=0$, there is a F-alg_hom from the mv_polynomial ring to the splitting field of the product of the $f$'s, whose image is nontrivial (contains F), so the ideal generated by any finitely many relations doesn't contain 1, which implies the ideal generated by all relations is not the whole mv_polynomial ring. For this argument, you can also adjoin one root at a time and use the injectivity of the inclusion of the base ring into adjoin_root f, where you need a generalized version of docs#adjoin_root.coe_injective' for arbitrary comm_ring instead of field but with an additional monic assumption (because after the first step the base ring may no longer be a field, though you can also quotient by a maximal ideal to get a field). This is still an inductive construction, but slightly simpler than splitting_field (no need of factoring out linear factors and taking an irreducible factor).

In fact, one step is enough; there is no need to repeat the "adjoin one root for each monic irreducible polynomial" construction and take the direct limit: if K/F contains one root for each monic irreducible polynomial in F[X], K is already algebraically closed, but the proof uses docs#field.exists_primitive_element and splitting_field as well.

There is another similar construction where instead of adjoining one root, you effectively adjoin all roots of each monic irreducible polynomial in the base field. For this construction, it's easy to prove that one step is enough, since it's easy to show if every monic irreducible polynomial in F[X] splits into linear factors in K/F, then K is algebraically closed; it suffices to use docs#algebra.is_algebraic_trans. However, to show the ideal generated by relations is not the unit ideal for this construction, we really need splitting_field, and the iterative adjoin_root argument doesn't apply.

An option of different flavor is to get an algebraic closure directly by Zorn's lemma. I imagine it would be easier to formalize in Lean, as we have global choice and hence "global Zorn's lemma"; I think the cardinality argument is unnecessary, and you just need to show a field is algebraically closed iff it has no nontrivial algebraic extension in the same universe, which is provided by adjoin_root.

So the conclusion is that if you want to ditch the current splitting_field construction, you need to either use a "totally nonconstructive" proof using Zorn's lemma, or you need to use a weaker iterated adjoin_root construction (and your algebraic closure needs to be an inductive + direct limit construction). I have been thinking about generalizing splitting_field to the "splitting ring" of a monic polynomial over an arbitrary comm_ring, which is useful in https://mathoverflow.net/a/123526/3332 (see (1)=>(2)), so if we decided to use algebraic closure to construct splitting field, we'd better think about how to generalize algebraic closure to comm_ring as well.

[Junyan Xu]

Hmm, it seems it's still necessary to use a cardinality argument; to show that any chain of field extensions has an upper bound, we need to take a direct limit, and that could cause a universe bump, so we need to restrict to field structures on subsets of a fixed type. So the Zorn's lemma argument isn't that simpler after all.

[Kevin Buzzard]

OK then how about renaming current splitting field into splitting_field_really_annoying_to_use_version and then defining splitting field as subfield of alg closure afterwards?

[Eric Rodriguez]

I should have some time today maybe I can try both of these approaches and seeing if any works better with the defeqs or not.

[Eric Rodriguez]

well, this magical "time" I was meant to have evaporated, but there's some stuff I found

[Eric Rodriguez]

image.png firstly this definitely isn't helping

[Eric Rodriguez]

I'll see if I can fix that at that end but I assume this is a problem that requires a similar solution to this one

[Eric Rodriguez]

(thankfully the ℚ instance works, as can also be seen)

[Eric Rodriguez]

this ℤ cast issue goes really far down, because the comm_ring instance is for example defined using docs#ideal.quotient.comm_ring; I guess I have to fix this at the source?

[Eric Rodriguez]

sorry, I'm still figuring this out little by little

[Eric Rodriguez]

okay, final thoughts - the fact that docs#adjoin_root.has_coe_t.has_coe_t ◌nat.cast : ℕ → K isn't defeq to nat.cast : ℕ → adjoin_root fis really annoying. I would appreciate helps on the tips to fix this, because I think if this _was_ true then Anne's proof should work pretty verbatim.

[Eric Rodriguez]

I've pushed some ugly workaround for now, in case this isn't doable and we need to make lemmata for this instead.

[Eric Rodriguez]

(and PS: yes, that name is bad, there's a PR fixing it already)

[Eric Rodriguez]

with much help from @Eric Wieser , I identified some subsidiary diamonds that were making this proof much much harder than it had any right to be. the ℕ one is being fixed in #15778 and the ℤ one in #15779- merging both of these should make work on this a lot easier! (I have provisionally merged them into the splitting_field-diamond branch)

[Riccardo Brasca]

I am still on holiday, but I promise I will read all your messages on Thursday :smile:

[Eric Rodriguez]

Anne Baanen said:

I've been thinking about this a bit more, the right solution for the algebra_map diamond is probably as follows:

• define lift : K → splitting_field_aux n f by recursion
• define {nat,int,rat}_cast n as lift (↑n)
• define lift_hom as lift bundled into a ring hom
• define algebra'.to_fun as lift_hom \circ algebra_map

update: the branch now has all up to field working. I'm having to make several PRs to fix diamonds that were found along the way + adding casts to everything that's needed. Could you spell out a bit more clearly what you want for the two steps? I think my brain is too much on "fixing code" mode and too little on maths mode to understand what's needed.

[Junyan Xu]

I started doing the Zorn's lemma proof just for fun. Now I've completed half of the proof, namely showing that a maximal element in the preorder of algebraic extensions is algebraically closed. I'm careful not to use the splitting field construction, and it's a bit tricky to show that there can't be any inclusion of a field inside itself that isn't surjective (edit: the inclusion needs to be an alg_hom over a base field over which the field is algebraic); it ends up depending on two missing lemmas that belong to ring_division.lean that I've long thought about adding.

lemma map_roots_le (f : R →+* S) (p : R[X]) (h : p.map f ≠ 0) :
  p.roots.map f ≤ (p.map f).roots := sorry
lemma card_roots_le_map (f : R →+* S) (p : R[X]) (h : p.map f ≠ 0) :
  p.roots.card ≤ (p.map f).roots.card := sorry

See this gist for the WIP so far.

[Kevin Buzzard]

@Sebastian Monnet did you prove this at some stage? IIRC you needed that if $L/K$ was algebraic then any $K$-linear map $L\to L$ was bijective.

[Junyan Xu]

K-linear is not enough (if infinite extension), but K-alg_hom should do.

[Kevin Buzzard]

Yeah I meant K-linear ring hom :-)

[Junyan Xu]

My proof is basically this (though I didn't prove exactly this result): if a K-alg_hom f : L → L is not surjective, take the minimal polynomial p over K of an element a that is not in the image (using algebraicity), which has the minpoly q of a over L as a factor. q has no roots in L, but q.map f has at least one root a. On the other hand, (p/q).map f has at least as many roots (counting multiplicity) in L as p/q (this is true for any ring_hom). So adding them up, p.map f has more roots than p in L. But p.map f = p because f is a K-alg_hom, contradiction.

[Junyan Xu]

Okay I have now completed the Zorn's lemma proof of existence of algebraic closure at https://gist.github.com/alreadydone/daa9760056383d31669755bbb41e2695 It's 334 lines including comments, about the same as file#field_theory/is_alg_closed/algebraic_closure, but some lemmas should go into other files.

It turns out my previous approach doesn't work; it defines the preorder using nonempty (K₁ →ₐ[k] K₂) which is bad, because to take a direct limit you need triangles of k-alg_homs to commute, so they can't be arbitrarily chosen, and there do exist non-identity K ≃ₐ[k] K, for example.

However if you take the underlying types of the extensions to be subsets of a fixed type (coerced to types), then inclusion between subsets gives rise to canonical maps between the subtypes, and you can take the direct limit (which is just a union, but the direct limit API is convenient). And it's really crucial to use a cardinality argument to show a non-algebraically-closed algebraic extension of k carried by a subset of a big enough type big k can be extended to an algebraic extension of k carried by a (strict) superset.

This approach doesn't use splitting field at all, but since the field and algebra instances are obtained by choice, it will require some work to fix the defeq if we want to use it in mathlib.

[Junyan Xu]

Kevin Buzzard said:

Sebastian Monnet did you prove this at some stage? IIRC you needed that if $L/K$ was algebraic then any $K$-linear map $L\to L$ was bijective.

Junyan Xu said:

My proof is basically this (though I didn't prove exactly this result): if a K-alg_hom f : L → L is not surjective, take the minimal polynomial p over K of an element a that is not in the image (using algebraicity), which has the minpoly q of a over L as a factor. q has no roots in L, but q.map f has at least one root a. On the other hand, (p/q).map f has at least as many roots (counting multiplicity) in L as p/q (this is true for any ring_hom). So adding them up, p.map f has more roots than p in L. But p.map f = p because f is a K-alg_hom, contradiction.

There is a much easier proof for this fact and my formalization is under 30 lines; will submit a PR.

[Kevin Buzzard]

Do you end up with a universe bump? Is the algebraic closure in the same universe as the field you started with?

[Junyan Xu]

It's in the same universe, and this is a perfectly valid ZFC proof.
def algebraic_closure : Type u := (exists_alg_closure k).some.carrier

Even if you end up in a higher universe, as long as there's an equiv with some type in the original universe (which exists by cardinality reason), you can transfer the instances (which is done three times in the gist above, but all in the same universe). There's docs#small API to show the existence of an equiv with some type in a certain universe.

[Junyan Xu]

btw I PR'd some lemmas about algebraicity #15873

[Thomas Browning]

@Junyan Xu Let me know if you end up PRing the new algebraic closure construction, because then it would make sense to clean up the splitting field construction.

[Eric Rodriguez]

I don't think we're far from fixing the splitting field construction, I just need to sit down and work on it some day

[Eric Rodriguez]

there's plenty of other issues in the file that need to be fixed, but as far as I can see the diamonds are FINALLY GONE!

[Eric Rodriguez]

if anyone wants to figure out some of them as I'm really tired right now: branch#splitting_field-diamond

[Eric Rodriguez]

thanks for your roadmap @Anne Baanen, it pretty much worked perfectly as described

[Eric Rodriguez]

oh, the file is fixed, I forgot to change the algebra instance from a def to an instance lol. yay! we can finally do flt-regular stuff again

[Eric Rodriguez]

I assume this is going to take a while to get into mathlib, so I suggest instead to run flt-regular off this branch until we merge everything.

[Riccardo Brasca]

I agree, this is much better. We will have time to catch up with new mathlib stuff later on

[Anne Baanen]

Thank you very much @Eric Rodriguez for putting in the work and finishing it!

[Eric Rodriguez]

this is all working super well! if anyone wants to see good signs please look at https://github.com/leanprover-community/mathlib/commit/84e8946a86375e925d0f6bab319b845bbec375ba

[Eric Rodriguez]

I have not yet made this work with cyclotomic_ring but that should likely die in a nice fire

[Eric Rodriguez]

the flt-regular bump will probably also go this way, with removing many converts and such like

[Eric Rodriguez]

thanks to @Bhavik Mehta who suggested a further refactor to Anne's ideas, instead of making lift : (a -> K) -> a -> splitting_field (f : K[X]) we instead have mk : K -> splitting_field (f :K[X]) and then composing with any required a -> Ks. I thought this was required to fix some issues, in the end it wasn't, but it fixed issues that I wasn't expecting, so I think it's probably the correct thing to do.

[Eric Rodriguez]

I've bumped flt_regular to use this branch of mathlib on the branch no_diamonds; it was very easy. I also finished the proof that 2 was regular :)

[Riccardo Brasca]

Feel free to the branch even on master. I don't know how this will interact with the automatic update

[Alex J. Best]

I think the automatic update will just fail and therefore not update, which is fine, we just have to remember to update the no_diamonds branch whenever we want anything new in it until it gets into master

[Eric Rodriguez]

if anyone would like to PR parts of the branch to master I'd really appreciate it, I'm not so sure I will have time to do it. distrib_smul I think is the first thing that should be done there

[Kevin Buzzard]

Eric Rodriguez said:

I've bumped flt_regular to use this branch of mathlib on the branch no_diamonds; it was very easy. I also finished the proof that 2 was regular :)

Wait what's your definition of regular? It's not the conjunction of about 37 things?

[Eric Rodriguez]

class number defn; we'll have to work on the bernoulli one later but we don't need that yet as we're in case 1

[Riccardo Brasca]

The idea is to introduce "strongly regular primes" and prove flt for them. Maybe in 3 years we will know that a prime is regular iff it is strongly regular

[Riccardo Brasca]

@Eric Rodriguez are you trying to PR your work?

[Eric Rodriguez]

I've been busy and computer-less for about a week, hopefully I'll get some time soon :)

[Patrick Johnson]

Regarding the literature: if anyone who wants to work on this project can't proceed due to lacking access to scientific material, please let me know. I have unlimited access to scientific books, papers and journals. I will be happy to share any pdf you need.

[Riccardo Brasca]

I've thought a little bit about what is better to do now, and I think that the fact the port to mathlib4 is really starting and we've just finished caseI is a nice coincidence.

In my (personal) opinion the port is the most important Lean project now, and I will try to spend much of me Lean-time on it. What we can do with our project is try to PR (to mathlib3 of course) as much material as possible. This is surely less fun and interesting than formalizing new mathematics, but it has to be done.

[Chris Birkbeck]

I think this is reasonable. I guess we need to decide what bits we should try to PR

[Riccardo Brasca]

@Eric Rodriguez If you agree I am going to PR what you did about norm' (the norm as an element of the ring of integers). It's a useful notion and it should be in mathlib anyway. Then I think we can simplify certain proofs using the ideal norm that Anne is PRing.

[Eric Rodriguez]

for sure it's okay, sorry i've not done much PRing

[Riccardo Brasca]

Don't worry, it's very low priority stuff.

[Riccardo Brasca]

@Alex J. Best I forgot what your tactic may_assume does. I think we are not using it.

[Alex J. Best]

its a version of wlog that lets you add assumptions like that the numbers giving a solution of the fermat equation are coprime, I think someone rewrote the main file not to use it at some point

[Riccardo Brasca]

Yes, I did it. The tactic was for ℕ instead of ℤ, or something like that, and I felt like a general lemma was better. I am checking if we still use it somewhere.

[Alex J. Best]

Sorry I don't understand, how could a tactic be for N and not Z? Maybe you had some other reason for removing it but that cant be it

[Riccardo Brasca]

Mmm, maybe it worked for ℕ but not for ℤ, I don't remember exactly.

[Alex J. Best]

I just tried a simple example and it works in the same way for the integers as naturals, the internals really don't depend on the type of the expressions involved, its just shuffling goals around

[Eric Rodriguez]

So a quick update for everyone about the status of the project:

The diamond

The diamond relating to splitting fields has finally been fixed, and we have merged these fixes into FLT-regular. We have pretty much eliminated all instance-related converts! I am currently doing a little bit more related tidying to do with localised instances, and this should hopefully make the codebase easier to use. (see #19067, it's a small PR, and then related tidying will happen in the repository). I will be writing a blogpost about how this diamond was fixed in the near-future, so stay tuned!

The port

The port is not too far from flt-regular content, and as soon as all that is ported, we will work on getting flt-regular into Lean4! Hopefully this doesn't run into too many issues. Case II development will then hopefully resume after the port is done :)

The paper

For ITP, we worked on a short paper about the project - it's now on the arXiv if you'd all like to check it out!