finite fields

Stream: maths

[Joey van Langen]

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?

[Rob Lewis]

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

[Rob Lewis]

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

[Kenny Lau]

ik ben aan het bezoeken in de stedelijk museum :p

[Joey van Langen]

Integers modulo p is a nice start

[Rob Lewis]

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

[Joey van Langen]

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

[Kenny Lau]

use hott!

[Joey van Langen]

what do you mean by use hott?

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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 $X^{p^n}-X$ over $\mathbb{F}_p$, but I don't think Lean has splitting fields, at least not publically.

[Joey van Langen]

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

[Joey van Langen]

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 $\mathbb{F}_p$

[Joey van Langen]

How do you put latex in these messages?

[Kevin Buzzard]

$$\mathbb{F}_p$$

[Kevin Buzzard]

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

[Joey van Langen]

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 $\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

[Chris Hughes]

Yes

[Joey van Langen]

Any suggestions of where to put that stuff?

[Johan Commelin]

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

[Joey van Langen]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Joey van Langen]

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

[Joey van Langen]

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

[Chris Hughes]

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

[Johan Commelin]

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