Help on Galois Fields

Stream: new members

[Riyaz Ahuja]

Hello, I'm playing around with Galois fields, and was wondering how elements of the GF are represented. In that, looking at the implementation, GF's are defined in the standard way as the splitting field of $X^{p^n} - X$ (w.r.t $(\mathbb{Z}/p)[X]$). Quickly testing, I get that#check ((7 :ℕ ): GaloisField 7 2) is a valid element in GF(7,2) (as expected), but when I attempt:

#check ((X : (ZMod 7)[X]): GaloisField 7 2)

Or anything similar involving some element of (ZMod 7)[X], i get that:

type mismatch
  X
has type
  (ZMod 7)[X] : Type
but is expected to have type
  GaloisField 7 2 : Type

So, it seems that any lifting into the splitting field isn't handled automatically. Is there some explicit function to convert this element of (ZMod p)[X]to an element in the GF?

Thanks

[Kevin Buzzard]

docs#GaloisField

[Ruben Van de Velde]

Does algebraMap work?

[Aaron Liu]

GaloisField p n is an algebra over ZMod p, but not over (ZMod p)[X]

[Aaron Liu]

import Mathlib

open Polynomial

instance : Fact (Nat.Prime 7) := Fact.mk (by norm_num)

/--
error: failed to synthesize
  Algebra (ZMod 7)[X] (GaloisField 7 2)

Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
#check (algebraMap _ _ (X : (ZMod 7)[X]) : GaloisField 7 2)

[Kevin Buzzard]

Mathlib isn't a computer algebra system. It's not even clear to me that these elements are "represented". Here's a maths question. Let k be a field with 2^37 elements. What "is" an element of k? I don't think this question makes sense. Lean's understanding of finite fields is closer to a mathematician's understanding of them rather than a computer algebra package's understanding. You can factor a polynomial and choose a root at random but I'm not sure that the elements are "represented" by anything.

[Riyaz Ahuja]

I see, this makes sense for a ITP implementation of finite fields.

[Riyaz Ahuja]

I'm working on making an interface for Macaulay2 for lean, and have been working on adding grobner basis support for more types (i.e. whatever macaulay2 is able to support). One such thing was finite fields, as well as quotient rings and the like.

The idea here was if a lean user needed to, say, calculate ideal membership for some polynomials in some finite field, my tactic could parse that finite field into a galois field, which is then converted to macaulay2 galois fields, and eventually mapped back after the computation. M2 handles GF's using the same implementation of splitting fields as lean, so such a mapping should be pretty straightforward, I imagine?

[Riyaz Ahuja]

Kevin Buzzard said:

Mathlib isn't a computer algebra system. It's not even clear to me that these elements are "represented". Here's a maths question. Let k be a field with 2^37 elements. What "is" an element of k? I don't think this question makes sense. Lean's understanding of finite fields is closer to a mathematician's understanding of them rather than a computer algebra package's understanding. You can factor a polynomial and choose a root at random but I'm not sure that the elements are "represented" by anything.

As for this, if we're talking about this specific implementation of GF's, why wouldn't elements of the field be well-defined? I mean, its a quotient at the end of the day, and I would imagine that just as a is an element in the M2 implementation of GF's, Polynomial.X should be in our implementation as well?

[Riyaz Ahuja]

Aaron Liu said:

GaloisField p n is an algebra over ZMod p, but not over (ZMod p)[X]

Does this mean that I can only lift elements of ZMod p into the GF?

[Riyaz Ahuja]

I guess my real confusion here is what are the elements of GaloisField p n?

[Aaron Liu]

They are elements of the splitting field

[Riyaz Ahuja]

Aaron Liu said:

They are elements of the splitting field

And so they are elements of MvPolynomial (SplittingFieldAux f.natDegree f) (ZMod p)? What do those look like?

[Aaron Liu]

They look like multivariate polynomials in K with indeterminates indexed by SplittingFieldAux f.natDegree f

[Aaron Liu]

And it looks like SplittingFieldAux n f is just K but with a different algebra instance

[Aaron Liu]

So MvPolynomial (SplittingFieldAux f.natDegree f) (ZMod p) is multivariate polynomials in ZMod p with indeterminates indexed by ZMod p

[Aaron Liu]

and then take a quotient

[Riyaz Ahuja]

Shouldn't this just be the same as some quotient of $(\mathbb{Z}/p)[a]$ though?

[Aaron Liu]

So actually SplittingFieldAux n f is AdjoinRoot f.removeFactor.removeFactor.....factor and I just misread what the code was doing

[Aaron Liu]

whoops

[Riyaz Ahuja]

So in the example of GF(3,2), we have our f as:
$x^{3^2}-x = x(x+1)(x+2)(x^2+1)(x^2+x+2)(x^2+2x+2)$

Then what does SplittingFieldAux f.natDegree f return?

[Riyaz Ahuja]

because I think I'm a bit lost on what this function is doing here

[Riyaz Ahuja]

and according to the CAS's, the lean representation of GF(3,2) should be something like $\frac{(\mathbb Z/3)[x]}{x^2-x-1}$

[Aaron Liu]

It uses choice to find an irreducible factor of x^3^2-x, defaulting to Polynomial.X if none exists
Then it adjoins a root of this factor to the field and divides the factor out to get a new polynomial in the new field

[Aaron Liu]

It does this 8 more times recursively with the new polynomial in the new field

[Aaron Liu]

Then it returns the resulting field which is ZMod 3 with 9 roots adjoined sequentially

[Aaron Liu]

Or at least, that's what I am getting from reading the code and I could be wrong

[Bjørn Kjos-Hanssen]

I just opened up Zulip to look for an answer to this question and this was literally the top topic displayed (without searching). What are the odds...

Riyaz Ahuja said:

Hello, I'm playing around with Galois fields, and was wondering how elements of the GF are represented. ````

[Bjørn Kjos-Hanssen]

How would one prove this "theorem" (totally not trying to use Lean as a computer algebra system ;))

∃ α : @SplittingField (ZMod 2) (ZMod.instField 2)
  (X ^ 2 ^ 2 - X), α * α = α + 1

[Aaron Liu]

Bjørn Kjos-Hanssen said:

How would one prove this "theorem" (totally not trying to use Lean as a computer algebra system ;))

∃ α : @SplittingField (ZMod 2) (ZMod.instField 2)
  (X ^ 2 ^ 2 - X), α * α = α + 1

Construct an explicit field with that property and the use docs#Polynomial.IsSplittingField.algEquiv to transfer it

[Aaron Liu]

It's only four elements, not that bad

[Riyaz Ahuja]

Aaron Liu said:

Bjørn Kjos-Hanssen said:

How would one prove this "theorem" (totally not trying to use Lean as a computer algebra system ;))

∃ α : @SplittingField (ZMod 2) (ZMod.instField 2)
  (X ^ 2 ^ 2 - X), α * α = α + 1

Construct an explicit field with that property and the use docs#Polynomial.IsSplittingField.algEquiv to transfer it

Wait, can't this same idea be extended to the question of explicitly constructing GF(p,n)? In that, macaulay2 or any other CAS can explicitly construct GF(3,2) as $\frac{(\mathbb Z/3)[x]}{x^2-x-1}$. Is it feasible to simply show that it is algebraically equivalent, and then i can simplify to considering elements within the explicit CAS-produced construction?

[Aaron Liu]

How do you obtain the $x^2-x-1$ in $\frac{(\mathbb Z/3)[x]}{x^2-x-1}$?

[Riyaz Ahuja]

just computationally using M2:

Macaulay2, version 1.21
with packages: ConwayPolynomials, Elimination, IntegralClosure, InverseSystems, Isomorphism, LLLBases, MinimalPrimes, OnlineLookup, PrimaryDecomposition, ReesAlgebra, Saturation, TangentCone

i1 : R=GF(3,2)

o1 = R

o1 : GaloisField

i2 : ambient R

        ZZ
        --[a]
         3
o2 = ----------
      2
     a  - a - 1

o2 : QuotientRing

[Riyaz Ahuja]

this should be the explicit construction of whatever nonconstructive stuff is happening in the lean implementation

[Aaron Liu]

I meant algorithmically, what is M2 doing to get to a^2 - a - 1?

[Bjørn Kjos-Hanssen]

I must be doing this in a way too tedious way... here's how I construct multiplication on GF(4).

/-- Thinking of (u,v) as u α + v. -/
instance mymul : Mul (Fin 2 × Fin 2) := {
  mul := fun p => match p with
  |(0,0) => fun q => (0,0)
  |(0,1) => id
  |(1,0) => fun q => match q with
    |(0,0) => (0,0)
    |(0,1) => (1,0)
    |(1,0) => (1,1)
    |(1,1) => (0,1)
  |(1,1) => fun q => match q with
    |(0,0) => (0,0)
    |(0,1) => (1,1)
    |(1,0) => (0,1)
    |(1,1) => (1,0)
}

[Riyaz Ahuja]

Aaron Liu said:

I meant algorithmically, what is M2 doing to get to a^2 - a - 1?

it seems that it's enumerating monic polynomials of degree n in (Z/p)[a] and testing for irreducibility. It is known that quotient of $(\mathbb{Z}/p)[x]$ by a monic irreducible $f$ of degree $n$ is a finite field of size $p^n$. See wikipedia

[Aaron Liu]

I guess we could add Conway polynomials to mathlib

[Riyaz Ahuja]

Riyaz Ahuja said:

this should be the explicit construction of whatever nonconstructive stuff is happening in the lean implementation

unfortunately, i don't think this will work in practice as even though the output of M2 is correct, the implementation of docs#Polynomial.IsSplittingField.algEquiv relies on (a) a bunch of really annoying to prove facts, and (b) a lot of noncomputable things, so you can't just map elements via the isomorphism (explicitly).

[Riyaz Ahuja]

Yeah, then it'd come down to showing algebraic equivalence to GF(p,n) exactly once but then we'd have a nice explicit construction for any finite field work.

[Riyaz Ahuja]

where talking about elements actually makes sense

[Aaron Liu]

Riyaz Ahuja said:

Riyaz Ahuja said:

this should be the explicit construction of whatever nonconstructive stuff is happening in the lean implementation

unfortunately, i don't think this will work in practice as even though the output of M2 is correct, the implementation of docs#Polynomial.IsSplittingField.algEquiv relies on (a) a bunch of really annoying to prove facts, and (b) a lot of noncomputable things, so you can't just map elements via the isomorphism (explicitly).

There's also no easy way to construct any elements at all except by using docs#Polynomial.IsSplittingField.algEquiv

[Aaron Liu]

So you can just cancel the equiv

[Kevin Buzzard]

Mathlib's abstract implementation of splitting fields is probably noncomputable. What you'd want to do here is to make a computable representation (ideally equal to M2's) and then prove that the types are in bijection and then implement mathlib's finite fields with the concrete computable representation.

[Riyaz Ahuja]

I don't think conway polynomials are necessarily required for this either. We can just require monic irreducible in our quotient and instantly get a more general implementation. (The specific matching with M2 is unnecessary imo as they literally enumerate and filter according to some (probably lexicographic) ordering to find their quotient. But as long as its monic irreducible its actually fine.) This does have the annoying issue of making the proof of isomorphism a bit more difficult but it shouldn't be unmanageable.

It seems to me that the splitting field implementation was designed for a more generalized use, but as finite fields are a very commonly used structure, it probably makes sense to have a constructive version that is a lot easier to directly reason about.

[Riyaz Ahuja]

(the fact that it makes my life a lot easier for implementing M2 stuff in lean is just a nice extra benefit :grinning_face_with_smiling_eyes: )