# Zulip Chat Archive

## Stream: FLT-regular

### Topic: Project status

#### Riccardo Brasca (Feb 04 2022 at 11:37):

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 of
`zeta`

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 (Feb 04 2022 at 11:42):

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 (Feb 04 2022 at 11:44):

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 (Feb 04 2022 at 11:54):

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 (Feb 04 2022 at 11:56):

`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 (Feb 04 2022 at 11:58):

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 (Feb 04 2022 at 11:59):

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 (Feb 04 2022 at 11:59):

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

#### Chris Birkbeck (Feb 04 2022 at 12:00):

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 (Feb 04 2022 at 12:01):

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

#### Chris Birkbeck (Feb 04 2022 at 12:01):

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

#### Chris Birkbeck (Feb 04 2022 at 12:02):

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 (Feb 04 2022 at 12:03):

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 (Feb 04 2022 at 12:04):

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

#### Eric Rodriguez (Feb 04 2022 at 12:30):

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

#### Eric Rodriguez (Feb 04 2022 at 12:31):

Washington seems to use Herbrand-Ribet

#### Riccardo Brasca (Feb 04 2022 at 12:31):

For case II you mean?

#### Eric Rodriguez (Feb 04 2022 at 12:32):

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

#### Riccardo Brasca (Feb 04 2022 at 12:34):

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 (Feb 04 2022 at 12:34):

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

#### Riccardo Brasca (Feb 04 2022 at 12:37):

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 (Feb 04 2022 at 13:06):

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 (Feb 04 2022 at 13:09):

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

#### Riccardo Brasca (Feb 04 2022 at 13:09):

Maybe `p=3`

is doable, since the ring is norm euclidean

#### Chris Birkbeck (Feb 04 2022 at 13:10):

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

?

#### Riccardo Brasca (Feb 04 2022 at 13:11):

I don't think so. We have it for `n=4`

, that it's easier.

#### Riccardo Brasca (Feb 04 2022 at 13:11):

Let me check

#### Yaël Dillies (Feb 04 2022 at 13:12):

docs#fermat_42 for reference

#### Chris Birkbeck (Feb 04 2022 at 13:13):

`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 (Feb 04 2022 at 13:13):

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 (Feb 04 2022 at 13:13):

(in case I at least)

#### Chris Birkbeck (Feb 04 2022 at 13:15):

Sorry, I meant, case I for `p=3`

isnt hard. Case II for `p=3`

might well be harder

#### Eric Rodriguez (Feb 04 2022 at 13:15):

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 (Feb 04 2022 at 13:16):

Ah yes, case I can very well be elementary

#### Chris Birkbeck (Feb 04 2022 at 13:19):

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 (Feb 04 2022 at 13:21):

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 (Feb 04 2022 at 13:23):

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 (Feb 04 2022 at 13:38):

I'd think this is helpful, for sure

#### Chris Birkbeck (Feb 04 2022 at 13:42):

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 (Feb 04 2022 at 13:42):

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 (Feb 04 2022 at 13:48):

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 (Feb 05 2022 at 06:53):

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 (Feb 05 2022 at 06:54):

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 (Feb 05 2022 at 12:41):

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 (Feb 08 2022 at 16:28):

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 (Feb 08 2022 at 16:28):

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

#### Riccardo Brasca (Feb 08 2022 at 16:32):

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 (Feb 08 2022 at 16:33):

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

#### Riccardo Brasca (Feb 08 2022 at 16:34):

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

#### Eric Rodriguez (Feb 08 2022 at 17:34):

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 (Feb 08 2022 at 17:48):

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 (Feb 08 2022 at 17:49):

(we need both because using `zeta`

we can compute the discriminant, and `zeta - 1`

has eisenstein minimal polynomial).

#### Riccardo Brasca (Feb 08 2022 at 17:50):

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

I think

#### Alex J. Best (Feb 08 2022 at 17:51):

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 (Feb 08 2022 at 17:52):

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 (Feb 08 2022 at 17:53):

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 (Feb 08 2022 at 17:56):

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 (Feb 08 2022 at 18:02):

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 (Feb 08 2022 at 18:04):

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 (Feb 08 2022 at 19:30):

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 (Feb 08 2022 at 19:31):

I think that's missing right now, Kevin

#### Kevin Buzzard (Feb 08 2022 at 19:32):

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

#### Damiano Testa (Feb 08 2022 at 20:29):

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 (Feb 08 2022 at 21:13):

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 (Jul 13 2022 at 14:22):

So section 3 of the blueprint is done.

#### Riccardo Brasca (Jul 13 2022 at 14:23):

The next thing to do is `flt_fact_2`

#### Chris Birkbeck (Jul 13 2022 at 14:23):

Section 3 I guess you mean

#### Riccardo Brasca (Jul 13 2022 at 14:24):

:grinning_face_with_smiling_eyes: yes

#### Riccardo Brasca (Jul 13 2022 at 14:26):

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 (Jul 13 2022 at 15:07):

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 (Jul 13 2022 at 15:11):

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 (Jul 14 2022 at 10:31):

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 (Jul 14 2022 at 19:23):

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 (Jul 14 2022 at 19:23):

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

#### Anne Baanen (Jul 15 2022 at 09:19):

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 (Jul 15 2022 at 09:23):

that would be super helpful, many thanks!

#### Riccardo Brasca (Jul 21 2022 at 08:08):

I am going to remove any mention of `cyclotomic_ring`

from the project, using `𝓞 K`

everywhere.

#### Riccardo Brasca (Jul 21 2022 at 09:03):

@Eric Rodriguez now that the `algebra_rat`

diamond should be fixed, can you have a look at this proof? Thanks!

#### Eric Rodriguez (Jul 21 2022 at 19:31):

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 (Jul 21 2022 at 22:04):

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 (Jul 21 2022 at 22:13):

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

#### Eric Rodriguez (Jul 21 2022 at 22:39):

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 (Jul 21 2022 at 22:40):

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 (Jul 22 2022 at 08:49):

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 (Jul 22 2022 at 08:50):

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 (Jul 22 2022 at 09:12):

4 is in mathlib proper, might just need a link

#### Anne Baanen (Jul 22 2022 at 09:12):

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 (Jul 22 2022 at 09:12):

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

#### Eric Wieser (Jul 22 2022 at 09:13):

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

#### Riccardo Brasca (Jul 22 2022 at 09:13):

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 (Jul 22 2022 at 09:14):

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 (Jul 22 2022 at 09:18):

Wait, how does `rat_algebra`

even apply to splitting_field? I can't see the char_zero instance

#### Anne Baanen (Jul 22 2022 at 09:19):

docs#cyclotomic_field.char_zero

#### Anne Baanen (Jul 22 2022 at 09:22):

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 (Jul 22 2022 at 09:22):

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

#### Eric Wieser (Jul 22 2022 at 09:23):

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

#### Eric Wieser (Jul 22 2022 at 09:24):

(updated)

#### Anne Baanen (Jul 22 2022 at 18:20):

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 (Jul 22 2022 at 20:43):

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 (Jul 24 2022 at 20:15):

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 (Jul 25 2022 at 08:21):

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

#### Anne Baanen (Jul 25 2022 at 08:55):

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 (Jul 25 2022 at 09:24):

Ah right, we don't have a `distrib_mul_action ℚ K`

if `K`

doesn't have characteristic zero...

#### Anne Baanen (Jul 25 2022 at 12:09):

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 (Jul 25 2022 at 12:10):

This is enough to define `polynomial.has_smul`

and is satisfied by the `ℚ`

-action on any division ring.

#### Yaël Dillies (Jul 25 2022 at 12:16):

Let me mention #9123

#### Anne Baanen (Jul 25 2022 at 12:19):

I need a weaker form of `distrib_mul_action`

, this one is too strong! :)

#### Anne Baanen (Jul 25 2022 at 12:20):

Namely, `mul_smul : (a * b : ℚ) \bu x = a \bu x + b \bu x`

doesn't hold outside of characteristic 0.

#### Yaël Dillies (Jul 25 2022 at 12:24):

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

#### Anne Baanen (Jul 25 2022 at 14:38):

Alright, pushed a fix for the diamonds in `splitting_field_aux`

scalar diamonds, let's see what breaks...

#### Eric Rodriguez (Jul 25 2022 at 14:47):

thanks so much for all this work!

#### Anne Baanen (Jul 25 2022 at 15:14):

The `algebra`

instances still aren't quite right...

#### Anne Baanen (Jul 25 2022 at 16:05):

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 (Jul 29 2022 at 10:31):

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 (Jul 29 2022 at 10:31):

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 (Jul 29 2022 at 10:55):

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 (Jul 29 2022 at 10:56):

The file defining algebraic closures definitely imports `splitting_field`

.

#### Anne Baanen (Jul 29 2022 at 10:57):

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 (Jul 29 2022 at 11:00):

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

#### Thomas Browning (Jul 29 2022 at 13:09):

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.adjoin`

ing 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 (Jul 29 2022 at 19:44):

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 (Jul 29 2022 at 20:00):

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 (Jul 29 2022 at 21:33):

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 (Jul 30 2022 at 14:29):

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 (Jul 31 2022 at 01:45):

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

#### Eric Rodriguez (Jul 31 2022 at 01:45):

image.png firstly this definitely isn't helping

#### Eric Rodriguez (Jul 31 2022 at 01:46):

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 (Jul 31 2022 at 01:46):

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

#### Eric Rodriguez (Jul 31 2022 at 01:48):

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 (Jul 31 2022 at 01:49):

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

#### Eric Rodriguez (Jul 31 2022 at 02:18):

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 f`

is 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 (Jul 31 2022 at 02:18):

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 (Jul 31 2022 at 02:18):

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

#### Eric Rodriguez (Jul 31 2022 at 16:45):

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 (Jul 31 2022 at 18:35):

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

#### Eric Rodriguez (Jul 31 2022 at 22:31):

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 (Aug 01 2022 at 09:03):

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 (Aug 01 2022 at 09:05):

@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 (Aug 01 2022 at 09:11):

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

#### Kevin Buzzard (Aug 01 2022 at 09:14):

Yeah I meant K-linear ring hom :-)

#### Junyan Xu (Aug 01 2022 at 09:31):

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 (Aug 05 2022 at 02:52):

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 (Aug 05 2022 at 06:25):

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 (Aug 05 2022 at 06:52):

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

#### Junyan Xu (Aug 05 2022 at 07:03):

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 (Aug 05 2022 at 07:05):

btw I PR'd some lemmas about algebraicity #15873

#### Thomas Browning (Aug 05 2022 at 14:49):

@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 (Aug 05 2022 at 15:09):

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 (Aug 09 2022 at 18:01):

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 (Aug 09 2022 at 18:01):

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

#### Eric Rodriguez (Aug 09 2022 at 18:01):

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

#### Eric Rodriguez (Aug 09 2022 at 18:14):

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 (Aug 09 2022 at 18:14):

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 (Aug 09 2022 at 18:22):

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

#### Anne Baanen (Aug 09 2022 at 19:51):

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

#### Eric Rodriguez (Aug 11 2022 at 01:07):

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 (Aug 11 2022 at 01:07):

I have not yet made this work with `cyclotomic_ring`

but that should likely die in a nice fire

#### Eric Rodriguez (Aug 11 2022 at 01:08):

the flt-regular bump will probably also go this way, with removing many `convert`

s and such like

#### Eric Rodriguez (Aug 11 2022 at 01:10):

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 (Aug 11 2022 at 12:47):

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 (Aug 11 2022 at 15:13):

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

#### Alex J. Best (Aug 11 2022 at 15:18):

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 (Aug 11 2022 at 15:20):

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 (Aug 11 2022 at 16:42):

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 (Aug 11 2022 at 16:44):

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 (Aug 11 2022 at 17:10):

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 (Aug 17 2022 at 11:28):

@Eric Rodriguez are you trying to PR your work?

#### Eric Rodriguez (Aug 17 2022 at 11:30):

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

#### Patrick Johnson (Aug 19 2022 at 05:29):

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 (Nov 15 2022 at 17:02):

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 (Nov 15 2022 at 17:55):

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

#### Riccardo Brasca (Nov 21 2022 at 15:35):

@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 (Nov 21 2022 at 15:35):

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

#### Riccardo Brasca (Nov 21 2022 at 15:41):

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

#### Riccardo Brasca (Nov 21 2022 at 16:14):

@Alex J. Best I forgot what your tactic `may_assume`

does. I think we are not using it.

#### Alex J. Best (Nov 21 2022 at 16:15):

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 (Nov 21 2022 at 16:25):

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 (Nov 21 2022 at 16:30):

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 (Nov 21 2022 at 16:32):

Mmm, maybe it worked for `ℕ`

but not for `ℤ`

, I don't remember exactly.

#### Alex J. Best (Nov 21 2022 at 16:33):

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 (Feb 04 2022 at 11:37):

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 of
`zeta`

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 (Feb 04 2022 at 11:42):

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 (Feb 04 2022 at 11:44):

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 (Feb 04 2022 at 11:54):

`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 (Feb 04 2022 at 11:56):

`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 (Feb 04 2022 at 11:58):

Eric Rodriguez said:

`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 (Feb 04 2022 at 11:59):

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 (Feb 04 2022 at 11:59):

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

#### Chris Birkbeck (Feb 04 2022 at 12:00):

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 (Feb 04 2022 at 12:01):

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

#### Chris Birkbeck (Feb 04 2022 at 12:01):

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

#### Chris Birkbeck (Feb 04 2022 at 12:02):

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 (Feb 04 2022 at 12:03):

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 (Feb 04 2022 at 12:04):

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

#### Eric Rodriguez (Feb 04 2022 at 12:30):

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

#### Eric Rodriguez (Feb 04 2022 at 12:31):

Washington seems to use Herbrand-Ribet

#### Riccardo Brasca (Feb 04 2022 at 12:31):

For case II you mean?

#### Eric Rodriguez (Feb 04 2022 at 12:32):

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

#### Riccardo Brasca (Feb 04 2022 at 12:34):

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 (Feb 04 2022 at 12:34):

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

#### Riccardo Brasca (Feb 04 2022 at 12:37):

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 (Feb 04 2022 at 13:06):

Riccardo Brasca said:

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 (Feb 04 2022 at 13:09):

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

#### Riccardo Brasca (Feb 04 2022 at 13:09):

Maybe `p=3`

is doable, since the ring is norm euclidean

#### Chris Birkbeck (Feb 04 2022 at 13:10):

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

?

#### Riccardo Brasca (Feb 04 2022 at 13:11):

I don't think so. We have it for `n=4`

, that it's easier.

#### Riccardo Brasca (Feb 04 2022 at 13:11):

Let me check

#### Yaël Dillies (Feb 04 2022 at 13:12):

docs#fermat_42 for reference

#### Chris Birkbeck (Feb 04 2022 at 13:13):

`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 (Feb 04 2022 at 13:13):

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 (Feb 04 2022 at 13:13):

(in case I at least)

#### Chris Birkbeck (Feb 04 2022 at 13:15):

Sorry, I meant, case I for `p=3`

isnt hard. Case II for `p=3`

might well be harder

#### Eric Rodriguez (Feb 04 2022 at 13:15):

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 (Feb 04 2022 at 13:16):

Ah yes, case I can very well be elementary

#### Chris Birkbeck (Feb 04 2022 at 13:19):

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 (Feb 04 2022 at 13:21):

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 (Feb 04 2022 at 13:23):

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 (Feb 04 2022 at 13:38):

I'd think this is helpful, for sure

#### Chris Birkbeck (Feb 04 2022 at 13:42):

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 (Feb 04 2022 at 13:42):

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 (Feb 04 2022 at 13:48):

Eric Rodriguez said:

`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 (Feb 05 2022 at 06:53):

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 (Feb 05 2022 at 06:54):

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 (Feb 05 2022 at 12:41):

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 (Feb 08 2022 at 16:28):

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 (Feb 08 2022 at 16:28):

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

#### Riccardo Brasca (Feb 08 2022 at 16:32):

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 (Feb 08 2022 at 16:33):

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

#### Riccardo Brasca (Feb 08 2022 at 16:34):

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

#### Eric Rodriguez (Feb 08 2022 at 17:34):

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 (Feb 08 2022 at 17:48):

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 (Feb 08 2022 at 17:49):

(we need both because using `zeta`

we can compute the discriminant, and `zeta - 1`

has eisenstein minimal polynomial).

#### Riccardo Brasca (Feb 08 2022 at 17:50):

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

I think

#### Alex J. Best (Feb 08 2022 at 17:51):

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 (Feb 08 2022 at 17:52):

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 (Feb 08 2022 at 17:53):

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 (Feb 08 2022 at 17:56):

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 (Feb 08 2022 at 18:02):

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 (Feb 08 2022 at 18:04):

Eric Rodriguez said:

Yeah that's why type ascriptions are normally better, I can see why doing `(n : ℕ)`

isn't super readable to outsiders

#### Kevin Buzzard (Feb 08 2022 at 19:30):

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 (Feb 08 2022 at 19:31):

I think that's missing right now, Kevin

#### Kevin Buzzard (Feb 08 2022 at 19:32):

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

#### Damiano Testa (Feb 08 2022 at 20:29):

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 (Feb 08 2022 at 21:13):

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 (Jul 13 2022 at 14:22):

So section 3 of the blueprint is done.

#### Riccardo Brasca (Jul 13 2022 at 14:23):

The next thing to do is `flt_fact_2`

#### Chris Birkbeck (Jul 13 2022 at 14:23):

Section 3 I guess you mean

#### Riccardo Brasca (Jul 13 2022 at 14:24):

:grinning_face_with_smiling_eyes: yes

#### Riccardo Brasca (Jul 13 2022 at 14:26):

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 (Jul 13 2022 at 15:07):

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 (Jul 13 2022 at 15:11):

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 (Jul 14 2022 at 10:31):

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 (Jul 14 2022 at 19:23):

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 (Jul 14 2022 at 19:23):

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

#### Anne Baanen (Jul 15 2022 at 09:19):

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 (Jul 15 2022 at 09:23):

that would be super helpful, many thanks!

#### Riccardo Brasca (Jul 21 2022 at 08:08):

I am going to remove any mention of `cyclotomic_ring`

from the project, using `𝓞 K`

everywhere.

#### Riccardo Brasca (Jul 21 2022 at 09:03):

@Eric Rodriguez now that the `algebra_rat`

diamond should be fixed, can you have a look at this proof? Thanks!

#### Eric Rodriguez (Jul 21 2022 at 19:31):

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 (Jul 21 2022 at 22:04):

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 (Jul 21 2022 at 22:13):

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

#### Eric Rodriguez (Jul 21 2022 at 22:39):

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 (Jul 21 2022 at 22:40):

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 (Jul 22 2022 at 08:49):

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 (Jul 22 2022 at 08:50):

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 (Jul 22 2022 at 09:12):

4 is in mathlib proper, might just need a link

#### Anne Baanen (Jul 22 2022 at 09:12):

Eric Rodriguez said:

`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 (Jul 22 2022 at 09:12):

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

#### Eric Wieser (Jul 22 2022 at 09:13):

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

#### Riccardo Brasca (Jul 22 2022 at 09:13):

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 (Jul 22 2022 at 09:14):

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 (Jul 22 2022 at 09:18):

Wait, how does `rat_algebra`

even apply to splitting_field? I can't see the char_zero instance

#### Anne Baanen (Jul 22 2022 at 09:19):

docs#cyclotomic_field.char_zero

#### Anne Baanen (Jul 22 2022 at 09:22):

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 (Jul 22 2022 at 09:22):

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

#### Eric Wieser (Jul 22 2022 at 09:23):

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

#### Eric Wieser (Jul 22 2022 at 09:24):

(updated)

#### Anne Baanen (Jul 22 2022 at 18:20):

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 (Jul 22 2022 at 20:43):

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 (Jul 24 2022 at 20:15):

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 (Jul 25 2022 at 08:21):

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

#### Anne Baanen (Jul 25 2022 at 08:55):

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 (Jul 25 2022 at 09:24):

Ah right, we don't have a `distrib_mul_action ℚ K`

if `K`

doesn't have characteristic zero...

#### Anne Baanen (Jul 25 2022 at 12:09):

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 (Jul 25 2022 at 12:10):

This is enough to define `polynomial.has_smul`

and is satisfied by the `ℚ`

-action on any division ring.

#### Yaël Dillies (Jul 25 2022 at 12:16):

Let me mention #9123

#### Anne Baanen (Jul 25 2022 at 12:19):

I need a weaker form of `distrib_mul_action`

, this one is too strong! :)

#### Anne Baanen (Jul 25 2022 at 12:20):

Namely, `mul_smul : (a * b : ℚ) \bu x = a \bu x + b \bu x`

doesn't hold outside of characteristic 0.

#### Yaël Dillies (Jul 25 2022 at 12:24):

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

#### Anne Baanen (Jul 25 2022 at 14:38):

Alright, pushed a fix for the diamonds in `splitting_field_aux`

scalar diamonds, let's see what breaks...

#### Eric Rodriguez (Jul 25 2022 at 14:47):

thanks so much for all this work!

#### Anne Baanen (Jul 25 2022 at 15:14):

The `algebra`

instances still aren't quite right...

#### Anne Baanen (Jul 25 2022 at 16:05):

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 (Jul 29 2022 at 10:31):

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 (Jul 29 2022 at 10:31):

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 (Jul 29 2022 at 10:55):

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 (Jul 29 2022 at 10:56):

The file defining algebraic closures definitely imports `splitting_field`

.

#### Anne Baanen (Jul 29 2022 at 10:57):

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 (Jul 29 2022 at 11:00):

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

#### Thomas Browning (Jul 29 2022 at 13:09):

Kevin Buzzard said:

Actually, I was wondering the same thing. I recently proved that if a polynomial splits, then `intermediate_field.adjoin`

ing 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 (Jul 29 2022 at 19:44):

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 (Jul 29 2022 at 20:00):

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 (Jul 29 2022 at 21:33):

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 (Jul 30 2022 at 14:29):

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 (Jul 31 2022 at 01:45):

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

#### Eric Rodriguez (Jul 31 2022 at 01:45):

image.png firstly this definitely isn't helping

#### Eric Rodriguez (Jul 31 2022 at 01:46):

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 (Jul 31 2022 at 01:46):

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

#### Eric Rodriguez (Jul 31 2022 at 01:48):

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 (Jul 31 2022 at 01:49):

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

#### Eric Rodriguez (Jul 31 2022 at 02:18):

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 f`

is 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 (Jul 31 2022 at 02:18):

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 (Jul 31 2022 at 02:18):

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

#### Eric Rodriguez (Jul 31 2022 at 16:45):

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 (Jul 31 2022 at 18:35):

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

#### Eric Rodriguez (Jul 31 2022 at 22:31):

Anne Baanen said:

`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 (Aug 01 2022 at 09:03):

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 (Aug 01 2022 at 09:05):

@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 (Aug 01 2022 at 09:11):

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

#### Kevin Buzzard (Aug 01 2022 at 09:14):

Yeah I meant K-linear ring hom :-)

#### Junyan Xu (Aug 01 2022 at 09:31):

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 (Aug 05 2022 at 02:52):

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 (Aug 05 2022 at 06:25):

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:

`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 (Aug 05 2022 at 06:52):

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

#### Junyan Xu (Aug 05 2022 at 07:03):

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 (Aug 05 2022 at 07:05):

btw I PR'd some lemmas about algebraicity #15873

#### Thomas Browning (Aug 05 2022 at 14:49):

@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 (Aug 05 2022 at 15:09):

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 (Aug 09 2022 at 18:01):

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 (Aug 09 2022 at 18:01):

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

#### Eric Rodriguez (Aug 09 2022 at 18:01):

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

#### Eric Rodriguez (Aug 09 2022 at 18:14):

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 (Aug 09 2022 at 18:14):

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 (Aug 09 2022 at 18:22):

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

#### Anne Baanen (Aug 09 2022 at 19:51):

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

#### Eric Rodriguez (Aug 11 2022 at 01:07):

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 (Aug 11 2022 at 01:07):

I have not yet made this work with `cyclotomic_ring`

but that should likely die in a nice fire

#### Eric Rodriguez (Aug 11 2022 at 01:08):

the flt-regular bump will probably also go this way, with removing many `convert`

s and such like

#### Eric Rodriguez (Aug 11 2022 at 01:10):

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 (Aug 11 2022 at 12:47):

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 (Aug 11 2022 at 15:13):

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

#### Alex J. Best (Aug 11 2022 at 15:18):

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 (Aug 11 2022 at 15:20):

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 (Aug 11 2022 at 16:42):

Eric Rodriguez said:

`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 (Aug 11 2022 at 16:44):

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 (Aug 11 2022 at 17:10):

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 (Aug 17 2022 at 11:28):

@Eric Rodriguez are you trying to PR your work?

#### Eric Rodriguez (Aug 17 2022 at 11:30):

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

#### Patrick Johnson (Aug 19 2022 at 05:29):

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 (Nov 15 2022 at 17:02):

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 (Nov 15 2022 at 17:55):

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

#### Riccardo Brasca (Nov 21 2022 at 15:35):

@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 (Nov 21 2022 at 15:35):

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

#### Riccardo Brasca (Nov 21 2022 at 15:41):

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

#### Riccardo Brasca (Nov 21 2022 at 16:14):

@Alex J. Best I forgot what your tactic `may_assume`

does. I think we are not using it.

#### Alex J. Best (Nov 21 2022 at 16:15):

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 (Nov 21 2022 at 16:25):

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 (Nov 21 2022 at 16:30):

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 (Nov 21 2022 at 16:32):

Mmm, maybe it worked for `ℕ`

but not for `ℤ`

, I don't remember exactly.

#### Alex J. Best (Nov 21 2022 at 16:33):

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 (May 23 2023 at 14:59):

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!

Last updated: Dec 20 2023 at 11:08 UTC