Theory Perfect_Field_Altdef

(*
  File:      Perfect_Fields/Perfect_Field_Altdef.thy
  Authors:   Katharina Kreuzer (TU München)
             Manuel Eberl (University of Innsbruck)

  Proof that a field where every irreducible polynomial is separable is perfect.
  This effectively shows that our definition is equivalent to the textbook one.

  We put this in a separate file because importing HOL-Algebra.Algebraic_Closure
  comes with a lot of annoying baggage that we don't want to pollute our namespace
  with.
*)
subsection ‹Alternative definition of perfect fields›
theory Perfect_Field_Altdef
imports 
  "HOL-Algebra.Algebraic_Closure_Type"
  Perfect_Fields
begin

text ‹
  In the following, we will show that our definition of perfect fields is equivalent
  to the usual textbook one (for example \cite{conrad}). 
That is: a field in which every irreducible polynomial is separable
  (or, equivalently, has non-zero derivative) either has characteristic $0$ or a surjective
  Frobenius endomorphism.

  The proof works like this:

  Let's call our field K› with prime characteristic p›.
  Suppose there were some c ∈ K› that is not a p›-th root.
  The polynomial $P := X^p - c$ in $K[X]$ clearly has a zero derivative and is therefore
  not separable. By our assumption, it must then have a monic non-trivial factor
  $Q \in K[X]$.

  Let L› be some field extension of K› where c› does have a p›-th root α› (in our
  case, we choose L› to be the algebraic closure of K›).

  Clearly, Q› is also a non-trivial factor of P› in L›. However, we also
  have P = X^p - c = X^p - α^p = (X - α)^p›, so we must have $Q = (X - \alpha )^m$
  for some 0 ≤ m < p› since X - α› is prime.

  However, the coefficient of $X^{m-1}$ in $(X - \alpha )^m$ is -mα›, and since
  Q ∈ K[X]› we must have -mα ∈ K› and therefore α ∈ K›.
›
theorem perfect_field_alt:
  assumes "p :: 'a :: field_gcd poly. Factorial_Ring.irreducible p  pderiv p  0"
  shows   "CHAR('a) = 0  surj (frob :: 'a  'a)"
proof (cases "CHAR('a) = 0")
  case False
  let ?p = "CHAR('a)"
  from False have "Factorial_Ring.prime ?p"
    by (simp add: prime_CHAR_semidom)
  hence "?p > 1"
    using prime_gt_1_nat by blast
  note p = Factorial_Ring.prime ?p ?p > 1

  interpret to_ac: map_poly_inj_comm_ring_hom "to_ac :: 'a  'a alg_closure"
    by unfold_locales auto

  have "surj (frob :: 'a  'a)"
  proof safe
    fix c :: 'a
    obtain α :: "'a alg_closure" where α: "α ^ ?p = to_ac c"
      using p nth_root_exists[of ?p "to_ac c"] by auto
    define P where "P = Polynomial.monom 1 ?p + [:-c:]"
    define P' where "P' = map_poly to_ac P"
    have deg: "Polynomial.degree P = ?p"
      unfolding P_def using p by (subst degree_add_eq_left) (auto simp: degree_monom_eq)

    have "[:-α, 1:] ^ ?p = ([:0, 1:] + [:-α:]) ^ ?p"
      by (simp add: one_pCons)
    also have " = [:0, 1:] ^ ?p - [:α^?p:]"
      using p by (subst freshmans_dream) (auto simp: poly_const_pow minus_power_prime_CHAR)
    also have "α ^ ?p = to_ac c"
      by (simp add: α)
    also have "[:0, 1:] ^ CHAR('a) - [:to_ac c:] = P'"
      by (simp add: P_def P'_def to_ac.hom_add to_ac.hom_power 
               to_ac.base.map_poly_pCons_hom monom_altdef)
    finally have eq: "P' = [:-α, 1:] ^ ?p" ..

    have "¬is_unit P" "P  0"
      using deg p by auto
    then obtain Q where Q: "Factorial_Ring.prime Q" "Q dvd P"
      by (metis prime_divisor_exists)
    have "monic Q"
      using unit_factor_prime[OF Q(1)] by (auto simp: unit_factor_poly_def one_pCons)

    from Q(2) have "map_poly to_ac Q dvd P'"
      by (auto simp: P'_def)
    hence "map_poly to_ac Q dvd [:-α, 1:] ^ ?p"
      by (simp add: P' = [:-α, 1:] ^ ?p)
    moreover have "Factorial_Ring.prime_elem [:-α, 1:]"
      by (intro prime_elem_linear_field_poly) auto
    hence "Factorial_Ring.prime [:-α, 1:]"
      unfolding Factorial_Ring.prime_def by (auto simp: normalize_monic)
    ultimately obtain m where "m  ?p" "normalize (map_poly to_ac Q) = [:-α, 1:] ^ m"
      using divides_primepow by blast
    hence "map_poly to_ac Q = [:-α, 1:] ^ m"
      using monic Q by (subst (asm) normalize_monic) auto
    moreover from this have "m > 0"
      using Q by (intro Nat.gr0I) auto
    moreover have "m  ?p"
    proof
      assume "m = ?p"
      hence "Q = P"
        using map_poly to_ac Q = [:-α, 1:] ^ m eq
        by (simp add: P'_def to_ac.injectivity)
      with Q have "Factorial_Ring.irreducible P"
        using idom_class.prime_elem_imp_irreducible by blast
      with assms have "pderiv P  0"
        by blast
      thus False
        by (auto simp: P_def pderiv_add pderiv_monom of_nat_eq_0_iff_char_dvd)
    qed
    ultimately have m: "m  {0<..<?p}" "map_poly to_ac Q = [:-α, 1:] ^ m"
      using m  ?p by auto

    from m(1) have "¬?p dvd m"
      using p by auto
    have "poly.coeff ([:-α, 1:] ^ m) (m - 1) = - of_nat (m choose (m - 1)) * α"
      using m(1) by (subst coeff_linear_poly_power) auto
    also have "m choose (m - 1) = m"
      using 0 < m by (subst binomial_symmetric) auto
    also have "[:-α, 1:] ^ m = map_poly to_ac Q"
      using m(2) ..
    also have "poly.coeff  (m - 1) = to_ac (poly.coeff Q (m - 1))"
      by simp
    finally have "α = to_ac (-poly.coeff Q (m - 1) / of_nat m)"
      using m(1) p ¬?p dvd m by (auto simp: field_simps of_nat_eq_0_iff_char_dvd)
    hence "(- poly.coeff Q (m - 1) / of_nat m) ^ ?p = c"
      using α by (metis to_ac.base.eq_iff to_ac.base.hom_power)
    thus "c  range frob"
      unfolding frob_def by blast
  qed auto
  thus ?thesis ..
qed auto

corollary perfect_field_alt':
  assumes "p :: 'a :: field_gcd poly. Factorial_Ring.irreducible p  Rings.coprime p (pderiv p)"
  shows   "CHAR('a) = 0  surj (frob :: 'a  'a)"
proof (rule perfect_field_alt)
  fix p :: "'a poly"
  assume p: "Factorial_Ring.irreducible p"
  with assms[OF p] show "pderiv p  0"
    by auto
qed

end