Theory Finite_Fields_Isomorphic

section ‹Isomorphism between Finite Fields\label{sec:uniqueness}›

theory Finite_Fields_Isomorphic
  imports
    Card_Irreducible_Polynomials
begin

lemma (in finite_field) eval_on_root_is_iso:
  defines "p ≡ char R"
  assumes "f ∈ carrier (poly_ring (ZFact p))" 
  assumes "pirreducible⇘(ZFact p)⇙ (carrier (ZFact p)) f" 
  assumes "order R = p^degree f"
  assumes "x ∈ carrier R" 
  assumes "eval (map (char_iso R) f) x = 𝟬"
  shows "ring_hom_ring (Rupt⇘(ZFact p)⇙ (carrier (ZFact p)) f) R 
    (λg. the_elem ((λg'. eval (map (char_iso R) g') x) ` g))"
proof -
  let ?P = "poly_ring (ZFact p)"

  have char_pos: "char R > 0"
    using finite_carr_imp_char_ge_0[OF finite_carrier] by simp

  have p_prime: "Factorial_Ring.prime p" 
    unfolding p_def 
    using characteristic_is_prime[OF char_pos] by simp

  interpret zf: finite_field "ZFact p"
    using zfact_prime_is_finite_field p_prime by simp
  interpret pzf: principal_domain "poly_ring (ZFact p)"
    using zf.univ_poly_is_principal[OF zf.carrier_is_subfield] by simp

  interpret i: ideal "(PIdl⇘?P⇙ f)" "?P" 
    by (intro pzf.cgenideal_ideal assms(2))
  have rupt_carr: "y ⊆ carrier (poly_ring (ZFact p))"
    if "y ∈ carrier (Rupt⇘ZFact p⇙ (carrier (ZFact p)) f)" for y
    using that pzf.quot_carr i.ideal_axioms by (simp add:rupture_def)

  have rupt_is_ring: "ring (Rupt⇘ZFact p⇙ (carrier (ZFact p)) f)"
    unfolding rupture_def by (intro i.quotient_is_ring)

  have "map (char_iso R) ∈ 
    ring_iso ?P (poly_ring (R⦇carrier := char_subring R⦈))"
    using lift_iso_to_poly_ring[OF char_iso] zf.domain_axioms 
    using char_ring_is_subdomain subdomain_is_domain
    by (simp add:p_def)
  moreover have "(char_subring R)[X] = 
    poly_ring (R ⦇carrier := char_subring R⦈)"
    using univ_poly_consistent[OF char_ring_is_subring] by simp
  ultimately have 
    "map (char_iso R) ∈ ring_hom ?P ((char_subring R)[X])"
    by (simp add:ring_iso_def)
  moreover have "(λp. eval p x) ∈ ring_hom ((char_subring R)[X]) R"
    using eval_is_hom char_ring_is_subring assms(5) by simp
  ultimately have 
    "(λp. eval p x) ∘ map (char_iso R) ∈ ring_hom ?P R"
    using ring_hom_trans by blast
  hence a:"(λp. eval (map (char_iso R) p) x) ∈ ring_hom ?P R"
    by (simp add:comp_def)
  interpret h:ring_hom_ring "?P" "R" "(λp. eval (map (char_iso R) p) x)"
    by (intro ring_hom_ringI2 pzf.ring_axioms a ring_axioms)

  let ?h = "(λp. eval (map (char_iso R) p) x)"
  let ?J = "a_kernel (poly_ring (ZFact (int p))) R ?h"

  have "?h ` a_kernel (poly_ring (ZFact (int p))) R ?h ⊆ {𝟬}"
    by auto
  moreover have 
    "𝟬⇘?P⇙ ∈ a_kernel (poly_ring (ZFact (int p))) R ?h" 
    "?h 𝟬⇘?P⇙ = 𝟬" 
    unfolding a_kernel_def' by simp_all
  hence "{𝟬} ⊆ ?h ` a_kernel (poly_ring (ZFact (int p))) R ?h"
    by simp
  ultimately have c:
    "?h ` a_kernel (poly_ring (ZFact (int p))) R ?h = {𝟬}"
    by auto

  have d: "PIdl⇘?P⇙ f ⊆ a_kernel ?P R ?h"
  proof (rule subsetI) 
    fix y assume "y ∈ PIdl⇘?P⇙ f"
    then obtain y' where y'_def: "y' ∈ carrier ?P" "y = y' ⊗⇘?P⇙ f" 
      unfolding cgenideal_def by auto
    have "?h y = ?h (y' ⊗⇘?P⇙ f)" by (simp add:y'_def)
    also have "... = ?h y' ⊗ ?h f"
      using y'_def assms(2) by simp
    also have "... = ?h y' ⊗ 𝟬"
      using assms(6) by simp
    also have "... = 𝟬"
      using y'_def by simp
    finally have "?h y = 𝟬" by simp
    moreover have "y ∈ carrier ?P" using y'_def assms(2) by simp
    ultimately show "y ∈ a_kernel ?P R ?h"
      unfolding a_kernel_def kernel_def by simp
  qed

  have "(λy. the_elem ((λp. eval (map (char_iso R) p) x) ` y)) 
    ∈ ring_hom (?P Quot ?J) R"
    using h.the_elem_hom by simp
  moreover have "(λy. ?J <+>⇘?P⇙ y) 
    ∈ ring_hom (Rupt⇘(ZFact p)⇙ (carrier (ZFact p)) f) (?P Quot ?J)"
    unfolding rupture_def using h.kernel_is_ideal d assms(2)
    by (intro pzf.quot_quot_hom pzf.cgenideal_ideal) auto
  ultimately have "(λy. the_elem (?h ` y)) ∘ (λy. ?J <+>⇘?P⇙ y)
    ∈ ring_hom (Rupt⇘(ZFact p)⇙ (carrier (ZFact p)) f) R"
    using ring_hom_trans by blast
  hence b: "(λy. the_elem (?h ` (?J <+>⇘?P⇙ y))) ∈ 
    ring_hom (Rupt⇘(ZFact p)⇙ (carrier (ZFact p)) f) R"
    by (simp add:comp_def)
  have "?h ` y = ?h ` (?J <+>⇘?P⇙ y)"
    if "y ∈ carrier (Rupt⇘ZFact p⇙ (carrier (ZFact p)) f)"
    for y
  proof -
    have y_range: "y ⊆ carrier ?P"
      using rupt_carr that by simp
    have "?h ` y = {𝟬} <+>⇘R⇙ ?h ` y"
      using y_range h.hom_closed by (subst set_add_zero, auto)
    also have "... = ?h ` ?J <+>⇘R⇙ ?h ` y"
      by (subst c, simp)
    also have "... = ?h ` (?J <+>⇘?P⇙ y)"
      by (subst set_add_hom[OF a _ y_range], subst a_kernel_def') auto
    finally show ?thesis by simp
  qed
  hence "(λy. the_elem (?h ` y)) ∈ 
    ring_hom (Rupt⇘(ZFact p)⇙ (carrier (ZFact p)) f) R"
    by (intro ring_hom_cong[OF _ rupt_is_ring b]) simp
  thus ?thesis
    by (intro ring_hom_ringI2 rupt_is_ring ring_axioms, simp)
qed

lemma (in domain) pdivides_consistent:
  assumes "subfield K R" "f ∈ carrier (K[X])" "g ∈ carrier (K[X])"
  shows "f pdivides g ⟷ f pdivides⇘R ⦇ carrier := K ⦈⇙ g"
proof -
  have a:"subring K R" 
    using assms(1) subfieldE(1) by auto
  let ?S = "R ⦇ carrier := K ⦈"
  have "f pdivides g ⟷ f divides⇘K[X]⇙ g"
    using pdivides_iff_shell[OF assms] by simp
  also have "... ⟷ (∃x ∈ carrier (K[X]). f ⊗⇘K[X]⇙ x = g)"
    unfolding pdivides_def factor_def by auto
  also have "... ⟷ 
    (∃x ∈ carrier (poly_ring ?S). f ⊗⇘poly_ring ?S⇙ x = g)"
    using univ_poly_consistent[OF a] by simp
  also have "... ⟷ f divides⇘poly_ring ?S⇙ g"
    unfolding pdivides_def factor_def by auto
  also have "... ⟷ f pdivides⇘?S⇙ g"
    unfolding pdivides_def by simp
  finally show ?thesis by simp
qed

lemma (in finite_field) find_root:
  assumes "subfield K R"
  assumes "monic_irreducible_poly (R ⦇ carrier := K ⦈) f"
  assumes "order R = card K^degree f"
  obtains x where "eval f x = 𝟬" "x ∈ carrier R"
proof -
  define τ :: "'a list ⇒ 'a list" where "τ = id"
  let ?K = "R ⦇ carrier := K ⦈"
  have "finite K" 
    using assms(1) by (intro finite_subset[OF _ finite_carrier], simp)
  hence fin_K: "finite (carrier (?K))" 
    by simp 
  interpret f: finite_field "?K"
    using assms(1) subfield_iff fin_K finite_fieldI by blast
  have b:"subring K R" 
    using assms(1) subfieldE(1) by blast
  interpret e: ring_hom_ring "(K[X])" "(poly_ring R)" "τ"
    using embed_hom[OF b] by (simp add:τ_def)

  have a: "card K^degree f > 1"
    using assms(3) finite_field_min_order by simp
  have "f ∈ carrier (poly_ring ?K)"
    using f.monic_poly_carr assms(2)
    unfolding monic_irreducible_poly_def by simp
  hence f_carr_2: "f ∈ carrier (K[X])"
    using univ_poly_consistent[OF b] by simp
  have f_carr: "f ∈ carrier (poly_ring R)"
    using e.hom_closed[OF f_carr_2] unfolding τ_def by simp

  have gp_carr: "gauss_poly ?K (order ?K^degree f) ∈ carrier (K[X])"
    using f.gauss_poly_carr univ_poly_consistent[OF b] by simp

  have "gauss_poly ?K (order ?K^degree f) = 
    gauss_poly ?K (card K^degree f)"
    by (simp add:Coset.order_def)
  also have "... = 
    X⇘?K⇙ [^]⇘poly_ring ?K⇙ card K ^ degree f ⊖⇘poly_ring ?K⇙ X⇘?K⇙"
    unfolding gauss_poly_def by simp
  also have "... = X⇘R⇙ [^]⇘K[X]⇙ card K ^ degree f  ⊖⇘K[X]⇙ X⇘R⇙"
    unfolding var_def using univ_poly_consistent[OF b] by simp
  also have "... = τ (X⇘R⇙ [^]⇘K[X]⇙ card K ^ degree f  ⊖⇘K[X]⇙ X⇘R⇙)"
    unfolding τ_def by simp
  also have "... = gauss_poly R (card K^degree f)"
    unfolding gauss_poly_def a_minus_def using var_closed[OF b]
    by (simp add:e.hom_nat_pow, simp add:τ_def)
  finally have gp_consistent: "gauss_poly ?K (order ?K^degree f) = 
    gauss_poly R (card K^degree f)"
    by simp

  have deg_f: "degree f > 0" 
    using f.monic_poly_min_degree[OF assms(2)] by simp

  have "splitted f"
  proof (cases "degree f > 1")
    case True
  
    have "f pdivides⇘?K⇙ gauss_poly ?K (order ?K^degree f)"
      using f.div_gauss_poly_iff[OF deg_f assms(2)] by simp
    hence "f pdivides gauss_poly ?K (order ?K^degree f)"
      using pdivides_consistent[OF assms(1)] f_carr_2 gp_carr by simp
    hence "f pdivides gauss_poly R (card K^degree f)"
      using gp_consistent by simp
    moreover have "splitted (gauss_poly R (card K^degree f))" 
      unfolding assms(3)[symmetric] using gauss_poly_splitted by simp
    moreover have "gauss_poly R (card K^degree f) ≠ []" 
      using gauss_poly_not_zero a by (simp add: univ_poly_zero)
    ultimately show "splitted f"
      using pdivides_imp_splitted f_carr gauss_poly_carr by auto
  next
    case False
    hence "degree f = 1" using deg_f by simp
    thus ?thesis using f_carr degree_one_imp_splitted by auto
  qed
  hence "size (roots f) > 0"
    using deg_f unfolding splitted_def by simp
  then obtain x where x_def: "x ∈ carrier R" "is_root f x"
    using roots_mem_iff_is_root[OF f_carr]
    by (metis f_carr nonempty_has_size not_empty_rootsE)
  have "eval f x = 𝟬"
    using x_def is_root_def by blast
  thus ?thesis using x_def using that by simp
qed

lemma (in finite_field) find_iso_from_zfact:
  defines "p ≡ int (char R)"
  assumes "monic_irreducible_poly (ZFact p) f"
  assumes "order R = char R^degree f"
  shows "∃φ. φ ∈ ring_iso (Rupt⇘(ZFact p)⇙ (carrier (ZFact p)) f) R"
proof -
  have char_pos: "char R > 0"
    using finite_carr_imp_char_ge_0[OF finite_carrier] by simp

  interpret zf: finite_field "ZFact p"
    unfolding p_def using zfact_prime_is_finite_field 
    using characteristic_is_prime[OF char_pos] by simp

  interpret zfp: polynomial_ring "ZFact p" "carrier (ZFact p)"
    unfolding polynomial_ring_def polynomial_ring_axioms_def
    using zf.field_axioms zf.carrier_is_subfield by simp

  let ?f' = "map (char_iso R) f" 
  let ?F = "Rupt⇘(ZFact p)⇙ (carrier (ZFact p)) f"

  have "domain (R⦇carrier := char_subring R⦈)"
    using char_ring_is_subdomain subdomain_is_domain by simp 

  hence "monic_irreducible_poly (R ⦇ carrier := char_subring R ⦈) ?f'" 
    using char_iso p_def zf.domain_axioms
    by (intro monic_irreducible_poly_hom[OF assms(2)]) auto
  moreover have "order R = card (char_subring R)^degree ?f'"
    using assms(3) unfolding char_def by simp
  ultimately obtain x where x_def: "eval ?f' x = 𝟬" "x ∈ carrier R"
    using find_root[OF char_ring_is_subfield[OF char_pos]] by blast
  let ?φ = "(λg. the_elem ((λg'. eval (map (char_iso R) g') x) ` g))"
  interpret r: ring_hom_ring "?F" "R" "?φ"
    using assms(2,3)
    unfolding monic_irreducible_poly_def monic_poly_def p_def
    by (intro eval_on_root_is_iso x_def, auto) 
  have a:"?φ ∈ ring_hom ?F R" 
    using r.homh by auto

  have "field (Rupt⇘ZFact p⇙ (carrier (ZFact p)) f)"
    using assms(2)
    unfolding monic_irreducible_poly_def monic_poly_def
    by (subst zfp.rupture_is_field_iff_pirreducible, simp_all) 
  hence b:"inj_on ?φ (carrier ?F)"
    using non_trivial_field_hom_is_inj[OF a _ field_axioms] by simp

  have "card (?φ ` carrier ?F) = order ?F"
    using card_image[OF b] unfolding Coset.order_def by simp
  also have "... =  card (carrier (ZFact p))^degree f"
    using assms(2) zf.monic_poly_min_degree[OF assms(2)]
    unfolding monic_irreducible_poly_def monic_poly_def
    by (intro zf.rupture_order[OF zf.carrier_is_subfield]) auto
  also have "... = char R ^degree f"
    unfolding p_def by (subst card_zfact_carr[OF char_pos], simp)
  also have "... = card (carrier R)"
    using assms(3) unfolding Coset.order_def by simp  
  finally have "card (?φ ` carrier ?F) = card (carrier R)" by simp
  moreover have "?φ ` carrier ?F ⊆ carrier R"
    by (intro image_subsetI, simp)
  ultimately have "?φ ` carrier ?F = carrier R"
    by (intro card_seteq finite_carrier, auto) 
  hence "bij_betw ?φ (carrier ?F) (carrier R)"
    using b bij_betw_imageI by auto

  thus ?thesis
    unfolding ring_iso_def using a b by auto
qed

theorem uniqueness:
  assumes "finite_field F⇩1"
  assumes "finite_field F⇩2"
  assumes "order F⇩1 = order F⇩2"
  shows "F⇩1 ≃ F⇩2"
proof -
  obtain n where o1: "order F⇩1 = char F⇩1^n" "n > 0"
    using finite_field.finite_field_order[OF assms(1)] by auto
  obtain m where o2: "order F⇩2 = char F⇩2^m" "m > 0"
    using finite_field.finite_field_order[OF assms(2)] by auto

  interpret f1: "finite_field" F⇩1 using assms(1) by simp 
  interpret f2: "finite_field" F⇩2 using assms(2) by simp 

  have char_pos: "char F⇩1 > 0" "char F⇩2 > 0"
    using f1.finite_carrier f1.finite_carr_imp_char_ge_0 
    using f2.finite_carrier f2.finite_carr_imp_char_ge_0 by auto
  hence char_prime: 
    "Factorial_Ring.prime (char F⇩1)" 
    "Factorial_Ring.prime (char F⇩2)"
    using f1.characteristic_is_prime f2.characteristic_is_prime
    by auto

  have "char F⇩1^n = char F⇩2^m" 
    using o1 o2 assms(3) by simp
  hence eq: "n = m" "char F⇩1 = char F⇩2"
    using char_prime char_pos o1(2) o2(2) prime_power_inj' by auto

  obtain p where p_def: "p = char F⇩1" "p = char F⇩2" 
    using eq by simp

  have p_prime: "Factorial_Ring.prime p" 
    unfolding p_def(1)
    using f1.characteristic_is_prime char_pos by simp

  interpret zf: finite_field "ZFact (int p)"
    using zfact_prime_is_finite_field p_prime o1(2) 
    using prime_nat_int_transfer by blast

  interpret zfp: polynomial_ring "ZFact p" "carrier (ZFact p)"
    unfolding polynomial_ring_def polynomial_ring_axioms_def
    using zf.field_axioms zf.carrier_is_subfield by simp

  obtain f where f_def: 
    "monic_irreducible_poly (ZFact (int p)) f" "degree f = n"
    using zf.exist_irred o1(2) by auto

  let ?F⇩0  = "Rupt⇘(ZFact p)⇙ (carrier (ZFact p)) f" 

  obtain φ⇩1 where φ⇩1_def: "φ⇩1 ∈ ring_iso ?F⇩0 F⇩1"
    using f1.find_iso_from_zfact f_def o1
    unfolding p_def by auto

  obtain φ⇩2 where φ⇩2_def: "φ⇩2 ∈ ring_iso ?F⇩0 F⇩2"
    using f2.find_iso_from_zfact f_def o2
    unfolding p_def(2) eq(1) by auto

  have "?F⇩0 ≃ F⇩1" using φ⇩1_def is_ring_iso_def by auto
  moreover have "?F⇩0 ≃ F⇩2" using φ⇩2_def is_ring_iso_def by auto
  moreover have "field ?F⇩0" 
    using f_def(1) zf.monic_poly_carr monic_irreducible_poly_def
    by (subst zfp.rupture_is_field_iff_pirreducible) auto
  hence "ring ?F⇩0" using field.is_ring by auto
  ultimately show ?thesis 
    using ring_iso_trans ring_iso_sym by blast
qed

end