finite field

Stream: new members

[Alex Zhang]

import tactic.gptf
import data.fintype.card
import data.finset.basic
import field_theory.finite.basic

variables {F : Type*} [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]
example (a : F) : ∃ b : ℕ, coe b = a := by {sorry}

Is this proved in mathlib? If not, does anyone know how to prove it? :sweat:

[Yakov Pechersky]

Instead of constantly working with existentials, you can use the existing ring_homs and ring_isos. Try zmod.cast_hom

[Yakov Pechersky]

That goes in the other direction, but maybe it is useful

[Eric Wieser]

docs#zmod.cast_hom

[Eric Wieser]

docs#zmod.ring_equiv is stronger, but I don't think you can satisfy the hypothesis

[Kevin Buzzard]

The statement you want to prove is not true

[Kevin Buzzard]

Not every finite field is Z/pZ

[Alex Zhang]

Kevin reminded me of the right thing!!

[Alex Zhang]

F is a finite filed of char p, is it true that (∃ (a : F), a ^ 2 = -1) → (∃ (y : zmod p), y ^ 2 = -1).
If so, how to get this?

[Adam Topaz]

This is not true. If you take a prime $p$ such that $-1$ is not a square mod $p$, you can always adjoin a square-root of $-1$ to $\mathbb{F}_p$ to get a finite extesion where $Y^2 = -1$ has a solution.

[Alex Zhang]

Is the following lemma proved in mathlib? I only noticed a weaker version for zmod p

import tactic
import field_theory.finite.basic
import number_theory.quadratic_reciprocity

variables {F : Type*} [field F] [fintype F] [decidable_eq F] (p : ℕ) [char_p F p]

lemma finite_field.exists_sq_eq_neg_one_iff_mod_four_ne_three :
∃ a : F, a ^ 2 = -1 ↔ fintype.card F % 4 ≠ 3 := sorry

#check zmod.exists_sq_eq_neg_one_iff_mod_four_ne_three

zmod.exists_sq_eq_neg_one_iff_mod_four_ne_three is here
https://leanprover-community.github.io/mathlib_docs/number_theory/quadratic_reciprocity.html#zmod.exists_sq_eq_neg_one_iff_mod_four_ne_three

[Kevin Buzzard]

AFAIK everything we have about finite fields in general (i.e. not stuff about just Z/p) will be in src.field_theory.finite.*

[Kevin Buzzard]

and apparently there are also things which aren't about finite fields at all in there too, like Fermat-Euler and mv_polynomial.evalₗ (which seems to be proved under a superfluous fintype K assumption unless I'm missing something)

[Kevin Buzzard]

The result is pretty straightforward mathematically if you know the multiplicative group is finite, and we have a more general statement that a finite subgroup of the units of any ID is cyclic somewhere in mathlib.

[Alex Zhang]

Yeah, I saw the cyclic lemma somewhere before. If this lemma is not there, I am to do it myself :)

[Alex Zhang]

The result is pretty straightforward mathematically. Indeed, no sure whether it is still straightforward when implementing.

[Alex Zhang]

I just wanna pre-check here to see if I can save some effort.

[Alex Zhang]

Is there another quick way to prove that fintype.card F % 4 =1 → ∃ a : F, a ^ 2 = -1 for a finite field F without using the fact that the unit group is cyclic? @Kevin Buzzard

[Kevin Buzzard]

We have that the unit group is cyclic in Lean. If all you know about $F^\times$ is that it's a group of order 0 mod 4 then this isn't enough because it could be isomorphic to $\Z/2\Z\times\Z/n\Z$ with the generator of the $\Z/2\Z$ being $-1$.

[Kevin Buzzard]

There's a trick for $\Z/p\Z$ because then using Wilson's theorem you have the explicit solution $a=(\frac{p-1}{2})!$ but this doesn't work for general finite $F$.

[David Wärn]

Generalising this trick, I guess for general finite F you can pick one of {x, -x} for each nonzero such pair and multiply them.

[Kevin Buzzard]

Right! So the first observation is that the product of all the units is $-1$ (we have this in Lean too, IIRC, indeed I just fixed the proof so that it didn't use is_monoid_hom yesterday), and this is because every unit other than $\pm1$ has an inverse which is distinct from it so it cancels with it. Now you consider the involution $x\mapsto -x$ on the units; now every orbit has size 2, so sharing them equally into two subsets with products $a$ and $b$ we have $ab=-1$ and $b=(-1)^{(q-1)/2}a$ which is $a$ under the hypothesis $q\equiv1$ mod $4$ (here $q$ is the size of the field). This might be longer to formalise than the cyclic proof though.

[Alex Zhang]

Is the existence of finite fields proved in mathlib?

import field_theory.finiteness

example {n p : ℕ} (hp : p.prime) : ∃ {F : Type*} [c : fintype F] [d : field F],
@fintype.card F c = p^(n.succ) :=
begin
  sorry
end

[Alex Zhang]

(deleted)

[Eric Wieser]

(an unrelated tip: if you replace the , with , by exactI you don't need the @)

[Eric Rodriguez]

https://leanprover-community.github.io/mathlib_docs/field_theory/finite/basic.html

[Eric Wieser]

I couldn't see a proof of existence that looks like Alex's statement there

[Ruben Van de Velde]

https://leanprover-community.github.io/mathlib_docs/data/zmod/basic.html#zmod.field is a start, at least

[Alex Zhang]

I think the finite filed basic file can't have it as the existence requires the use of splitting field in my memory.

[Eric Rodriguez]

ah I see the issue! do we have that there exists an irreducible polynomial of any degree? (is that even true in general - I know it's true in ℤ/pℤ but that's in turn due to the finite field construction)

[Eric Rodriguez]

because then docs#adjoin_root.field probably gives us thie result instantly

[Eric Rodriguez]

that still may not be the best way to do it, though; we'd probably want a primitive polynomial if we could, because that's closer to the "canonical" finite field and it's nice that the root generates

[Alex Zhang]

to construct a field F of order p^n = q, we want it to be the splitting field of x^q - x over GF(p).

[Alex Zhang]

If the existence hasn't been established or there isn't an instant solution. I guess https://leanprover-community.github.io/mathlib_docs/field_theory/splitting_field.html#polynomial.is_splitting_field
is the file to start with. Some lemmas there can help.

[Eric Rodriguez]

yes, that's one way — i think we can also do what I said too though, right? splitting fields seem more tricky, as we then have to toy a little to get the number of elements, whilst my idea gets it for free, I think

[Alex J. Best]

A long time ago (in mathlib terms) a few people worked on this at https://github.com/leanprover-community/mathlib/tree/finite-fields-exist but i don't think it made it to mathlib in the end for some reason. Maybe you can find the thread here on Julio somewhere

[Eric Wieser]

Specifically this line: https://github.com/leanprover-community/mathlib/compare/finite-fields-exist#diff-2a88a230cdd2ba9936dfcce670803cf356cb6ab2ed303ef41aa74b8e9730979fR222

[Eric Wieser]

I guess the thing to do is try merging master into that branch and work out which bits are now already merged; maybe with the help of the people who worked on it!

[Eric Rodriguez]

should this thread be moved to #maths?

[Ruben Van de Velde]

Eric Wieser said:

I guess the thing to do is try merging master into that branch and work out which bits are now already merged; maybe with the help of the people who worked on it!

You nerd-sniped me into PRing this: https://github.com/leanprover-community/mathlib/pull/8692

[Eric Rodriguez]

okay... so the finrank thing isn't true

[Eric Rodriguez]

splitting field of n=0 is some nonsense, I assume probably just zmod p itself

[Eric Rodriguez]

im too tired to figure out whether that's a big deal or not

[Eric Rodriguez]

probably not and we'll have to carry around an (n ≠ 0) everywhere

[Eric Rodriguez]

it's now merged into master @Alex Zhang

[Alex Zhang]

Thanks for letting me know Eric @Eric Rodriguez. Could you point me where the lemma lies?

[Ruben Van de Velde]

https://leanprover-community.github.io/mathlib_docs/field_theory/finite/galois_field.html

[Ruben Van de Velde]

The actual \exists isn't there yet, but should be simple to write