Zulip Chat Archive

Stream: maths

Topic: number fields in lean?


view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 02 2019 at 09:08):

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

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Aug 02 2019 at 09:10):

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

view this post on Zulip Alex J. Best (Aug 02 2019 at 09:10):

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

view this post on Zulip Johan Commelin (Aug 02 2019 at 09:11):

Aha, now I understand

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 02 2019 at 09:11):

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

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Aug 02 2019 at 09:14):

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

view this post on Zulip Johan Commelin (Aug 02 2019 at 09:14):

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

view this post on Zulip Rob Lewis (Aug 02 2019 at 09:15):

@Antoine Béreau is Sander's student.

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 09:15):

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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Aug 02 2019 at 09:16):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 02 2019 at 09:17):

Right, that's even better (-;

view this post on Zulip Johan Commelin (Aug 02 2019 at 09:17):

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

view this post on Zulip Johan Commelin (Aug 02 2019 at 09:17):

I think number_field should extend algebra.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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: May 09 2021 at 09:11 UTC