Theory of finite fields

Stream: Is there code for X?

[Johan Commelin]

Let $L/K$ be an extension of finite fields. We know that this is a Galois extension by docs#GaloisField.instIsGaloisOfFinite

• Do we know that the Galois group is cyclic?
• Do we know that the norm map $N_{L/K}$ is surjective?

[Andrew Yang]

You've asked it once here #mathlib4 > Galois theory of finite fields and I think the answer is both (and still) no.

[Johan Commelin]

Aaahrg, at least we have proof that I'm getting old :oops:

[Jz Pan]

Johan Commelin said:

Aaahrg, at least we have proof that I'm getting old :oops:

No, we have proof that Zulip tends to lost the participated conversation history :man_facepalming:

[Jz Pan]

• Do we know that the Galois group is cyclic?

I think this shouldn't be hard? We can construct the Frobenius automorphism and prove that all automorphisms are powers of it.

[Jz Pan]

We already have Frobenius to some extent in mathlib.

[Kevin Buzzard]

Johan Commelin said:

Aaahrg, at least we have proof that I'm getting old :oops:

Or that you have 3 kids and a busy life. But my experience is that by the time the kids have stopped bothering you, you'll be old ;-)

[Kevin Buzzard]

Jz Pan said:

• Do we know that the Galois group is cyclic?

I think this shouldn't be hard? We can construct the Frobenius automorphism and prove that all automorphisms are powers of it.

How does one prove that all automorphisms are powers of it?

[Jz Pan]

Kevin Buzzard said:

Jz Pan said:

• Do we know that the Galois group is cyclic?

I think this shouldn't be hard? We can construct the Frobenius automorphism and prove that all automorphisms are powers of it.

How does one prove that all automorphisms are powers of it?

Let me check textbooks :joy:

[Kevin Buzzard]

I guess one proof would be: if L/K is finite degree d and L is finite then choose a generator g of L^x (which I think we know is cyclic) and then g has multiplicative order q^d-1 so t mapsto t^q has order d on g so has order at least d in the Galois group which has order d by FTG

[Antoine Chambert-Loir]

If $K$ has $q$ elements, then $L$ has $q^d$ elements, and the $q$-frobenius automorphism is exactly of order $d$ because $x^{q^e}=x$ as at most $q^e$ roots.

[Junyan Xu]

Yeah this is the standard proof which I also outlined here. Maybe it's also on Lang's Algebra or something. To show all elements of Gal(L/K) are powers of the $q$-Frobenius we'd combine this with an upper bound on the order of Gal(L/K), which can be given by e.g. card_algHom_le_finrank (no need of full FTG).
We do know the unit group is cyclic: instIsCyclicUnitsOfFinite.

I've attempted to define the generator of Gal(L/K):

variable (K L : Type*) [Field K] [CommRing L] [Finite K] [Algebra K L]

-- upgrade to AlgEquiv when L is perfect
def frobeniusAlgHom : L →ₐ[K] L where
  __ := powMonoidHom (Nat.card K)
  map_zero' := sorry
  map_add' := sorry
  commutes' _ := sorry

This is more general than code written by @Gian Cordana Sanjaya 2+ years ago.
However most of the library on finite fields are written using Fintype.card rather than Nat.card, and I think we should switch to the latter similar to what @Thomas Browning did/is doing for group theory.

[Johan Commelin]

I need to do something else, but I think this might also be useful start

import Mathlib

variable (K : Type*) [Field K] [Finite K]

instance : IsCyclic (K ≃+* K) := by
  obtain ⟨⟩ := nonempty_fintype K
  have ⟨p, _⟩ := CharP.exists K
  obtain ⟨n, hp, hn⟩ := FiniteField.card K p
  have : Fact (p.Prime) := ⟨hp⟩
  let alg : Algebra (ZMod p) K := by exact ZMod.algebra K p
  have := card_algHom_le_finrank (ZMod p) K K
  have : Finite (K ≃+* K) := sorry
  apply isCyclic_of_orderOf_eq_card (frobeniusEquiv K p)
  sorry

[Riccardo Brasca]

Is there a reasonable characterization of Galois group generated by the Frobenius besides the case of finite fields?

[Adam Topaz]

Riccardo Brasca said:

Is there a reasonable characterization of Galois group generated by the Frobenius besides the case of finite fields?

What do you mean by this?

[Kevin Buzzard]

Any Galois group of size 1 for a perfect field of characteristic p works. Yeah, what does "Frobenius" mean in this context? Here we're using it to mean "raise everything in the big field to the number which is the size of the small finite field"

[Riccardo Brasca]

Some power of the map x ↦ x^p, but maybe it doesn't really make sense.

[Adam Topaz]

Note that when $K$ has characteristic $p$, then the fixed field of $x \mapsto x^p$ is $\mathbb{F}_p$. I think I have some code somewhere out there that proves this...

[Adam Topaz]

import Mathlib

noncomputable section

open Classical Polynomial

variable (n : ℕ) (k : Type) (p : ℕ) [Fact (Nat.Prime p)] [CommRing k] [IsDomain k] [Algebra (GaloisField p n) k]

theorem foo (hn : n ≠ 0) (x : k) : (x^(p^n) = x) ↔ (∃ y : GaloisField p n, algebraMap _ _ y = x) := by
  let Q : k[X] := X^(p^n) - X
  have deg_Q : Q.natDegree = p^n := by
    rw [Polynomial.natDegree_sub_eq_left_of_natDegree_lt] <;>
      simp [Nat.Prime.one_lt Fact.out]
  have hQ₀ : Q ≠ 0 := by
    apply Polynomial.ne_zero_of_natDegree_gt (n := 1)
    simp only [deg_Q, Nat.Prime.one_lt Fact.out]
  let S := Q.roots.toFinset
  have hS : ∀ x, x ∈ S ↔ x ^ (p^n) = x := by simp_all [S, Q, sub_eq_zero]
  suffices Finset.image (algebraMap (GaloisField p n) k) Finset.univ = S by
    constructor
    · intro hx
      simpa [← hS, ← this] using hx
    · rintro ⟨y, rfl⟩ ; simp only [← RingHom.map_pow, ← GaloisField.card _ _ hn, FiniteField.pow_card]
  apply Finset.eq_of_subset_of_card_le
  · rintro x hx
    obtain ⟨x₀, rfl⟩ : ∃ x₀, (algebraMap (GaloisField p n) k) x₀ = x := by simpa using hx
    rw [hS, ← RingHom.map_pow, ← GaloisField.card _ _ hn, FiniteField.pow_card]
  · rw [Finset.card_image_of_injective _ (RingHom.injective _),
      Finset.card_univ, GaloisField.card _ _ hn, ← deg_Q]
    exact Q.roots.toFinset_card_le.trans Q.card_roots'

[Adam Topaz]

( Parts of this were done by @Naoya Umezaki )

[Riccardo Brasca]

Oh yes sorry, I should stop talking about math on Friday evening.

[Kevin Buzzard]

For standard infinite fields of char p like $(\Z/p\Z)(X)$ the absolute Frobenius isn't even an isomorphism :-/

[Junyan Xu]

Cyclicity is done in #22885 with the statement

instance (K L) [Finite K] [Finite L] [Field K] [Field L] [Algebra K L] : IsCyclic (L ≃ₐ[K] L)

(cc @Scott Carnahan)
Some students at the PKU/BICMR workshop Feb 12-16 also attempted to work on this (that's why I didn't resume working on this until now), and I hope they see this ...

[Junyan Xu]

#22934 proves surjectivity of norm.