Algebraic Conjugate over Finite Fields

Stream: Is there code for X?

[Gian Cordana Sanjaya]

Hello,

Is there a code for one of the following results: Let q = p^k, where p is prime and k >= 1. Then...

1. For any x \in F_q, any algebraic conjugate of x is of form x^{p^m} for some 0 <= m < k.
2. The Galois group of F_q/F_p consists of iterations of Frobenius endomorphisms.

[Junyan Xu]

After some search I did not find the exact result in mathlib . However, at least we know docs#galois_field.is_galois, where galois_field is the construction of a finite field of cardinality p^k as splitting field of x^(p^k)-1. And we know that every finite field is equivalent to a galois_field (docs#galois_field.alg_equiv_galois_field).

The Galois group Gal(E/F) is spelt E ≃ₐ[F] E in mathlib, and docs#frobenius is just a ring homomorphism and doesn't seem to have a alg_hom (over zmod p) version, but it's easy to see it fixes zmod p. Then docs#normal.alg_hom_equiv_aut gets you from alg_hom to alg_equiv (≃ₐ). So there's a homomorphism from multiplicative (zmod k) to Gal(F_q/F_p) using docs#zmod.lift and docs#finite_field.frobenius_pow, and it is injective because a X^(p^k)-X cannot have more than p^k roots when k < n. Finally use docs#is_galois.card_aut_eq_finrank to conclude it's an isomorphism. Hope this helps!

[Gian Cordana Sanjaya]

I'll try this method and see if I can make it work. Thank you very much!

[Kevin Buzzard]

Yeah these would be nice additions! Do we even have Galois conjugates?

[Gian Cordana Sanjaya]

Hmm... I can't find one. Maybe that should be added first. I don't know what results should we add for algebraic conjugates though.

[Kevin Buzzard]

The concept is a bit delicate because for an algebraic non-Galois extension you can still define an equivalence relation on the top field by "we have the same min poly over the bottom field" but recent discussions about normal closures in #maths have convinced me that it's not obviously a useful notion.

[Kevin Buzzard]

In the algebraic normal (perhaps infinite, perhaps nonseparable) case is it true that if two elements of the top field have the same min poly then there's an automorphism of the top field sending one to the other? Probably this can be extracted from what we have if it's true

[Kevin Buzzard]

One thing we don't have, as far as I know, is that L/K is normal iff any K-alg hom from L to any other K-field has image independent of the hom. I'm in the process of adding that in a branch called something like kbuzzard-normal-universal (on mobile, sorry)

[Junyan Xu]

In the algebraic normal (perhaps infinite, perhaps nonseparable) case is it true that if two elements of the top field have the same min poly then there's an automorphism of the top field sending one to the other? Probably this can be extracted from what we have if it's true

Just use
https://leanprover-community.github.io/mathlib_docs/field_theory/normal.html#alg_equiv.lift_normal ?

[Gian Cordana Sanjaya]

I'm confused with using docs#normal.alg_hom_equiv_aut to get the alg_equiv. So instead, I'm trying to prove that φ^n = 1, use that to get a perfect ring instance for F_q, and get frobenius_equiv from that instance.

[Eric Rodriguez]

I'm surprised we don't have that yet! What are you confused about docs#normal.alg_hom_equiv_aut?

[Eric Rodriguez]

I'll also say, a def I told myself to write a while ago is a theoretical def power_basis.map_conjugate (s : S) (pb : power_basis R S) (h : pb.minpoly_gen = minpoly R s) : power_basis R S , which, using docs#power_basis.lift, should immediately give you the correct results. The problem with this was that figuring out the right conditions is hard; it definitely works for fields, but I'm not sure if it even generalises at all from there. (The proof from fields is simple, but a bit finicky in Lean). I wonder if this is the important thing we're missing

[Gian Cordana Sanjaya]

I'm surprised we don't have that yet! What are you confused about docs#normal.alg_hom_equiv_aut?

I've deleted my code that uses it. Now I'm trying to remember...

[Gian Cordana Sanjaya]

So I tried using this line:

def frobenius_alg (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] : R →ₐ[zmod p] R :=
{ commutes' := λ r, by rw [ring_hom.to_fun_eq_coe, ← ring_hom.map_frobenius, zmod.frobenius_zmod, ring_hom.id_apply],
  .. frobenius R p }

def frobenius_alg_equiv (p : ℕ) [fact p.prime] (n : ℕ) (h : 0 < n) : galois_field p n ≃ₐ[zmod p] galois_field p n :=
  normal.alg_hom_equiv_aut (zmod p) (galois_field p n) (galois_field p n) (frobenius_alg (galois_field p n) p)

But then I got an error message like this:
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized galois_field.algebra p n inferred zmod.algebra (galois_field p n) p

Aside: Should we a good alternative notation for galois_field p n, like GF(p, n) or something like that?

[Eric Rodriguez]

aah dear lord there's a diamond, can you try do something like (on the lines before this) do local attribute [-instance] galois_field.algebra?

[Eric Rodriguez]

I'm in favour of a notation; galois_field is relatively new!

[Gian Cordana Sanjaya]

Good news: the line now works. Thanks!

[Gian Cordana Sanjaya]

I'm now stuck at this line.

theorem frobenius_pow_eq_one (p : ℕ) [fact p.prime] (n : ℕ) (h : 0 < n) :
    (frobenius (galois_field p n) p) ^ n = 1 :=
  finite_field.frobenius_pow (card p n (ne_of_gt h))

noncomputable instance perfect_ring (p : ℕ) [fact p.prime] (n : ℕ) (h : 0 < n) : perfect_ring (galois_field p n) p :=
{ pth_root' := (frobenius (galois_field p n) p)^[n.pred],
  frobenius_pth_root' := λ x,
    by rw [← function.comp_app (frobenius _ p), function.comp_iterate_pred_of_pos _ h,
           ← ring_hom.coe_pow, frobenius_pow_eq_one p n h, ring_hom.coe_one, id.def],
  pth_root_frobenius' := λ x,
    by rw [← function.comp_app ((frobenius _ p) ^[n.pred]), function.iterate_pred_comp_of_pos _ h,
           ← ring_hom.coe_pow, frobenius_pow_eq_one p n h, ring_hom.coe_one, id.def] }

noncomputable def frobenius_alg_of_zmod (p : ℕ) [fact p.prime] (n : ℕ) (h : 0 < n) :
    (zmod n) → additive (galois_field p n ≃ₐ[zmod p] (galois_field p n)) :=
  zmod.lift (frobenius_alg_of_int (galois_field p n) p)

In the bottom definition, frobenius_alg_of_int is a map ℤ → (R ≃ₐ[zmod p] R) defined by 1 ↦ frobenius. Now I'm stuck because Lean tells me it fails to synthesize type class instance for perfect_ring (galois_field p n) p... which is the instance I defined right above it.

[Eric Rodriguez]

can you post your imports as well so we can just copy+paste everything in? (#mwe)

[Gian Cordana Sanjaya]

Alright.

import
  field_theory.galois
  field_theory.normal
  field_theory.finite.galois_field
  data.zmod.algebra

universe u



def frobenius_alg_of_int (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] [perfect_ring R p] :
  ℤ →+ additive (R ≃ₐ[zmod p] R) := sorry



namespace galois_field

local attribute [-instance] galois_field.algebra



theorem frobenius_pow_eq_one (p : ℕ) [fact p.prime] (n : ℕ) (h : 0 < n) :
    (frobenius (galois_field p n) p) ^ n = 1 :=
  finite_field.frobenius_pow (card p n (ne_of_gt h))

noncomputable instance perfect_ring (p : ℕ) [fact p.prime] (n : ℕ) (h : 0 < n) :
  perfect_ring (galois_field p n) p :=
{ pth_root' := (frobenius (galois_field p n) p)^[n.pred],
  frobenius_pth_root' := λ x,
    by rw [← function.comp_app (frobenius _ p), function.comp_iterate_pred_of_pos _ h,
           ← ring_hom.coe_pow, frobenius_pow_eq_one p n h, ring_hom.coe_one, id.def],
  pth_root_frobenius' := λ x,
    by rw [← function.comp_app ((frobenius _ p) ^[n.pred]), function.iterate_pred_comp_of_pos _ h,
           ← ring_hom.coe_pow, frobenius_pow_eq_one p n h, ring_hom.coe_one, id.def] }

noncomputable def frobenius_alg_of_zmod (p : ℕ) [fact p.prime] (n : ℕ) (h : 0 < n) :
    (zmod n) → additive (galois_field p n ≃ₐ[zmod p] (galois_field p n)) :=
  zmod.lift (frobenius_alg_of_int (galois_field p n) p)



end galois_field

Edit: Uh my bad, the previous one wasn't minimal. Should be trimmed good enough now.

[Eric Rodriguez]

Sorry Gian, this slipped my mind - I'm away from the computer today, but I'll have a look at this tomorrow, if someone hasn't helped you yet

[Gian Cordana Sanjaya]

No problem.

[Alex J. Best]

So the problem with the instance is that it has an argument that lean can't supply automatically, the 0 < n hypothesis for the instance. The linter (type #lint) at the end of the file will tell you about this sort of problem.
There are a couple of ways to fix this sort of thing.

• You could remove the hypothesis, as when n = 0 we have galois_field p 0 is just zmod p again the result should still be true.
• use docs#fact to put the fact that n is positive into the typeclass system, you can see examples of this in file#data/zmod/basic

[Alex J. Best]

I'm talking about the instance instance perfect_ring you have written

[Ruben Van de Velde]

Or use pnat / n + 1

[Alex J. Best]

Yeah I guess it depends what you want to do with it. Ideally the instance should fire for explicit small primes. I'm not sure how to do that with making the instance for a Coe of a pnat?

[Gian Cordana Sanjaya]

Thanks for the suggestions. I'm now using [fact (0 < n)]; I think handling the case n = 0 will require case divisions for the instance perfect_ring and I want to avoid it for now. Maybe it will be the better alternative.

[Alex J. Best]

I got a bit bored and did the zero case, hope its useful

import
  field_theory.galois
  field_theory.normal
  field_theory.finite.galois_field
  data.zmod.algebra

universe u



def frobenius_alg_of_int (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] [perfect_ring R p] :
  ℤ →+ additive (R ≃ₐ[zmod p] R) := sorry



namespace galois_field

section



theorem frobenius_pow_eq_one (p : ℕ) [fact p.prime] (n : ℕ) :
    (frobenius (galois_field p n) p) ^ n = 1 :=
begin
  rcases (eq_zero_or_pos : n = 0 ∨ _) with rfl | h,
  simp,
  exact finite_field.frobenius_pow (card p n (ne_of_gt h)),
end


open polynomial
open_locale polynomial
  --used in normal.of_is_splitting_field too
instance is_splitting_field_self {F : Type*} [field F] :
  is_splitting_field F F 0 := ⟨splits_zero _, subsingleton.elim _ _⟩
   -- TODO Const and X sub C versions? anything obviously small degree

local attribute [-instance] zmod.algebra

noncomputable
def galois_field_zero_equiv_zmod (p : ℕ) [fact p.prime] : galois_field p 0 ≃ₐ[zmod p] zmod p :=
begin
  symmetry,
  convert polynomial.is_splitting_field.alg_equiv _ (X ^ (p ^ 0) - X : polynomial (zmod p)),
  simp,
  apply_instance,
end

@[simp]
lemma card_galois_field_zero (p : ℕ) [fact p.prime] : fintype.card (galois_field p 0) = p :=
by simp [← fintype.card_of_bijective (galois_field_zero_equiv_zmod p).symm.bijective]

noncomputable instance perfect_ring (p : ℕ) [fact p.prime] (n : ℕ) :
  perfect_ring (galois_field p n) p :=
{ pth_root' := (frobenius (galois_field p n) p)^[n.pred],
  frobenius_pth_root' := λ x,
    begin
      rcases eq_or_ne n 0 with rfl | hn,
      { rw [← pow_one (frobenius (galois_field p _) p), finite_field.frobenius_pow];
        simp, },
      rw ← zero_lt_iff at hn,
      rw [← function.comp_app (frobenius _ p), function.comp_iterate_pred_of_pos _ hn,
           ← ring_hom.coe_pow, frobenius_pow_eq_one p n, ring_hom.coe_one, id.def],
    end,
  pth_root_frobenius' := λ x,
    begin
      rcases eq_or_ne n 0 with rfl | hn,
      { rw [← pow_one (frobenius (galois_field p _) p), finite_field.frobenius_pow];
        simp, },
      rw ← zero_lt_iff at hn,
      rw [← function.comp_app ((frobenius _ p) ^[n.pred]), function.iterate_pred_comp_of_pos _ hn,
            ← ring_hom.coe_pow, frobenius_pow_eq_one p n, ring_hom.coe_one, id.def],
    end }
end

noncomputable def frobenius_alg_of_zmod (p : ℕ) [fact p.prime] (n : ℕ) (h : 0 < n) :
    (zmod n) → additive (galois_field p n ≃ₐ[zmod p] (galois_field p n)) :=
  zmod.lift n (frobenius_alg_of_int (galois_field p n) p)



end galois_field

[Gian Cordana Sanjaya]

I changed some eq_or_ne with eq_zero_or_pos. After some addition, now it looks like this:

import
  field_theory.galois
  field_theory.normal
  field_theory.finite.galois_field
  data.zmod.algebra

universe u



def frobenius_alg (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] :
  R →ₐ[zmod p] R :=
{ commutes' := λ r, by rw [ring_hom.to_fun_eq_coe,
    ← ring_hom.map_frobenius, zmod.frobenius_zmod, ring_hom.id_apply],
  .. frobenius R p }

def pth_root_alg (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] : R →ₐ[zmod p] R :=
{ commutes' := λ r, by rw [ring_hom.to_fun_eq_coe, eq_comm, eq_pth_root_iff,
    ← ring_hom.map_frobenius, zmod.frobenius_zmod, ring_hom.id_apply],
  .. pth_root R p }

def frobenius_alg_equiv (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] : R ≃ₐ[zmod p] R :=
{ inv_fun := pth_root_alg R p,
  left_inv := by unfold frobenius_alg pth_root_alg; simp; exact left_inverse_pth_root_frobenius,
  right_inv := by unfold frobenius_alg pth_root_alg; simp; exact right_inverse_pth_root_frobenius,
  .. frobenius_alg R p }

def frobenius_of_int (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] : ℤ →+ additive (R ≃+* R) :=
{ to_fun := λ n, additive.of_mul ((frobenius_equiv R p) ^ n),
  map_zero' := by rw [zpow_zero, of_mul_one],
  map_add' := λ x y, by rw [zpow_add, of_mul_mul] }

def frobenius_alg_of_int (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] : ℤ →+ additive (R ≃ₐ[zmod p] R) :=
{ to_fun := λ n, additive.of_mul ((frobenius_alg_equiv R p) ^ n),
  map_zero' := by rw [zpow_zero, of_mul_one],
  map_add' := λ x y, by rw [zpow_add, of_mul_mul] }



namespace galois_field

section



theorem frobenius_pow_eq_one (p : ℕ) [fact p.prime] (n : ℕ) :
    (frobenius (galois_field p n) p) ^ n = 1 :=
begin
  rcases (eq_zero_or_pos : n = 0 ∨ _) with rfl | h,
  simp,
  exact finite_field.frobenius_pow (card p n (ne_of_gt h)),
end


open polynomial
open_locale polynomial
  --used in normal.of_is_splitting_field too
instance is_splitting_field_self {F : Type*} [field F] :
  is_splitting_field F F 0 := ⟨splits_zero _, subsingleton.elim _ _⟩
   -- TODO Const and X sub C versions? anything obviously small degree

local attribute [-instance] zmod.algebra

noncomputable
def galois_field_zero_equiv_zmod (p : ℕ) [fact p.prime] : galois_field p 0 ≃ₐ[zmod p] zmod p :=
begin
  symmetry,
  convert polynomial.is_splitting_field.alg_equiv _ (X ^ (p ^ 0) - X : polynomial (zmod p)),
  simp,
  apply_instance,
end

@[simp]
lemma card_galois_field_zero (p : ℕ) [fact p.prime] : fintype.card (galois_field p 0) = p :=
by simp [← fintype.card_of_bijective (galois_field_zero_equiv_zmod p).symm.bijective]

noncomputable instance perfect_ring (p : ℕ) [fact p.prime] (n : ℕ) :
  perfect_ring (galois_field p n) p :=
{ pth_root' := (frobenius (galois_field p n) p)^[n.pred],
  frobenius_pth_root' := λ x,
    begin
      rcases n.eq_zero_or_pos with rfl | hn,
      { rw [← pow_one (frobenius (galois_field p _) p), finite_field.frobenius_pow];
        simp, },
      rw [← function.comp_app (frobenius _ p), function.comp_iterate_pred_of_pos _ hn,
           ← ring_hom.coe_pow, frobenius_pow_eq_one p n, ring_hom.coe_one, id.def],
    end,
  pth_root_frobenius' := λ x,
    begin
      rcases n.eq_zero_or_pos with rfl | hn,
      { rw [← pow_one (frobenius (galois_field p _) p), finite_field.frobenius_pow];
        simp, },
      rw [← function.comp_app ((frobenius _ p) ^[n.pred]), function.iterate_pred_comp_of_pos _ hn,
            ← ring_hom.coe_pow, frobenius_pow_eq_one p n, ring_hom.coe_one, id.def],
    end }
end

theorem frobenius_alg_pow_eq_zero (p : ℕ) [fact p.prime] (n : ℕ) :
  frobenius_alg_of_int (galois_field p n) p n = 0 :=
begin
  unfold frobenius_alg_of_int; simp,
  apply alg_equiv.ext; intros a; simp,
  ---- I don't know how to change the goal into `(frobenius (galois_field p n) p ^ n) a = a`
  sorry,
end

local attribute [-instance] galois_field.algebra

noncomputable def frobenius_alg_of_zmod' (p : ℕ) [fact p.prime] (n : ℕ) :
    zmod n →+ additive (galois_field p n ≃ₐ[zmod p] galois_field p n) :=
  zmod.lift n ⟨frobenius_alg_of_int (galois_field p n) p, frobenius_alg_pow_eq_zero p n⟩

local attribute [instance] galois_field.algebra zmod.algebra

theorem frobenius_alg_of_zmod_bij (p : ℕ) [fact p.prime] (n : ℕ) [fact (0 < n)] :
  function.bijective (frobenius_alg_of_zmod' p n) :=
begin
  rw [fintype.bijective_iff_injective_and_card, and_comm]; split,

  ---- First show that the cardinality are equal
  -- this line fails: rw [zmod.card, fintype.of_equiv_card (@additive.of_mul (galois_field p n ≃ₐ[zmod p] galois_field p n))],
  sorry,

  ---- Now show that the function is injective
  sorry,
end

noncomputable def frobenius_alg_of_zmod (p : ℕ) [fact p.prime] (n : ℕ) [fact (0 < n)] :
    (zmod n) ≃+ additive (galois_field p n ≃ₐ[zmod p] galois_field p n) :=
  add_equiv.of_bijective (frobenius_alg_of_zmod' p n) (frobenius_alg_of_zmod_bij p n)




end galois_field

[Gian Cordana Sanjaya]

Also, I'm curious about these:

1. Would it be better to directly prove the result for any finite field of size p^n?
2. Should we make a bijection between zmod n and ℤ / nℤ? So, instead of working over zmod n, we use quotient_group and the first isomorphism theorem to get the desired isomorphism.
3. I feel like the frobenius_alg_of_int map could be re-written, but I don't know how.

[Junyan Xu]

3. I think this definition is nicer:

def frobenius_alg_of_int (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] : ℤ →+ additive (R ≃ₐ[zmod p] R) :=
(zpowers_hom _ (frobenius_alg_equiv R p)).to_additive''

1. I think we should strive to define

def frobenius_alg_equiv_of_zmod (p : ℕ) [fact p.prime]
  {F} [field F] [fintype F] [char_p F p] :
  zmod (finite_dimensional.finrank (zmod p) F) ≃+ additive (F ≃ₐ[zmod p] F) := sorry

such that the forward map is the zmod.lift of (zpowers_hom _ (frobenius_alg_equiv F p)).to_additive'', which probably has the best defeq property. I don't know a general description of the inverse map, so maybe just construct it "by choice" from bijectivity. These are the only data involved in this definition; the rest are proofs and we don't care how proofs are done, and you are free to use equivalence with galois_field to complete the proofs.

2. We have docs#int.quotient_span_equiv_zmod but I don't think we need to invoke it.

Finally, I was able to fill in your first two sorries by introducing two lemmas:

lemma alg_equiv.coe_pow {R A} [comm_semiring R] [semiring A] [algebra R A]
  (f : A ≃ₐ[R] A) (n : ℕ) : ⇑(f ^ n) = (⇑f^[n]) :=
hom_coe_pow _ (by { ext, refl }) (by { intros, ext, refl }) f n

lemma frobenius_alg_of_int_apply (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] (n : ℕ) (r : R) :
  frobenius_alg_of_int R p n r = ((frobenius R p) ^ n) r :=
begin
  change ((frobenius_alg_equiv R p) ^ n) r = _,
  rw [alg_equiv.coe_pow, ring_hom.coe_pow], refl,
end

theorem frobenius_alg_pow_eq_zero (p : ℕ) [fact p.prime] (n : ℕ) :
  frobenius_alg_of_int (galois_field p n) p n = 0 :=
begin
  ext, rw [frobenius_alg_of_int_apply, frobenius_pow_eq_one], refl,
end

theorem frobenius_alg_of_zmod_bij (p : ℕ) [fact p.prime] (n : ℕ) [fact (0 < n)] :
  function.bijective (frobenius_alg_of_zmod' p n) :=
begin
  rw [fintype.bijective_iff_injective_and_card, and_comm]; split,
  ---- First show that the cardinality are equal
  rw [zmod.card, ← fintype.card_congr additive.of_mul, is_galois.card_aut_eq_finrank],
  { symmetry, convert galois_field.finrank p _,
    exact (fact.out (0 < n)).ne.symm },
  ---- Now show that the function is injective
  { sorry },
end

It took me a while to find docs#ring_hom.coe_pow, and the API seems underdeveloped and many lemmas missing.

[Junyan Xu]

With three more lemmas, I am able to close the last sorry. These would be nice additions to mathlib, if they don't already exist. @Gian Cordana Sanjaya Would you try to generalize the proof to all finite fields?

lemma zmod.lift_injective_iff {A} [add_group A] (f : ℤ →+ A) (n : ℕ) (hf : f n = 0) :
  function.injective (zmod.lift n ⟨f, hf⟩) ↔ ∀ k : zmod n, f k = 0 → k = 0 :=
begin
  split; intro h,
  { intros k hk, apply h, convert hk, apply map_zero },
  { intros k l he, rw ← sub_eq_zero at he ⊢, rw ← map_sub at he, exact h _ he },
end

lemma iterate_pow (M : Type u) [monoid M] (n k : ℕ) :
  (λ m : M, m ^ n)^[k] = (λ m : M, m ^ n ^ k) :=
begin
  induction k with k ih,
  { ext, rw [pow_zero, pow_one], refl },
  { ext, rw [function.iterate_succ, pow_succ, pow_mul, ih] },
end

open polynomial
open_locale polynomial
lemma nat_degree_pow_X_sub_X {R} [nontrivial R] [ring R] (n : ℕ) (hn : 1 < n) :
  (X ^ n - X : R[X]).nat_degree = n :=
begin
  convert ← nat_degree_add_eq_left_of_nat_degree_lt _; rw nat_degree_X_pow,
  rw [nat_degree_neg, nat_degree_X], exact hn,
end

theorem frobenius_alg_of_zmod_bij (p : ℕ) [fact p.prime] (n : ℕ) [fact (0 < n)] :
  function.bijective (frobenius_alg_of_zmod' p n) :=
begin
  have hn : n ≠ 0 := (fact.out (0 < n)).ne.symm,
  rw [fintype.bijective_iff_injective_and_card, and_comm]; split,
  ---- First show that the cardinality are equal
  rw [zmod.card, ← fintype.card_congr additive.of_mul, is_galois.card_aut_eq_finrank],
  { symmetry, convert galois_field.finrank p hn },
  ---- Now show that the function is injective
  { unfold frobenius_alg_of_zmod',
    rw zmod.lift_injective_iff,
    intros k h,
    simp only [zmod.lift_apply_apply, ← zmod.nat_cast_val] at h,
    rw alg_equiv.ext_iff at h, by_contra hk,
    let P : (galois_field p n)[X] := X ^ p ^ k.val - X,
    have hPd : P.nat_degree = p ^ k.val,
    { dsimp [P], rw nat_degree_pow_X_sub_X, apply nat.one_lt_pow,
      exacts [nat.pos_of_ne_zero $ mt (zmod.val_eq_zero k).1 hk, (fact.out p.prime).one_lt] },
    have hP : P ≠ 0,
    { intro h, have := congr_arg nat_degree h, rw hPd at this,
      exact pow_ne_zero _ (fact.out p.prime).ne_zero this },
    have hmem : ∀ x, x ∈ P.root_set (galois_field p n),
    { intro x, rw [mem_root_set_iff, map_sub, map_pow, aeval_X, sub_eq_zero],
      { convert h x, rw [frobenius_alg_of_int_apply, ring_hom.coe_pow],
        change _ = ((λ x, x ^ p)^[k.val]) x, rw iterate_pow },
      { exact hP } },
    have hle : p ^ n ≤ P.roots.card,
    { classical, convert ← P.roots.to_finset_card_le,
      convert galois_field.card p n hn, ext, split; intro h,
      { apply finset.mem_univ },
      { rw ← finset.mem_coe, convert hmem a using 3, exact congr_arg roots map_id.symm } },
    have := hle.trans (polynomial.card_roots' P),
    rw [hPd, pow_le_pow_iff] at this,
    exacts [this.not_lt k.val_lt, (fact.out p.prime).one_lt] },
end

[Junyan Xu]

By the way, I never understand why docs#polynomial.root_set is defined to be a set coerced from finset to set. Shouldn't we keep it a finset?

[Junyan Xu]

If anyone spot any lemma above that already exist in mathlib, please let me know! This thread happens to be in the correct stream for this purpose.

[Gian Cordana Sanjaya]

I'll try reconstructing the proof now. I was away doing some random stuff.
I'll also try generalizing; I feel like it will be just nicer as you remove their dependency on the Galois field case.

[Gian Cordana Sanjaya]

Also, I saw that Alex added is_splitting_field_self. I added the case X - c as below, which we can add to mathlib if needed.

  --used in normal.of_is_splitting_field too
instance is_splitting_field_self_zero {F : Type*} [field F] :
  is_splitting_field F F 0 := ⟨splits_zero _, subsingleton.elim _ _⟩

instance is_splitting_field_self_X_sub_C {F : Type*} [field F] {c : F} :
  is_splitting_field F F (X - C c) := ⟨splits_X_sub_C _, subsingleton.elim _ _⟩

[Gian Cordana Sanjaya]

Weirdly enough after updating mathlib to its current state, I cannot solve galois_field_zero_equiv_zmod. I'll send the whole code down, if no one minds; it'll be very long.
@Junyan Xu Thanks for making the rest work!

import
  field_theory.galois
  field_theory.normal
  field_theory.finite.galois_field
  data.zmod.algebra

universe u



def frobenius_alg (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] :
  R →ₐ[zmod p] R :=
{ commutes' := λ r, by rw [ring_hom.to_fun_eq_coe,
    ← ring_hom.map_frobenius, zmod.frobenius_zmod, ring_hom.id_apply],
  .. frobenius R p }

def pth_root_alg (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] : R →ₐ[zmod p] R :=
{ commutes' := λ r, by rw [ring_hom.to_fun_eq_coe, eq_comm, eq_pth_root_iff,
    ← ring_hom.map_frobenius, zmod.frobenius_zmod, ring_hom.id_apply],
  .. pth_root R p }

def frobenius_alg_equiv (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] : R ≃ₐ[zmod p] R :=
{ inv_fun := pth_root_alg R p,
  left_inv := by unfold frobenius_alg pth_root_alg; simp; exact left_inverse_pth_root_frobenius,
  right_inv := by unfold frobenius_alg pth_root_alg; simp; exact right_inverse_pth_root_frobenius,
  .. frobenius_alg R p }

def frobenius_of_int (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] : ℤ →+ additive (R ≃+* R) :=
{ to_fun := λ n, additive.of_mul ((frobenius_equiv R p) ^ n),
  map_zero' := by rw [zpow_zero, of_mul_one],
  map_add' := λ x y, by rw [zpow_add, of_mul_mul] }

def frobenius_alg_of_int (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] : ℤ →+ additive (R ≃ₐ[zmod p] R) :=
(zpowers_hom _ (frobenius_alg_equiv R p)).to_additive''



namespace galois_field

section



theorem frobenius_pow_eq_one (p : ℕ) [fact p.prime] (n : ℕ) :
    (frobenius (galois_field p n) p) ^ n = 1 :=
begin
  rcases (eq_zero_or_pos : n = 0 ∨ _) with rfl | h,
  simp,
  exact finite_field.frobenius_pow (card p n (ne_of_gt h)),
end


open polynomial
open_locale polynomial
  --used in normal.of_is_splitting_field too
instance is_splitting_field_self {F : Type*} [field F] :
  is_splitting_field F F 0 := ⟨splits_zero _, subsingleton.elim _ _⟩
   -- TODO Const and X sub C versions? anything obviously small degree



noncomputable
def galois_field_zero_equiv_zmod (p : ℕ) [fact p.prime] : galois_field p 0 ≃ₐ[zmod p] zmod p :=
begin
  symmetry,
  convert polynomial.is_splitting_field.alg_equiv _ (X ^ (p ^ 0) - X : polynomial (zmod p)),
  apply_instance,
  rw [pow_zero, pow_one, sub_self],
  ---- The lines below this should NOT be necessary
  fconstructor,
  finish,
  simp,
  sorry,
end

@[simp]
lemma card_galois_field_zero (p : ℕ) [fact p.prime] : fintype.card (galois_field p 0) = p :=
by simp [← fintype.card_of_bijective (galois_field_zero_equiv_zmod p).symm.bijective]

noncomputable instance perfect_ring (p : ℕ) [fact p.prime] (n : ℕ) :
  perfect_ring (galois_field p n) p :=
{ pth_root' := (frobenius (galois_field p n) p)^[n.pred],
  frobenius_pth_root' := λ x,
    begin
      rcases n.eq_zero_or_pos with rfl | hn,
      { rw [← pow_one (frobenius (galois_field p _) p), finite_field.frobenius_pow];
        simp, },
      rw [← function.comp_app (frobenius _ p), function.comp_iterate_pred_of_pos _ hn,
           ← ring_hom.coe_pow, frobenius_pow_eq_one p n, ring_hom.coe_one, id.def],
    end,
  pth_root_frobenius' := λ x,
    begin
      rcases n.eq_zero_or_pos with rfl | hn,
      { rw [← pow_one (frobenius (galois_field p _) p), finite_field.frobenius_pow];
        simp, },
      rw [← function.comp_app ((frobenius _ p) ^[n.pred]), function.iterate_pred_comp_of_pos _ hn,
            ← ring_hom.coe_pow, frobenius_pow_eq_one p n, ring_hom.coe_one, id.def],
    end }
end

lemma alg_equiv.coe_pow {R A} [comm_semiring R] [semiring A] [algebra R A]
  (f : A ≃ₐ[R] A) (n : ℕ) : ⇑(f ^ n) = (⇑f^[n]) :=
hom_coe_pow _ (by { ext, refl }) (by { intros, ext, refl }) f n

lemma frobenius_alg_of_int_apply (R : Type u) [comm_ring R] (p : ℕ) [fact p.prime]
  [char_p R p] [perfect_ring R p] (n : ℕ) (r : R) :
  frobenius_alg_of_int R p n r = ((frobenius R p) ^ n) r :=
begin
  change ((frobenius_alg_equiv R p) ^ n) r = _,
  rw [alg_equiv.coe_pow, ring_hom.coe_pow], refl,
end

theorem frobenius_alg_pow_eq_zero (p : ℕ) [fact p.prime] (n : ℕ) :
  frobenius_alg_of_int (galois_field p n) p n = 0 :=
begin
  ext, rw [frobenius_alg_of_int_apply, frobenius_pow_eq_one], refl,
end

local attribute [-instance] galois_field.algebra

noncomputable def frobenius_alg_of_zmod' (p : ℕ) [fact p.prime] (n : ℕ) :
    zmod n →+ additive (galois_field p n ≃ₐ[zmod p] galois_field p n) :=
  zmod.lift n ⟨frobenius_alg_of_int (galois_field p n) p, frobenius_alg_pow_eq_zero p n⟩



lemma zmod.lift_injective_iff {A} [add_group A] (f : ℤ →+ A) (n : ℕ) (hf : f n = 0) :
  function.injective (zmod.lift n ⟨f, hf⟩) ↔ ∀ k : zmod n, f k = 0 → k = 0 :=
begin
  split; intro h,
  { intros k hk, apply h, convert hk, apply map_zero },
  { intros k l he, rw ← sub_eq_zero at he ⊢, rw ← map_sub at he, exact h _ he },
end

lemma iterate_pow (M : Type u) [monoid M] (n k : ℕ) :
  (λ m : M, m ^ n)^[k] = (λ m : M, m ^ n ^ k) :=
begin
  induction k with k ih,
  { ext, rw [pow_zero, pow_one], refl },
  { ext, rw [function.iterate_succ, pow_succ, pow_mul, ih] },
end

open polynomial
open_locale polynomial
lemma nat_degree_pow_X_sub_X {R} [nontrivial R] [ring R] (n : ℕ) (hn : 1 < n) :
  (X ^ n - X : R[X]).nat_degree = n :=
begin
  convert ← nat_degree_add_eq_left_of_nat_degree_lt _; rw nat_degree_X_pow,
  rw [nat_degree_neg, nat_degree_X], exact hn,
end

theorem frobenius_alg_of_zmod_bij (p : ℕ) [fact p.prime] (n : ℕ) [fact (0 < n)] :
  function.bijective (frobenius_alg_of_zmod' p n) :=
begin
  have hn : n ≠ 0 := (fact.out (0 < n)).ne.symm,
  rw [fintype.bijective_iff_injective_and_card, and_comm]; split,
  ---- First show that the cardinality are equal
  rw [zmod.card, ← fintype.card_congr additive.of_mul, is_galois.card_aut_eq_finrank],
  { symmetry, convert galois_field.finrank p hn },
  ---- Now show that the function is injective
  { unfold frobenius_alg_of_zmod',
    rw zmod.lift_injective_iff,
    intros k h,
    simp only [zmod.lift_apply_apply, ← zmod.nat_cast_val] at h,
    rw alg_equiv.ext_iff at h, by_contra hk,
    let P : (galois_field p n)[X] := X ^ p ^ k.val - X,
    have hPd : P.nat_degree = p ^ k.val,
    { dsimp [P], rw nat_degree_pow_X_sub_X, apply nat.one_lt_pow,
      exacts [nat.pos_of_ne_zero $ mt (zmod.val_eq_zero k).1 hk, (fact.out p.prime).one_lt] },
    have hP : P ≠ 0,
    { intro h, have := congr_arg nat_degree h, rw hPd at this,
      exact pow_ne_zero _ (fact.out p.prime).ne_zero this },
    have hmem : ∀ x, x ∈ P.root_set (galois_field p n),
    { intro x, rw [mem_root_set_iff, map_sub, map_pow, aeval_X, sub_eq_zero],
      { convert h x, rw [frobenius_alg_of_int_apply, ring_hom.coe_pow],
        change _ = ((λ x, x ^ p)^[k.val]) x, rw iterate_pow },
      { exact hP } },
    have hle : p ^ n ≤ P.roots.card,
    { classical, convert ← P.roots.to_finset_card_le,
      convert galois_field.card p n hn, ext, split; intro h,
      { apply finset.mem_univ },
      { rw ← finset.mem_coe, convert hmem a using 3, exact congr_arg roots map_id.symm } },
    have := hle.trans (polynomial.card_roots' P),
    rw [hPd, pow_le_pow_iff] at this,
    exacts [this.not_lt k.val_lt, (fact.out p.prime).one_lt] },
end


noncomputable def frobenius_alg_of_zmod (p : ℕ) [fact p.prime] (n : ℕ) [fact (0 < n)] :
    (zmod n) ≃+ additive (galois_field p n ≃ₐ[zmod p] galois_field p n) :=
  add_equiv.of_bijective (frobenius_alg_of_zmod' p n) (frobenius_alg_of_zmod_bij p n)




end galois_field

[Junyan Xu]

noncomputable
def galois_field_zero_equiv_zmod (p : ℕ) [fact p.prime] : galois_field p 0 ≃ₐ[zmod p] zmod p :=
begin
  symmetry,
  convert polynomial.is_splitting_field.alg_equiv _ (X ^ (p ^ 0) - X : polynomial (zmod p)),
  apply_instance,
  { convert galois_field.is_splitting_field_self, simp },
end

This solves the goal (though is_splitting_field_self is in the wrong namespace).

is_splitting_field_self_X_sub_C looks like a nice lemma to have, but I'm not sure if it should be an instance. What do people think?

[Gian Cordana Sanjaya]

Thanks. It works!
It seems that there's no instance of is_galois (zmod p) K for K a finite field of characteristic p. I don't know much about diamonds, but my guess is that it would conflict with is_galois (zmod p) (galois_field p n)?

[Junyan Xu]

I don't think that's a problem; is_galois is a Prop and since any two proofs of the Prop are defeq, there are no diamond problems with Prop-valued classes. is_galois for a finite field would be a nice addition to mathlib, and can be easily proven using docs#is_galois.of_alg_equiv and docs#galois_field.alg_equiv_galois_field (a version with n replaced by finite_dimensional.finrank (zmod p) K) would be easier to use).

[Junyan Xu]

Notice that my proof of the last sorry shares great similarity with src#galois_field.finrank. I think there's potential of extracting lemmas and golfing both proofs.

[Gian Cordana Sanjaya]

Speaking of docs#is_galois.alg_equiv_galois_field uses [algebra (zmod p) K] as an instance as opposed to [char_p K p]. Should it be changed, or is it fine as it?

[Junyan Xu]

You mean docs#galois_field.alg_equiv_galois_field? The choice of [algebra (zmod p) K] is probably intentional. There is such an instance inferred from [char_p K p], but using [algebra (zmod p) K] as an argument allows not only the inferred instance, but possibly other non-defeq instances, like the one from splitting_field (of course we know they are all equal propositionally).

[Gian Cordana Sanjaya]

Ah yes, I mean that. Ah I think I see what you mean now.

[Gian Cordana Sanjaya]

Proof of result generalized to any finite field. Should I send the whole code here, or make a PR through GitHub?

[Junyan Xu]

You are welcome to make a PR, which will make review/comments easier. I just fixed a problem at #14947 and will sleep now; see you tomorrow :)

[Gian Cordana Sanjaya]

Alright, thanks a lot for your help!

[Kevin Buzzard]

@Gian Cordana Sanjaya do you have push access to non master branches of mathlib?

@Junyan Xu you have two accounts here with the same pic so I don't know if I'm tagging the right one, but as you probably know you can access roots as a multiset which is arguably better than a finset.

[Gian Cordana Sanjaya]

I've never asked for any access before, so I'm guessing no. I'll check GitHub though as well.

[Junyan Xu]

@Kevin Buzzard Yes and I'm actually considering a refactor that first shows the number of roots is finite in a domain and each root has finite multiplicity (holds in any nontrivial ring), then synthesize the multiset from the finset + multiplicity. (btw I think you can reach me with either account.)

[Kevin Buzzard]

@Gian Cordana Sanjaya what is your GitHub userid?

[Gian Cordana Sanjaya]

userid: mortarsanjaya

[Mario Carneiro]

invite sent

[Alex J. Best]

Junyan Xu said:

is_splitting_field_self_X_sub_C looks like a nice lemma to have, but I'm not sure if it should be an instance. What do people think?

I think all versions of this with small polynomials should be instances yes, like X_add_C, X, C_mul_X, C_mul_X_add_C, C, maybe there is a clever way to make an instance chain that covers all these, but I cant immediately think of one.

[Gian Cordana Sanjaya]

Some lemmas that were used were not written by me. They also fit on some other files already existing in mathlib. Should I still make the PR for them?

[Gian Cordana Sanjaya]

I also have a question for one of the lemmas in the above category.

lemma lift_injective_iff :
  function.injective (zmod.lift n f) ↔ ∀ k : zmod n, f.val k = 0 → k = 0 :=
begin
  split; intro h,
  { intros k hk, apply h, convert hk, apply map_zero },
  { intros k l he, rw ← sub_eq_zero at he ⊢, rw ← map_sub at he, exact h _ he },
end

Should we make it a simp lemma?

[Kevin Buzzard]

People tend to be not too fussed about precise attribution here -- the goal is to make an amazing mathematics library together. Thanks for asking though! Please go ahead and make the PR.

[Alex J. Best]

:up: what Kevin says, but you can add a co-authored-by line as the last line before the --- in the PR message: https://github.com/leanprover-community/mathlib/blob/master/.github/CONTRIBUTING.md if you want to acknowledge someone as having contributed to the PR (this happens automatically if more than one person pushes commits to a branch).

[Junyan Xu]

I think all versions of this with small polynomials should be instances yes, like X_add_C, X, C_mul_X, C_mul_X_add_C, C, maybe there is a clever way to make an instance chain that covers all these, but I cant immediately think of one.

I think there is the problem that a polynomial can be written in many non-defeq or syntactically different ways, and an enormous amount of instances are needed to cover all combinations, which would probably slow down typeclass inference. For example, X + C r may be written as C r + X or X - C (-r), C r * X ^ n may be written as monomial n r, X can be written as C 1 * X or X ^ 1, etc. So some convert or rewrite would still be necessary in many cases, defying the purpose of instances. Maybe some tactic can put them in a normal form. (I've seen discussion of incorporating compute_degree into norm_num, may be a good idea?)

[Junyan Xu]

BTW, feel free to include lemmas I wrote in your PR!

[Alex J. Best]

I'm only thinking of things which are "syntactically linear" and in a reasonable looking format, but yes its certainly a trade-off between usefulness and not overloading tc-search, seeing as the head symbol is is_splitting_field I wouldn't think this would slow down many other uses of typeclass search.

[Gian Cordana Sanjaya]

Thanks for the comments! Added one small PR, now I'll sleep.

[Eric Wieser]

Just took a look at that PR (#15012); I think you just needed to find docs#injective_iff_map_eq_zero!

[Gian Cordana Sanjaya]

I should have checked first... Replacing them directly doesn't work (rather obviously), but it seems it should work well with some unfolding.

[Junyan Xu]

seems you just need to replace rw [frobenius_alg_of_int_apply, by erw. (at least for my original less general proof)

[Gian Cordana Sanjaya]

I'm thinking of removing alg_equiv.coe_pow, but the only proof I could think of for frobenius_alg_of_int_apply now uses induction on n, which is sort of sad. Would alg_equiv.coe_pow be a good addition? Is induction fine?

import
  field_theory.normal
  field_theory.finite.galois_field
  data.zmod.algebra



---- The definitions in this section does not seem to fit in any current file for some reason
section frobenius

variables (R : Type*) [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p]

/-- Frobenius automorphism as an `alg_hom`. -/
def frobenius_alg : R →ₐ[zmod p] R :=
{ commutes' := λ r, by rw [ring_hom.to_fun_eq_coe,
    ← ring_hom.map_frobenius, zmod.frobenius_zmod, ring_hom.id_apply],
  .. frobenius R p }

/-- `p`-th root of an element in a perfect ring as an `alg_hom`. -/
def pth_root_alg [perfect_ring R p] : R →ₐ[zmod p] R :=
{ commutes' := λ r, by rw [ring_hom.to_fun_eq_coe, eq_comm, eq_pth_root_iff,
    ← ring_hom.map_frobenius, zmod.frobenius_zmod, ring_hom.id_apply],
  .. pth_root R p }

/-- Frobenius automorphism of a perfect ring as an `alg_equiv`. -/
def frobenius_alg_equiv [perfect_ring R p] : R ≃ₐ[zmod p] R :=
{ inv_fun := pth_root R p,
  left_inv := by unfold frobenius_alg pth_root_alg; simp; exact left_inverse_pth_root_frobenius,
  right_inv := by unfold frobenius_alg pth_root_alg; simp; exact right_inverse_pth_root_frobenius,
  .. frobenius_alg R p }

/-- The homomorphism from `int` to the automorphism group of R as a ring,
  sending 1 to `frobenius_equiv`. -/
def frobenius_of_int [perfect_ring R p] : ℤ →+ additive (R ≃+* R) :=
{ to_fun := λ n, additive.of_mul ((frobenius_equiv R p) ^ n),
  map_zero' := by rw [zpow_zero, of_mul_one],
  map_add' := λ x y, by rw [zpow_add, of_mul_mul] }

/-- The homomorphism from `int` to the automorphism group of R as a `zmod p`-algebra,
  sending 1 to `frobenius_alg_equiv`. -/
def frobenius_alg_of_int [perfect_ring R p] : ℤ →+ additive (R ≃ₐ[zmod p] R) :=
(zpowers_hom _ (frobenius_alg_equiv R p)).to_additive''

---- As the name suggest, this fits in alg_equiv section of "algebra/algebra/basic.lean"
lemma alg_equiv.coe_pow {R A} [comm_semiring R] [semiring A] [algebra R A]
  (f : A ≃ₐ[R] A) (n : ℕ) : ⇑(f ^ n) = (⇑f^[n]) :=
hom_coe_pow _ (by { ext, refl }) (by { intros, ext, refl }) f n

lemma frobenius_alg_of_int_apply [perfect_ring R p] (n : ℕ) (r : R) :
  frobenius_alg_of_int R p n r = ((frobenius R p) ^ n) r :=
begin
  change ((frobenius_alg_equiv R p) ^ n) r = _,
  rw [alg_equiv.coe_pow, ring_hom.coe_pow], refl,
end

end frobenius

[Junyan Xu]

file#algebra/hom/iterate has a bunch of coe_pow lemmas and I think we should also add the alg_hom, alg_equiv, ring_equiv, mul_equiv versions. However the file doesn't import the file where alg_hom is defined. I am wondering whether we can generalize to [monoid_hom_class] so we don't need to have multiple versions.

[Junyan Xu]

monoid_hom_class doesn't even cover the version docs#equiv.perm.coe_pow. Maybe we should introduce an [endomorphism_class] which would extend docs#fun_like and docs#monoid, satisfying the conditions in docs#hom_coe_pow? Or should the monoid instance be defined in terms of the fun_like F M (λ _, M)? Notice all the coe_pow lemmas are proved by hom_coe_pow _ rfl (λ f g, rfl) _ _ (the alg_equiv version can too!), so in practice the mul and one are always defeq to function composition and the identity function.

[Gian Cordana Sanjaya]

Hello, can I know what the current state of the result over Gal(F_{p^k}/F_p)?
I didn't actually get this result into mathlib; I gave up at some point for some reason. However, I looked up Mathlib for a while and it seems that we have more theorem put into Mathlib that relates to the goal.

[Shreyas Srinivas]

Gian Cordana Sanjaya said:

Hello, can I know what the current state of the result over Gal(F_{p^k}/F_p)?
I didn't actually get this result into mathlib; I gave up at some point for some reason. However, I looked up Mathlib for a while and it seems that we have more theorem put into Mathlib that relates to the goal.

If it exists you might find it on Moogle

[Junyan Xu]

Not aware of new relevant developments but I think at least the diamond is now fixed :)