number fields in lean?

Stream: maths

[Alex J. Best]

Hi all, currently lean says that number fields needs the basics of f-d vector spaces and noetherian rings, but these seem to be somewhat developed now so I thought I'd try and do some number fields. I made a pretty big mess, but I've almost proved that adjoining a root of a polynomial to Q forms a number field
https://gist.github.com/alexjbest/9fa36a92f833436199a1f891620db6a1
comments about the approach so far would be much appreciated, suggestions to make my life easier etc., as would suggestions as to which parts of my long proofs should be spun out into lemmas . But mostly I would like help with one remaining sorry! It's really dumb but I really can't work it out it's essentially

example (b : ℚ) : (rat.cast b : adjoin_root f) = b := sorry

[Johan Commelin]

What do you mean with "currently lean says" in your first sentence?

[Kevin Buzzard]

Just to let you know: a group of undergraduates at Imperial have got some work on splitting fields etc (which I think is not currently publically available) and a masters student doing a summer project in VU is working on proving that ideals factor uniquely into prime ideals.

[Alex J. Best]

@Johan Commelin to be specific mathlib says in mathlib-overview.md line 48

[Alex J. Best]

@Kevin Buzzard Ok cool, I guess I won't take this too seriously then, thanks.

[Johan Commelin]

Aha, now I understand

[Johan Commelin]

First feedback: prove https://gist.github.com/alexjbest/9fa36a92f833436199a1f891620db6a1#file-nf-lean-L43 for a general field.

[Johan Commelin]

Also, maybe first prove that K^n is fin.dim, then deduce that K is findim over K

[Johan Commelin]

But that's only if you care about generalisations (-;

[Johan Commelin]

https://gist.github.com/alexjbest/9fa36a92f833436199a1f891620db6a1#file-nf-lean-L81 This should be called adjoin_root.mk_is...

[Kevin Buzzard]

Well, if people half-do things and they don't end up in mathlib then other people will redo them. You might want to get in touch with Chris Hughes/Kenny Lau about the splitting field stuff (they surely did adding one root of an irreducible poly) and to Sander Dahmen about the masters student (I am terrible with names, this is the guy I met in VU a couple of weeks ago, but his summer job is to do a bunch of number field stuff so he might well be making serious progress)

[Johan Commelin]

@Alex J. Best Maybe first define class finite_field_extension and then specialise to number fields.

[Johan Commelin]

Pretty soon we will want L/K finite + number_field K implies number_field L.

[Rob Lewis]

@Antoine Béreau is Sander's student.

[Kevin Buzzard]

That's the guy :-) And @Chris Hughes and @Kenny Lau might know about field extensions too.

[Johan Commelin]

We should also prove in general that the characteristic of K and adjoin_root f are the same.

[Chris Hughes]

The theorem rat.eq_cast will help fill in the sorry.

[Chris Hughes]

We should also prove in general that the characteristic of K and adjoin_root f are the same.

Or more generally, the characteristic of any field extension of anything is the same.

[Johan Commelin]

Right, that's even better (-;

[Johan Commelin]

@Alex J. Best Sorry, for spamming, I can shut up if you want (-;

[Johan Commelin]

I think number_field should extend algebra.

[Alex J. Best]

Alex J. Best Sorry, for spamming, I can shut up if you want (-;

No this is good thanks, I was just leaning, generalising finitely_generated K K worked but then it won't apply now :pensive:

[Chris Hughes]

I defined finite_dimensional vector spaces recently. The fact that K is finite dimensional over K, should be an automatic instance. The instance path is kind of funny, it's a consequence of the fact that fields are euclidean domains, so they are PIDs, so they are noetherian rings.

[Alex J. Best]

The theorem rat.eq_cast will help fill in the sorry.

Awesome thanks for this, exactly what I needed!