finite field has size ringExpChar^n

Stream: Is there code for X?

[Kevin Buzzard]

What I actually want is this (a statement which looks quite clean to me):

import Mathlib

open scoped Polynomial

lemma foo (k : Type*) [Field k] [Fintype k] (f : k[X]) (L : Type*) [CommRing L] [Algebra k L]
    (t : L) : f.eval₂ (algebraMap k L) (t^(Fintype.card k)) =
              (f.eval₂ (algebraMap k L) t)^(Fintype.card k) := by
  sorry

(mathematically this says that if $f\in k[X]$ then $f(t^q)=f(t)^q$ if $q$ is the size of the finite field $k$). I couldn't find it so thought I'd try proving it but I ended up taking everything apart and using induction, and even then I could only get to the end with another assumption bar, which surely is not hard but I can't put the pieces together with what we have. Am I even supposed to be using ringExpChar?

import Mathlib

open scoped Polynomial

lemma bar (k : Type*) [Field k] [Fintype k] : ∃ n : ℕ, ringExpChar k ^ n = Fintype.card k := by
  sorry

lemma foo (k : Type*) [Field k] [Fintype k] (f : k[X]) (L : Type*) [CommRing L] [Algebra k L]
    (t : L) : f.eval₂ (algebraMap k L) (t^(Fintype.card k)) =
              (f.eval₂ (algebraMap k L) t)^(Fintype.card k) := by
  obtain ⟨n, hn⟩ := bar k
  induction f using Polynomial.induction_on
  · simp [← map_pow, FiniteField.pow_card]
  · next g h h1 h2 =>
    simp only [Polynomial.eval₂_add, h1, h2]
    rw [← hn]
    by_cases hL : Nontrivial L
    · haveI := expChar_of_injective_algebraMap (NoZeroSMulDivisors.algebraMap_injective k L) (ringExpChar k)
      rw [add_pow_expChar_pow]
    · apply (not_nontrivial_iff_subsingleton.mp hL).elim
  · simp only [Polynomial.eval₂_mul, Polynomial.eval₂_C, Polynomial.eval₂_X_pow, mul_pow,
     ← map_pow, pow_right_comm, FiniteField.pow_card]

[Michael Stoll]

docs#frobenius ? It gives you a ring homomorphism, which should do most of what you want (you'll also need that it is the identity on coefficients).

[Michael Stoll]

docs#FiniteField.frobenius_pow

[Kevin Buzzard]

Yeah but frobenius_pow needs [CharP K p] which is what I'm struggling to get. The hypotheses of that result are "p is the characteristic" and "the cardinality is p^n". My statement about polynomials only needs the cardinality so there is no p at all in the statement, unless I create a p using e.g. the statement that a finite field has size a prime power, but then there's no relationship between this p and the characteristic. Or I can use the fact that a finite field has a characteristic, but then I need to relate it to the cardinality.

[Kevin Buzzard]

More succinctly: I claim that docs#FiniteField.frobenius_pow would help with my problem if it didn't have the unnecessary (in the sense that it's implied by the other inputs) [CharP K p]. Furthermore I claim that the other hypotheses imply that p = ringExpChar kand that p = ringChar k, so we even have a name for them, but now you have to relate them to the cardinality, and then I'm done.

[Michael Stoll]

So maybe there should be a variant of docs#FiniteField.card' that also gives you CharP K p.

[Michael Stoll]

import Mathlib

example (K : Type*) [Field K] [Fintype K] : ∃ p n, p.Prime ∧ Fintype.card K = p ^ ↑n ∧ CharP K p := by
  obtain ⟨p, n, h₁, h₂⟩ := FiniteField.card' K
  refine ⟨p, n, h₁, h₂, ?_⟩
  have : (p ^ (n : ℕ) : K) = 0 := mod_cast h₂ ▸ Nat.cast_card_eq_zero K
  rw [CharP.charP_iff_prime_eq_zero h₁]
  simpa only [ne_eq, PNat.ne_zero, not_false_eq_true, pow_eq_zero_iff] using this

This can certainly be optimized a bit...

[Michael Stoll]

Or maybe better(?) without PNat:

import Mathlib

example (K : Type*) [Field K] [Fintype K] : ∃ p n : ℕ, p.Prime ∧ Fintype.card K = p ^ n ∧ CharP K p := by
  obtain ⟨p, n, h₁, h₂⟩ := FiniteField.card' K
  refine ⟨p, n.val, h₁, h₂, ?_⟩
  have : (p ^ n.val : K) = 0 := mod_cast h₂ ▸ Nat.cast_card_eq_zero K
  rw [CharP.charP_iff_prime_eq_zero h₁]
  simpa only [ne_eq, PNat.ne_zero, not_false_eq_true, pow_eq_zero_iff] using this

[Junyan Xu]

There's also docs#iterateFrobenius but here's a pure rewrite proof without using frobenius:

import Mathlib

open scoped Polynomial

lemma foo (k : Type*) [Field k] [Fintype k] (f : k[X]) (L : Type*) [CommRing L] [Algebra k L]
    (t : L) : f.eval₂ (algebraMap k L) (t^(Fintype.card k)) =
              (f.eval₂ (algebraMap k L) t)^(Fintype.card k) := by
  simp_rw [← Polynomial.aeval_def] -- `eval₂ (algebraMap k L)` is just `aeval`
  rw [← map_pow, ← FiniteField.expand_card, Polynomial.expand_aeval]

[Kevin Buzzard]

Thanks a lot! We're on the way to Frobenius :-)

[Eric Wieser]

Iseval2 (algebraMap _ _) the same as aeval?