How to formalize a finite field exercise?

Stream: new members

[Mzk invert neko]

I’m trying to formalize a finite field exercise using Lean. The statement is:
Let $F = 𝔽_{q^m}$, and $K = 𝔽_q$. For any $c ∈ K$, define the polynomial
$f(x) = ∑_{j=0}^{m−1} x^{q^j} − c ∈ K[X]$.
Then we have:
$f(x) = ∏_{α ∈ F, Tr_{F/K}(α) = c} (x − α)$

I write this in Lean as:

import Mathlib

open FiniteField Polynomial Finset

open Classical
noncomputable section

variable {q m : ℕ} [hq : Fact q.Prime]
variable (K F : Type*) [Field K] [Field F] [Fintype K] [Fintype F]
variable [Algebra K F]
variable (c : K)
variable (f : Polynomial K := (Finset.range m).sum (λ j => X ^ (q ^ j)) - C c)
variable (S : Finset F := Finset.univ.filter (λ α => (Finset.range m).sum (λ j => α ^ (q ^ j)) = algebraMap K F c))
variable (hK : Fintype.card K = q) (hF : Fintype.card F = q ^ m)

theorem ex2_34 :
    f.map (algebraMap K F) = S.prod (λ α => X - C α) := by
  sorry

And I tried to write "S" in Lean as :

(S : Finset F := Finset.univ.filter (λ α => Algebra.trace K F α = c))

But I couldn’t find a statement in mathlib saying that the trace Algebra.trace K F α equals the Frobenius power sum

$$trace = ∑_{j=0}^{m−1} x^{q^j}$$

so I wasn’t sure whether this is the correct way to formalize the trace condition in Lean.

Mathematically, the core step is just to show that the trace polynomial $∑ x^{q^j} - c$ is separable (i.e., has no repeated roots).
Does anyone know whether this Frobenius-trace identity exists in mathlib?
Or alternatively, could anyone recommend which lemmas I might use in Lean to prove the separability of this polynomial?

Thanks a lot!

[Notification Bot]

This topic was moved here from #announce > How to formalize a finite field exercise? by Damiano Testa.

[Mzk invert neko]

And this is the original text:
image.png

[Kenny Lau]

@Mzk invert neko there's FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow:

Function.Bijective fun (n : Fin (Module.finrank K L)) => frobeniusAlgEquivOfAlgebraic K L ^ ↑n

This is an explicit bijection between Fin n and Gal(L/K) where n = [L:K] (defined using modules), and it sends each i < n to Frob^i (sorry i is n in the code)

[Kenny Lau]

I think your q.Prime might not be what the author intended

[Kenny Lau]

regrettably mathlib seems to be missing some key lemmas (or at least i can't find them)

[Kenny Lau]

import Mathlib

universe u v

variable (K : Type u) (L : Type v) [Field K] [Field L] [Fintype K] [Fintype L] [Algebra K L]

example : IsGalois K L := inferInstance
#check GaloisField.instIsGaloisOfFinite -- uses this!

open FiniteField

theorem algebraMap_trace_eq_sum_frobenius_pow (x : L) :
    algebraMap K L (Algebra.trace K L x) =
      ∑ i ∈ Finset.range (Module.finrank K L), (frobeniusAlgEquivOfAlgebraic K L ^ i) x := by
  rw [trace_eq_sum_automorphisms,
    ← Fintype.sum_bijective _ (bijective_frobeniusAlgEquivOfAlgebraic_pow K L) _ _ fun _ ↦ rfl,
    Finset.sum_range]

theorem ofId_trace_eq_sum_frobenius_pow :
    (Algebra.ofId K L).toLinearMap.comp (Algebra.trace K L) =
      ∑ i ∈ Finset.range (Module.finrank K L), (frobeniusAlgEquivOfAlgebraic K L).toLinearMap ^ i :=
  LinearMap.ext fun x ↦ (algebraMap_trace_eq_sum_frobenius_pow K L x).trans <| by
    simp [← AlgEquiv.pow_toLinearMap]

[Kenny Lau]

feel free to PR this to mathlib (or maybe i will eventually)

[Mzk invert neko]

Kenny Lau said:

feel free to PR this to mathlib (or maybe i will eventually)

Thank you! It helps. I’ll study it further.

[Kenny Lau]

@Mzk invert neko made #27289

[Mzk invert neko]

Here is the (maybe) good version of ex2.34:

universe u v
import Mathlib

variable (K : Type u) (L : Type v) [Field K] [Field L] [Fintype K] [Fintype L] [Algebra K L]

theorem ex2_34
    -- (hFK : Algebra.IsSeparable K L)(maybe useless)
    (c : K) (x : L)
    (S : Finset L := Finset.univ.filter (λ α => Algebra.trace K L α = c))
    (g := S.prod (fun α => X - C α))
    (f := ∑ i ∈ Finset.range (Module.finrank K L), X ^ (Fintype.card K ^ i) - C (algebraMap K L c)):
    f = g := by
  sorry

Both sides have the same roots, and all these roots are simple. I believe this is sufficient to prove the equality.
Maybe some tactics or lemmas of Polynomial work. I don't know.

[Kenny Lau]

@Mzk invert neko I entered "two polynomials with same roots are equal" into leanexplore and the first result is already the correct one