Zulip Chat Archive

Stream: Is there code for X?

Topic: finite fields


view this post on Zulip Patrick Massot (Jul 10 2020 at 17:16):

Does mathlib know there exist a finite field with cardinal pnp^n for all pp and nn?

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

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

view this post on Zulip Johan Commelin (Jul 10 2020 at 17:32):

Let's fix it by fixing mathlib.

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

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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:41):

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

view this post on Zulip Johan Commelin (Jul 10 2020 at 17:41):

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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:43):

https://arxiv.org/abs/2007.01389

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

view this post on Zulip Johan Commelin (Jul 10 2020 at 17:44):

Good point.

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

view this post on Zulip Johan Commelin (Jul 10 2020 at 17:45):

We already have the namespace finite_field

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:45):

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

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

view this post on Zulip Johan Commelin (Jul 10 2020 at 17:49):

I don't think HoTT cares about this.

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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:51):

Galois_field sounds right doesn't it

view this post on Zulip Johan Commelin (Jul 10 2020 at 17:54):

Ok, let's go with that.

view this post on Zulip Alex J. Best (Jul 10 2020 at 18:04):

/troll Or we could implement conway polynomials /troll

view this post on Zulip Johan Commelin (Jul 10 2020 at 18:06):

I pushed a tiny stub to finite-fields-exist

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

view this post on Zulip Johan Commelin (Jul 10 2020 at 18:40):

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

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

view this post on Zulip Johan Commelin (Jul 10 2020 at 20:22):

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

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

view this post on Zulip Alex J. Best (Jul 11 2020 at 00:59):

Which lemmas?

view this post on Zulip Aaron Anderson (Jul 11 2020 at 01:37):

Lines 303 to 321 of finite_fields.finite

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

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

view this post on Zulip Alex J. Best (Jul 11 2020 at 01:49):

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

view this post on Zulip Alex J. Best (Jul 11 2020 at 01:51):

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

view this post on Zulip Aaron Anderson (Jul 11 2020 at 01:57):

Uh, yes, sorry

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

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

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

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

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

view this post on Zulip Johan Commelin (Jul 11 2020 at 06:28):

I've pushed some WIP as well.

view this post on Zulip Kenny Lau (Jul 11 2020 at 06:28):

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

view this post on Zulip Johan Commelin (Jul 11 2020 at 06:29):

We are


Last updated: May 07 2021 at 18:19 UTC