Finite field is perfect ring

Stream: Is there code for X?

[Jz Pan]

It seems that there is no PerfectRing instance for finite fields (after searching docs I only found that currently only perfect closure, perfection and algebra closure are PerfectRing). Should I try to add it into mathlib4?

[Riccardo Brasca]

This came up in the stream about the Leidein conference. I proposed

import Mathlib.FieldTheory.PerfectClosure
import Mathlib.FieldTheory.Finite.Basic

variable (K : Type _) [Field K] [Fintype K] (p : ℕ) [inst : CharP K p]

theorem bar :
    have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
    Function.Surjective (frobenius K p) := by
  intro x
  obtain ⟨n, _, hn⟩ := FiniteField.card K p
  refine' ⟨x ^ (p ^ (n - 1)), _⟩
  dsimp [frobenius]
  calc
    _ = x ^ (p ^ (↑n - 1) * p ^ 1) := by rw [← pow_mul, pow_one]
    _ = x ^ (p ^ (↑n - 1 + 1)) := by rw [pow_add]
    _ = x ^ (p ^ ((n : ℕ).pred.succ)) := by rw [Nat.pred_eq_sub_one]
    _ = x ^ (p ^ n) := by rw [Nat.succ_pred n.ne_zero]
    _ = x := by rw [← hn, FiniteField.pow_card _]

noncomputable instance  :
    have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
    PerfectRing K p :=
  have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
  PerfectRing.ofSurjective K _ (bar K p)

@D. J. Bernstein you may be interested in this.

[Johan Commelin]

It's a bit sad that you need to repeat

have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩

so often...

[Riccardo Brasca]

I didn't try to optimize the code at all, so it's very possible it can be improved.

[Oliver Nash]

We could also use [Finite K] (possibly at the cost of have : Fintype K := Fintype.ofFinite K somewhere).

[Oliver Nash]

After all we only care that K is finite, now how!

[Jz Pan]

Oliver Nash said:

We could also use [Finite K] (possibly at the cost of have : Fintype K := Fintype.ofFinite K somewhere).

Currently the finite field API in mathlib4 uses Fintype K but not Finite K.

[Oliver Nash]

I know this but I like to take every opportunity to push Finite. Maybe someone reading this might carry out a reactor of this part of the library to favour Finite over Fintype :wink:

[Eric Wieser]

That docs#PerfectRing instance should be computable, right?

[Eric Wieser]

It's proving surjectivity by defining an explicit inverse, so you should state the stronger result that says the explicit inverse is an inverse

[Eric Wieser]

(thought we might be missing the glue that expresses docs#FiniteField.card as Fintype.card F = p ^ nat.log p (Fintype.card F))

[Jz Pan]

I made the above code shorter:

import Mathlib.FieldTheory.PerfectClosure
import Mathlib.FieldTheory.Finite.Basic

variable (K : Type _) [Field K] [Fintype K] (p : ℕ) [inst : CharP K p]

theorem bar :
    have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
    Function.Surjective (frobenius K p) := fun x => by
  obtain ⟨n, _, hn⟩ := FiniteField.card K p
  use x ^ (p ^ (↑n : ℕ).pred)
  dsimp [frobenius]
  rw [← pow_mul, ← pow_succ',
    ← Nat.succ_eq_add_one, Nat.succ_pred n.ne_zero, ← hn, FiniteField.pow_card]

noncomputable instance  :
    have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
    PerfectRing K p :=
  have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
  PerfectRing.ofSurjective K _ (bar K p)

[Eric Wieser]

Here's the computable version:

import Mathlib.FieldTheory.PerfectClosure
import Mathlib.FieldTheory.Finite.Basic

variable (K : Type _) [Field K] [Fintype K] (p : ℕ) [inst : CharP K p]

theorem bar :
    have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
    Function.RightInverse (fun x : K => x ^ (p ^ (Nat.log p (Fintype.card K)).pred)) (frobenius K p) := fun x => by
  obtain ⟨n, hp, hn⟩ := FiniteField.card K p
  dsimp [frobenius]
  rw [← pow_mul, ← pow_succ',
    ← Nat.succ_eq_add_one, hn, Nat.log_pow hp.one_lt, Nat.succ_pred n.ne_zero, ←hn, FiniteField.pow_card]

instance  :
    have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
    PerfectRing K p :=
  have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
  { pthRoot' := fun x => x ^ (p ^ (Nat.log p (Fintype.card K)).pred)
    frobenius_pthRoot' := bar _ _
    pthRoot_frobenius' := fun _x => frobenius_inj _ _ <| bar K _ _ }

[Jz Pan]

What about adding instance : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩? Then we can remove three haves and from now on, [Field K] [Fintype K] (p : ℕ) [CharP K p] automatically imply Fact (Nat.Prime p). Not sure if this will clash with existing type class instances.

[Eric Wieser]

That instance doesn't work because lean has no way to find K

[Eric Wieser]

Adding [Fact (Nat.Prime p)] to the assumptions is the easy way out

[Oliver Nash]

There is a short proof of this in #6182 (still WIP)