finite fields

Stream: Is there code for X?

[Patrick Massot]

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

[Alex J. Best]

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]

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

[Johan Commelin]

Let's fix it by fixing mathlib.

[Patrick Massot]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

https://arxiv.org/abs/2007.01389

[Kevin Buzzard]

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

[Johan Commelin]

Good point.

[Johan Commelin]

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]

We already have the namespace finite_field

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

I don't think HoTT cares about this.

[Johan Commelin]

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]

Galois_field sounds right doesn't it

[Johan Commelin]

Ok, let's go with that.

[Alex J. Best]

/troll Or we could implement conway polynomials /troll

[Johan Commelin]

I pushed a tiny stub to finite-fields-exist

[David Wärn]

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]

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

[Alex J. Best]

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]

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

[Aaron Anderson]

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"...

[Alex J. Best]

Which lemmas?

[Aaron Anderson]

Lines 303 to 321 of finite_fields.finite

[Aaron Anderson]

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

[Aaron Anderson]

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]

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

[Alex J. Best]

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

[Aaron Anderson]

Uh, yes, sorry

[Alex J. Best]

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]

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

[Aaron Anderson]

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

[Alex J. Best]

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]

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]

I've pushed some WIP as well.

[Kenny Lau]

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

[Johan Commelin]

We are