Zulip Chat Archive

Stream: maths

Topic: number fields in lean?


Alex J. Best (Aug 02 2019 at 09:07):

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 (Aug 02 2019 at 09:08):

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

Kevin Buzzard (Aug 02 2019 at 09:09):

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 (Aug 02 2019 at 09:10):

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

Alex J. Best (Aug 02 2019 at 09:10):

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

Johan Commelin (Aug 02 2019 at 09:11):

Aha, now I understand

Johan Commelin (Aug 02 2019 at 09:11):

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

Johan Commelin (Aug 02 2019 at 09:11):

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

Johan Commelin (Aug 02 2019 at 09:11):

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

Johan Commelin (Aug 02 2019 at 09:12):

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

Kevin Buzzard (Aug 02 2019 at 09:12):

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 (Aug 02 2019 at 09:14):

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

Johan Commelin (Aug 02 2019 at 09:14):

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

Rob Lewis (Aug 02 2019 at 09:15):

@Antoine Béreau is Sander's student.

Kevin Buzzard (Aug 02 2019 at 09:15):

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

Johan Commelin (Aug 02 2019 at 09:15):

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

Chris Hughes (Aug 02 2019 at 09:16):

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

Chris Hughes (Aug 02 2019 at 09:16):

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 (Aug 02 2019 at 09:17):

Right, that's even better (-;

Johan Commelin (Aug 02 2019 at 09:17):

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

Johan Commelin (Aug 02 2019 at 09:17):

I think number_field should extend algebra.

Alex J. Best (Aug 02 2019 at 09:18):

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 (Aug 02 2019 at 09:22):

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 (Aug 02 2019 at 09:57):

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

Awesome thanks for this, exactly what I needed!


Last updated: Dec 20 2023 at 11:08 UTC