Zulip Chat Archive

Stream: maths

Topic: finite fields


view this post on Zulip Joey van Langen (Jan 09 2019 at 15:09):

I'm going to do some works concerning finite fields. (number of elements, existence and uniqueness)
Can anyone tell me if the following things exist for lean in mathlib or somewhere else and where I can find them?
Integers modulo a prime, prime subfields, ring isomorphisms?

view this post on Zulip Rob Lewis (Jan 09 2019 at 15:14):

Integers mod a prime are at least instantiated as a field: https://github.com/leanprover/mathlib/blob/master/data/zmod/basic.lean#L313

view this post on Zulip Rob Lewis (Jan 09 2019 at 15:16):

Others will probably know more about your other questions. (@Kenny Lau ?)

view this post on Zulip Kenny Lau (Jan 09 2019 at 15:17):

ik ben aan het bezoeken in de stedelijk museum :p

view this post on Zulip Joey van Langen (Jan 09 2019 at 15:17):

Integers modulo p is a nice start

view this post on Zulip Rob Lewis (Jan 09 2019 at 15:18):

I'm glad someone is taking my suggestion to relax this afternoon!

view this post on Zulip Joey van Langen (Jan 09 2019 at 15:18):

Do isomorphisms exist in any context? I can only find them for types

view this post on Zulip Kenny Lau (Jan 09 2019 at 15:22):

use hott!

view this post on Zulip Joey van Langen (Jan 09 2019 at 15:24):

what do you mean by use hott?

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 15:37):

he's just trolling. He says "use something other than Lean"

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 15:38):

But I guess the answer to your question is that in general most objects don't have isomorphism between those objects already defined in Lean.

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 15:39):

You are more likely to find morphisms though, so you can define isomorphisms without too much pain. I guess morphisms of rings will be there somewhere.

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 15:40):

Some students at Imperial have done some work on splitting fields, but I don't know if it's public. What is your proposal for defining a finite field? Usually the definition I give is "splitting field of XpnXX^{p^n}-X over Fp\mathbb{F}_p, but I don't think Lean has splitting fields, at least not publically.

view this post on Zulip Joey van Langen (Jan 09 2019 at 15:41):

I'm going to use the definition as a splitting field, by using the splitting field stuff currently in the community repo

view this post on Zulip Joey van Langen (Jan 09 2019 at 15:45):

I will also use the material there concerning algebras as it will give me the tools to realize any finite field as a vector space over Fp\mathbb{F}_p

view this post on Zulip Joey van Langen (Jan 09 2019 at 15:45):

How do you put latex in these messages?

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 15:46):

$$\mathbb{F}_p$$

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 15:46):

Doesn't always work, for example \sqrt doesn't seem to work

view this post on Zulip Joey van Langen (Jan 11 2019 at 15:14):

So I have been doing some work on the finite fields with the help of @Casper Putz for the past couple of days.
We are now close to proving that every finite field has p^n elements with p a prime number.
Most effort was spent proving some simple results which we couldn't find anywhere,
such as the specification of the prime ideals and maximal ideals of Z\mathbb{Z} and proving that the zero ideal in a field is in fact maximal.
Would people be interested in seeing these results added to mathlib separately? They seem quite useful

view this post on Zulip Chris Hughes (Jan 11 2019 at 15:29):

Yes

view this post on Zulip Joey van Langen (Jan 11 2019 at 15:32):

Any suggestions of where to put that stuff?

view this post on Zulip Johan Commelin (Jan 11 2019 at 15:33):

Do you guys have push access to https://github.com/leanprover-community/mathlib/ ?

view this post on Zulip Joey van Langen (Jan 11 2019 at 15:33):

For example should the explicit specification of the prime ideals of the integers be put with ideals, with the integers or a separate file entirely

view this post on Zulip Johan Commelin (Jan 11 2019 at 15:33):

If so, put it on a branch finite_fields in that repo.

view this post on Zulip Johan Commelin (Jan 11 2019 at 15:34):

Aaah, I'm always bad at deciding what should go in which file.

view this post on Zulip Joey van Langen (Jan 11 2019 at 15:34):

Do you guys have push access to https://github.com/leanprover-community/mathlib/ ?

We don't have access to the leanprover-community yet. Would be nice to have

view this post on Zulip Joey van Langen (Jan 11 2019 at 15:35):

We're still working on it on my github, but after some cleanup that would probably be the best place to put it

view this post on Zulip Chris Hughes (Jan 11 2019 at 15:35):

It basically depends on imports. Probably ideals imports everything you need, so it should probably go there.

view this post on Zulip Johan Commelin (Jan 11 2019 at 16:00):

@Mario Carneiro Could you please give @Joey van Langen push access on community mathlib? He's a PhD student of Sander Dahmen.


Last updated: May 14 2021 at 19:21 UTC