Stream: Is there code for X?

Topic: finite fields

Patrick Massot (Jul 10 2020 at 17:16):

Does mathlib know there exist a finite field with cardinal $p^n$ for all $p$ and $n$?

Alex J. Best (Jul 10 2020 at 17:27):

I don't think so, we have adjoin_root so the only hard part is showing there exists an irreducible polynomial of every degree over any zmodp p, this follows from a counting argument but I've not seen it in mathlib/anywhere else.

Patrick Massot (Jul 10 2020 at 17:31):

That's what I suspected, so listing finite fields on the overview page is a pretty clear lie.

Johan Commelin (Jul 10 2020 at 17:32):

Let's fix it by fixing mathlib.

Patrick Massot (Jul 10 2020 at 17:33):

Sure, someone should do it while I cook dinner. I guess you had dinner a long time ago?

Kevin Buzzard (Jul 10 2020 at 17:41):

Sound just posted something on Arxiv literally a few days ago explaining a counting argument and arguing that it's a finite field version of Bertrand's postulate

Kevin Buzzard (Jul 10 2020 at 17:41):

It's something he lectured to his UGs in Stanford. It looked like a nice approach

Johan Commelin (Jul 10 2020 at 17:41):

Isn't it theoretically cleaner to define them as the splitting field of X^q - 1?

Kevin Buzzard (Jul 10 2020 at 17:43):

https://arxiv.org/abs/2007.01389

Kevin Buzzard (Jul 10 2020 at 17:44):

Yes, I just thought this was cool :-) I always do the splitting field argument (X^q-X not 1)

Good point.

Johan Commelin (Jul 10 2020 at 17:44):

How are we going to call the "canonical" field with p ^ n elements?
galois_field p n
finite_field p n
GF p n

Johan Commelin (Jul 10 2020 at 17:45):

We already have the namespace finite_field

Kevin Buzzard (Jul 10 2020 at 17:45):

There isn't a canonical field with p^n elements :-)

Kevin Buzzard (Jul 10 2020 at 17:46):

It's only defined up to nonunique isomorphism. Perhaps it's at this point we're glad we're not univalent

Johan Commelin (Jul 10 2020 at 17:49):

What I meant with "canonical" is: if people are going to need a finite field with p ^ n elements, they want to grab it from the library. Which name should they look for?

Kevin Buzzard (Jul 10 2020 at 17:51):

Galois_field sounds right doesn't it

Johan Commelin (Jul 10 2020 at 17:54):

Ok, let's go with that.

Alex J. Best (Jul 10 2020 at 18:04):

/troll Or we could implement conway polynomials /troll

Johan Commelin (Jul 10 2020 at 18:06):

I pushed a tiny stub to finite-fields-exist

David Wärn (Jul 10 2020 at 18:33):

I think even in HoTT there really is a canonical field with p^n elements: pick the first irreducible polynomial of degree n in lexicographic order and quotient. What's non-canonical is the isomorphism between two fields of p^n elements.

Johan Commelin (Jul 10 2020 at 18:40):

If anyone else is working on this, please coordinate here, to avoid duplicate efforts

Alex J. Best (Jul 10 2020 at 18:41):

Thats almost what conway polynomials are, except conway also assumes an extra compatibility between subfields. The word canonical is undefined but I wouldn't say lexicographic order is any more canonical than reverse lexicographic.

Johan Commelin (Jul 10 2020 at 20:22):

I'm done for today. There's quite a number of sorrys on the branch (-;

Aaron Anderson (Jul 11 2020 at 00:52):

I've been working on this, but my two lemmas on finite-dimensional vector spaces over finite fields (at the end of finite_fields.finite) give me the error "maximum class-instance resolution depth has been reached"...

Which lemmas?

Aaron Anderson (Jul 11 2020 at 01:37):

Lines 303 to 321 of finite_fields.finite

Aaron Anderson (Jul 11 2020 at 01:38):

Also, before we get too far along, I’m noticing that the injections between galois fields will not be canonical

Aaron Anderson (Jul 11 2020 at 01:41):

Do we perhaps want to take a slight detour in the overall design by constructing an algebraic closure of zmod p, and then labelling the finite subfields of that the Galois fields? I think that gives us better uniqueness

Alex J. Best (Jul 11 2020 at 01:49):

I'm sorry, I don't know what finite_fields.finite is

Alex J. Best (Jul 11 2020 at 01:51):

You're talking about src/field_theory/finite.lean?

Uh, yes, sorry

Alex J. Best (Jul 11 2020 at 01:58):

I know what you mean about having nice containments of the fields, but whats best really depends on what we want to do with finite fields, right now we were just intending to prove they exist (and personally I feel the splitting field is a lot more direct than going all the way to the algebraic closure). I don't believe we have algebraic closure in mathlib so I'd definitely vote for keeping it simple for the sake of "a" construction for now.

Alex J. Best (Jul 11 2020 at 01:59):

I think I'm of the opinion that your slight detour won't be so slight!

Aaron Anderson (Jul 11 2020 at 02:02):

It'd be pretty quick if we had algebraic closures already, but since we don't, fair enough...

Alex J. Best (Jul 11 2020 at 02:04):

There have been a few pushes to add algebraic closures via different approaches in the past but none of them have made it so far, hopefully soon enough :slight_smile:

Aaron Anderson (Jul 11 2020 at 06:25):

I’ve written some lemmas building up to showing that there are p^n roots of X^(p^n)-X in galois_field p n.

Johan Commelin (Jul 11 2020 at 06:28):

I've pushed some WIP as well.

Kenny Lau (Jul 11 2020 at 06:28):

we can just use the splitting field of X^p^n - X

Johan Commelin (Jul 11 2020 at 06:29):

We are

Last updated: May 07 2021 at 18:19 UTC