Gal(F_{p^n}:Z_p) is a cyclic group of order n.

Stream: mathlib4

[张守信(Shouxin Zhang)]

I'm working on formalizing this proof. Since this conclusion is quite classical, I thought there might be such a conclusion in the Mathlib4 library. However, after searching, I found that there isn't one. So, I wrote some rather unattractive code to formalize this conclusion.

import Mathlib
set_option maxHeartbeats 0
open Polynomial

variable (p : ℕ) [prime : Fact p.Prime] (n : ℕ)

instance one_lt_p : 1 < p := (@Nat.Prime.one_lt p Fact.out)
noncomputable instance : Fintype (GaloisField p n) := by
  exact Fintype.ofFinite (GaloisField p n)

theorem frobenius_generates (hn : n ≠ 0):
  IsCyclic (GaloisField p n ≃ₐ[ZMod p] GaloisField p n) := by
  apply isCyclic_iff_exists_ofOrder_eq_natCard.mpr ?_
  have : Nat.card (GaloisField p n ≃ₐ[ZMod p] GaloisField p n) = n := by
    rw [Nat.card_eq_fintype_card, IsGalois.card_aut_eq_finrank, GaloisField.finrank p hn]
  set f := frobeniusEquiv (GaloisField p n) p with hf
  let frobeniusAlgEquiv : GaloisField p n ≃ₐ[ZMod p] GaloisField p n := by
    apply AlgEquiv.ofRingEquiv (f := f)
    intro x
    simp only [f, frobeniusEquiv_apply, Algebra.algebraMap_eq_smul_one, frobenius_def, _root_.smul_pow, ZMod.pow_card, one_pow]
  use frobeniusAlgEquiv
  have h₁ : orderOf frobeniusAlgEquiv ≤ n := by
    simp_rw [← this, Nat.card_eq_fintype_card]
    exact orderOf_le_card_univ
  have h₂ : n ≤ orderOf frobeniusAlgEquiv := by
    have roots_count : ∀ x : GaloisField p n, x^(p^(orderOf frobeniusAlgEquiv)) = x := by
      intro x
      have iter_pow : ∀ k : ℕ, (frobeniusAlgEquiv^k) x = x^(p^k) := by
        intro k
        induction' k with k hk
        . simp only [pow_zero, AlgEquiv.one_apply, pow_one]
        . show (frobeniusAlgEquiv^k * frobeniusAlgEquiv) x = _
          rw [pow_mul_comm', AlgEquiv.mul_apply, hk, AlgEquiv.ofRingEquiv_apply, frobeniusEquiv_def]
          ring
      specialize iter_pow (orderOf frobeniusAlgEquiv)
      simp only [pow_orderOf_eq_one frobeniusAlgEquiv, AlgEquiv.one_apply] at iter_pow
      exact iter_pow.symm
    have h_roots : Nat.card (GaloisField p n) ≤ p^(orderOf frobeniusAlgEquiv) := by
      set r := orderOf frobeniusAlgEquiv with hr
      have zero_lt_r : 0 < r := orderOf_pos frobeniusAlgEquiv
      have one_le_p_pow_r : 1 < p^r := by
        exact Nat.one_lt_pow zero_lt_r.ne.symm (one_lt_p p)
      let poly := (X^(p^r) - X : (GaloisField p n)[X])
      have degree_eq : Polynomial.natDegree poly = p^r := by
        dsimp only [poly]
        compute_degree!
        . simp [one_le_p_pow_r.ne]
        . exact one_le_p_pow_r.le
      rw [← degree_eq, Nat.card_eq_fintype_card]
      apply Polynomial.card_le_degree_of_subset_roots
      intro x _
      apply (mem_roots_iff_aeval_eq_zero ?_).mpr ?_
      . apply Polynomial.ne_zero_of_natDegree_gt (n := 1)
        simp only [degree_eq, Nat.one_lt_pow zero_lt_r.ne.symm (one_lt_p p)]
      . simp only [coe_aeval_eq_eval, eval_sub, eval_pow, eval_X, poly, roots_count, sub_eq_zero]
    rw [GaloisField.card p n hn, pow_le_pow_iff_right₀ (one_lt_p p)] at h_roots
    exact h_roots
  linarith

Therefore, can this conclusion ultimately be accomplished concisely using the library API?

[Riccardo Brasca]

I am not sure this is already somewhere, but anyway rather than saying that the group is cyclic we surely prefer the fact the frobenius generates it.

[张守信(Shouxin Zhang)]

Riccardo Brasca said:

I am not sure this is already somewhere, but anyway rather than saying that the group is cyclic we surely prefer the fact the frobenius generates it.

Based on my code, the elements of my cyclic group will be generated by Frobenius. Additionally, I searched for Frobenius AlgEquiv in the library but couldn't find it, so I created one myself. This resulted in a decrease in the standardization of my code.

[Riccardo Brasca]

Yes, this is what you prove, but your statement is IsCyclic ... and Lean will forget about the proof. I am just suggesting to modify the statement.