Theory Finite_Fields_Preliminary_Results

section ‹Introduction›

text ‹The following section starts with preliminary results. Section~\ref{sec:ring_char} introduces
the characteristic of rings with the Frobenius endomorphism. Whenever it makes sense,
the definitions and facts do not assume the finiteness of the fields or rings. For example the
characteristic is defined over arbitrary rings (and also fields). 

While formal derivatives do exist for type-class based structures in
\verb|HOL-Computational_Algebra|, as far as I can tell, they do not exist for the structure based
polynomials in \verb|HOL-Algebra|. These are introduced in Section~\ref{sec:pderiv}.

A cornerstone of the proof is the derivation of Gauss' formula for the number of monic irreducible
polynomials over a finite field $R$ in Section~\ref{sec:card_irred}. The proof follows the
derivation by Ireland and Rosen~\<^cite>‹‹\textsection 7› in "ireland1982"› closely, with the caveat that it
does not assume that $R$ is a simple prime field, but that it is just a finite field.
This works by adjusting a proof step with the information that the order of a finite field must be 
of the form $p^n$, where $p$ is the characteristic of the field, derived in Section~\ref{sec:ring_char}.
The final step relies on the M\"obius inversion theorem formalized by
Eberl~\<^cite>‹"Dirichlet_Series-AFP"›.\footnote{Thanks to Katharina Kreuzer for discovering that
formalization.}

With Gauss' formula it is possible to show the existence of the finite fields of order $p^n$ 
where $p$ is a prime and $n > 0$. During the proof the fact that the polynomial $X^n - X$ splits
in a field of order $n$ is also derived, which is necessary for the uniqueness result as well.

The uniqueness proof is inspired by the derivation of the same result in
Lidl and Niederreiter~\<^cite>‹"lidl1986"›, but because of the already derived existence proof for 
irreducible polynomials, it was possible to reduce its complexity.

The classification consists of three theorems:
\begin{itemize}
\item \emph{Existence}: For each prime power $p^n$ there exists a finite field of that size. 
  This is shown at the conclusion of Section~\ref{sec:card_irred}.
\item \emph{Uniqueness}: Any two finite fields of the same size are isomorphic. 
  This is shown at the conclusion of Section~\ref{sec:uniqueness}.
\item \emph{Completeness}: Any finite fields' size must be a prime power. 
  This is shown at the conclusion of Section~\ref{sec:ring_char}.
\end{itemize}
›

section ‹Preliminary Results›

theory Finite_Fields_Preliminary_Results
  imports "HOL-Algebra.Polynomial_Divisibility"
begin

subsection ‹Summation in the discrete topology›

text ‹The following lemmas transfer the corresponding result from the summation over finite sets
to summation over functions which vanish outside of a finite set.›

lemma sum'_subtractf_nat:
  fixes f :: "'a ⇒ nat"
  assumes "finite {i ∈ A. f i ≠ 0}"
  assumes "⋀i. i ∈ A ⟹ g i ≤ f i"
  shows "sum' (λi. f i - g i) A = sum' f A - sum' g A"
    (is "?lhs = ?rhs")
proof -
  have c:"finite {i ∈ A. g i ≠ 0}"
    using assms(2)
    by (intro finite_subset[OF _ assms(1)] subsetI, force) 
  let ?B = "{i ∈ A. f i ≠ 0 ∨ g i ≠ 0}"

  have b:"?B = {i ∈ A. f i ≠ 0} ∪ {i ∈ A. g i ≠ 0}"
    by (auto simp add:set_eq_iff)
  have a:"finite ?B"
    using assms(1) c by (subst b, simp)
  have "?lhs = sum' (λi. f i - g i) ?B"
    by (intro sum.mono_neutral_cong_right', simp_all)
  also have "... = sum (λi. f i - g i) ?B"
    by (intro sum.eq_sum a) 
  also have "... = sum f ?B - sum g ?B"
    using assms(2) by (subst sum_subtractf_nat, auto)
  also have "... = sum' f ?B - sum' g ?B"
    by (intro arg_cong2[where f="(-)"] sum.eq_sum[symmetric] a)
  also have "... = ?rhs"
    by (intro arg_cong2[where f="(-)"] sum.mono_neutral_cong_left')
      simp_all
  finally show ?thesis
    by simp
qed

lemma sum'_nat_eq_0_iff:
  fixes f :: "'a ⇒ nat"
  assumes "finite {i ∈ A. f i ≠ 0}"
  assumes "sum' f A = 0"
  shows "⋀i. i ∈ A ⟹ f i = 0"
proof -
  let ?B = "{i ∈ A. f i ≠ 0}"

  have "sum f ?B = sum' f ?B"
    by (intro sum.eq_sum[symmetric] assms(1))
  also have "... = sum' f A"
    by (intro sum.non_neutral')
  also have "... = 0" using assms(2) by simp
  finally have a:"sum f ?B = 0" by simp
  have "⋀i. i ∈ ?B ⟹ f i = 0"
    using sum_nonneg_0[OF assms(1) _ a] by blast
  thus "⋀i. i ∈ A ⟹ f i = 0"
    by blast
qed

lemma sum'_eq_iff:
  fixes f :: "'a ⇒ nat"
  assumes "finite {i ∈ A. f i ≠ 0}"
  assumes "⋀i. i ∈ A ⟹ f i ≥ g i"
  assumes "sum' f A ≤ sum' g A"
  shows "∀i ∈ A. f i = g i"
proof -
  have "{i ∈ A. g i ≠ 0} ⊆ {i ∈ A. f i ≠ 0}"
    using assms(2) order_less_le_trans 
    by (intro subsetI, auto) 
  hence a:"finite {i ∈ A. g i ≠ 0}"
    by (rule finite_subset, intro assms(1))
  have " {i ∈ A. f i - g i ≠ 0} ⊆ {i ∈ A. f i ≠ 0}" 
    by (intro subsetI, simp_all)
  hence b: "finite {i ∈ A. f i - g i ≠ 0}" 
    by (rule finite_subset, intro assms(1))
  have "sum' (λi. f i - g i) A = sum' f A - sum' g A"
    using assms(1,2) a by (subst sum'_subtractf_nat, auto) 
  also have "... = 0"
    using assms(3) by simp
  finally have "sum' (λi. f i - g i) A = 0" by simp
  hence "⋀i. i ∈ A ⟹ f i - g i = 0"
    using sum'_nat_eq_0_iff[OF b] by simp
  thus ?thesis
    using assms(2) diff_is_0_eq' diffs0_imp_equal by blast
qed

subsection ‹Polynomials›

text ‹The embedding of the constant polynomials into the polynomials is injective:›

lemma (in ring) poly_of_const_inj:
  "inj poly_of_const"
proof -
  have "coeff (poly_of_const x) 0 = x" for x 
    unfolding poly_of_const_def normalize_coeff[symmetric]
    by simp
  thus ?thesis by (metis injI)
qed

lemma (in domain) embed_hom:
  assumes "subring K R"
  shows "ring_hom_ring (K[X]) (poly_ring R) id"
proof (rule ring_hom_ringI)
  show "ring (K[X])"
    using univ_poly_is_ring[OF assms(1)] by simp
  show "ring (poly_ring R)"
    using univ_poly_is_ring[OF carrier_is_subring] by simp
  have "K ⊆ carrier R" 
    using subringE(1)[OF assms(1)] by simp
  thus "⋀x. x ∈ carrier (K [X]) ⟹ id x ∈ carrier (poly_ring R)"
    unfolding univ_poly_carrier[symmetric] polynomial_def by auto
  show "id (x ⊗⇘K [X]⇙ y) = id x ⊗⇘poly_ring R⇙ id y" 
    if "x ∈ carrier (K [X])" "y ∈ carrier (K [X])" for x y
    unfolding univ_poly_mult by simp
  show "id (x ⊕⇘K [X]⇙ y) = id x ⊕⇘poly_ring R⇙ id y"
    if "x ∈ carrier (K [X])" "y ∈ carrier (K [X])" for x y
    unfolding univ_poly_add by simp
  show "id 𝟭⇘K [X]⇙ = 𝟭⇘poly_ring R⇙"
    unfolding univ_poly_one by simp
qed

text ‹The following are versions of the properties of the degrees of polynomials, that abstract
over the definition of the polynomial ring structure. In the theories
@{theory "HOL-Algebra.Polynomials"} and also @{theory "HOL-Algebra.Polynomial_Divisibility"}
these abstract version are usually indicated with the suffix ``shell'', consider for example:
@{thm [source] "domain.pdivides_iff_shell"}.›

lemma (in ring) degree_add_distinct:
  assumes "subring K R" 
  assumes "f ∈ carrier (K[X]) - {𝟬⇘K[X]⇙}"
  assumes "g ∈ carrier (K[X]) - {𝟬⇘K[X]⇙}"
  assumes "degree f ≠ degree g"
  shows "degree (f ⊕⇘K[X]⇙ g) = max (degree f) (degree g)"
  unfolding univ_poly_add using assms(2,3,4) 
  by (subst poly_add_degree_eq[OF assms(1)])
    (auto simp:univ_poly_carrier univ_poly_zero)

lemma (in domain) degree_mult:
  assumes "subring K R" 
  assumes "f ∈ carrier (K[X]) - {𝟬⇘K[X]⇙}"
  assumes "g ∈ carrier (K[X]) - {𝟬⇘K[X]⇙}"
  shows "degree (f ⊗⇘K[X]⇙ g) = degree f + degree g"
  unfolding univ_poly_mult using assms(2,3) 
  by (subst poly_mult_degree_eq[OF assms(1)])
    (auto simp:univ_poly_carrier univ_poly_zero)

lemma (in ring) degree_one:
  "degree (𝟭⇘K[X]⇙) = 0"
  unfolding univ_poly_one by simp

lemma (in domain) pow_non_zero: 
  "x ∈ carrier R ⟹ x ≠ 𝟬 ⟹ x [^] (n :: nat) ≠ 𝟬"
  using integral by (induction n, auto) 

lemma (in domain) degree_pow:
  assumes "subring K R" 
  assumes "f ∈ carrier (K[X]) - {𝟬⇘K[X]⇙}"
  shows "degree (f [^]⇘K[X]⇙ n) = degree f * n"
proof -
  interpret p:domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] by simp

  show ?thesis
  proof (induction n)
    case 0
    then show ?case by (simp add:univ_poly_one)
  next
    case (Suc n)
    have "degree (f [^]⇘K [X]⇙ Suc n) = degree (f [^]⇘K [X]⇙ n ⊗⇘K[X]⇙ f)"
      by simp
    also have "... = degree (f [^]⇘K [X]⇙ n) + degree f"
      using p.pow_non_zero assms(2)
      by (subst degree_mult[OF assms(1)], auto)
    also have "... = degree f * Suc n"
      by (subst Suc, simp)
    finally show ?case by simp
  qed
qed

lemma (in ring) degree_var:
  "degree (X⇘R⇙) = 1"
  unfolding var_def by simp

lemma (in domain) var_carr:
  fixes n :: nat
  assumes "subring K R"
  shows "X⇘R⇙ ∈ carrier (K[X]) - {𝟬⇘K [X]⇙}"
proof -
  have "X⇘R⇙ ∈ carrier (K[X])" 
    using var_closed[OF assms(1)] by simp
  moreover have "X ≠ 𝟬⇘K [X]⇙"
    unfolding var_def univ_poly_zero by simp
  ultimately show ?thesis by simp
qed

lemma (in domain) var_pow_carr:
  fixes n :: nat
  assumes "subring K R"
  shows "X⇘R⇙ [^]⇘K [X]⇙ n ∈ carrier (K[X]) - {𝟬⇘K [X]⇙}"
proof -
  interpret p:domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] by simp

  have "X⇘R⇙ [^]⇘K [X]⇙ n ∈ carrier (K[X])" 
    using var_pow_closed[OF assms(1)] by simp
  moreover have "X ≠ 𝟬⇘K [X]⇙"
    unfolding var_def univ_poly_zero by simp
  hence "X⇘R⇙ [^]⇘K [X]⇙ n ≠ 𝟬⇘K [X]⇙"
    using var_closed(1)[OF assms(1)]
    by (intro p.pow_non_zero, auto)
  ultimately show ?thesis by simp
qed

lemma (in domain) var_pow_degree:
  fixes n :: nat
  assumes "subring K R"
  shows "degree (X⇘R⇙ [^]⇘K [X]⇙ n) = n"
  using var_carr[OF assms(1)] degree_var
  by (subst degree_pow[OF assms(1)], auto)

lemma (in domain) finprod_non_zero:
  assumes "finite A"
  assumes "f ∈ A → carrier R - {𝟬}"
  shows "(⨂i ∈ A. f i) ∈ carrier R - {𝟬}"
  using assms
proof (induction A rule:finite_induct)
  case empty
  then show ?case by simp
next
  case (insert x F)
  have "finprod R f (insert x F) = f x ⊗ finprod R f F"
    using insert by (subst finprod_insert, simp_all add:Pi_def)
  also have "... ∈ carrier R-{𝟬}"
    using integral insert by auto
  finally show ?case by simp
qed

lemma (in domain) degree_prod:
  assumes "finite A"
  assumes "subring K R" 
  assumes "f ∈ A → carrier (K[X]) - {𝟬⇘K[X]⇙}"
  shows "degree (⨂⇘K[X]⇙i ∈ A. f i) = (∑i ∈ A. degree (f i))"
  using assms
proof -
  interpret p:domain "K[X]"
    using univ_poly_is_domain[OF assms(2)] by simp

  show ?thesis
    using assms(1,3)
  proof (induction A rule: finite_induct)
    case empty
    then show ?case by (simp add:univ_poly_one)
  next
    case (insert x F)
    have "degree (finprod (K[X]) f (insert x F)) = 
      degree (f x ⊗⇘K[X]⇙ finprod (K[X]) f F)"
      using insert by (subst p.finprod_insert, auto)
    also have "... = degree (f x) + degree (finprod (K[X]) f F)"
      using insert p.finprod_non_zero[OF insert(1)]
      by (subst degree_mult[OF assms(2)], simp_all) 
    also have "... = degree (f x) + (∑i ∈ F. degree (f i))"
      using insert by (subst insert(3), auto) 
    also have "... = (∑i ∈ insert x F. degree (f i))"
      using insert by simp
    finally show ?case by simp
  qed
qed

lemma (in ring) coeff_add:
  assumes "subring K R"
  assumes "f ∈ carrier (K[X])" "g ∈ carrier (K[X])"
  shows "coeff (f ⊕⇘K[X]⇙ g) i = coeff f i ⊕⇘R⇙ coeff g i"
proof -
  have a:"set f ⊆ carrier R"
    using assms(1,2) univ_poly_carrier 
    using subringE(1)[OF assms(1)] polynomial_incl
    by blast
  have b:"set g ⊆ carrier R" 
    using assms(1,3) univ_poly_carrier
    using subringE(1)[OF assms(1)] polynomial_incl
    by blast
  show ?thesis
    unfolding univ_poly_add poly_add_coeff[OF a b] by simp
qed

text ‹This is a version of geometric sums for commutative rings:›

lemma (in cring) geom:
  fixes q:: nat
  assumes [simp]: "a ∈ carrier R"
  shows "(a ⊖ 𝟭) ⊗ (⨁i∈{..<q}. a [^] i) = (a [^] q ⊖ 𝟭)"
    (is "?lhs = ?rhs")
proof -
  have [simp]: "a [^] i ∈ carrier R" for i :: nat
    by (intro nat_pow_closed assms)
  have [simp]: "⊖ 𝟭 ⊗ x = ⊖ x" if "x ∈ carrier R" for x
    using l_minus l_one one_closed that by presburger

  let ?cterm = "(⨁i∈{1..<q}. a [^] i)"

  have "?lhs = a ⊗ (⨁i∈{..<q}. a [^] i)  ⊖ (⨁i∈{..<q}. a [^] i)"
    unfolding a_minus_def by (subst l_distr, simp_all add:Pi_def)
  also have "... = (⨁i∈{..<q}. a ⊗ a [^] i) ⊖ (⨁i∈{..<q}. a [^] i)"
    by (subst finsum_rdistr, simp_all add:Pi_def)
  also have "... = (⨁i∈{..<q}. a [^] (Suc i)) ⊖ (⨁i∈{..<q}. a [^] i)"
    by (subst nat_pow_Suc, simp_all add:m_comm)
  also have "... = (⨁i∈Suc ` {..<q}. a [^] i) ⊖ (⨁i∈{..<q}. a [^] i)"
    by (subst finsum_reindex, simp_all)
  also have "... = 
    (⨁i∈ insert q {1..<q}. a [^] i) ⊖ 
    (⨁i∈ insert 0 {1..<q}. a [^] i)"
  proof (cases "q > 0")
    case True
    moreover have "Suc ` {..<q} = insert q {Suc 0..<q}" 
      using True lessThan_atLeast0 by fastforce 
    moreover have "{..<q} = insert 0 {Suc 0..<q}"
      using True by (auto simp add:set_eq_iff) 
    ultimately show ?thesis 
      by (intro arg_cong2[where f="λx y. x ⊖ y"] finsum_cong)
        simp_all
  next
    case False
    then show ?thesis by (simp, algebra)
  qed
  also have "... = (a [^] q ⊕ ?cterm) ⊖ (𝟭 ⊕ ?cterm)"
    by simp
  also have "... = a [^] q ⊕ ?cterm ⊕ (⊖ 𝟭 ⊕ ⊖ ?cterm)"
    unfolding a_minus_def by (subst minus_add, simp_all)
  also have "... = a [^] q ⊕ (?cterm ⊕ (⊖ 𝟭 ⊕ ⊖ ?cterm))"
    by (subst a_assoc, simp_all)
  also have "... = a [^] q ⊕ (?cterm ⊕ (⊖ ?cterm ⊕ ⊖ 𝟭))"
    by (subst a_comm[where x="⊖ 𝟭"], simp_all)
  also have "... = a [^] q ⊕ ((?cterm ⊕ (⊖ ?cterm)) ⊕ ⊖ 𝟭)"
    by (subst a_assoc, simp_all)
  also have "... = a [^] q ⊕ (𝟬 ⊕ ⊖ 𝟭)"
    by (subst r_neg, simp_all)
  also have "... = a [^] q ⊖ 𝟭" 
    unfolding a_minus_def by simp
  finally show ?thesis by simp
qed

lemma (in domain) rupture_eq_0_iff:
  assumes "subfield K R" "p ∈ carrier (K[X])" "q ∈ carrier (K[X])"
  shows "rupture_surj K p q = 𝟬⇘Rupt K p⇙ ⟷ p pdivides q"
    (is "?lhs ⟷ ?rhs")
proof -
  interpret h:ring_hom_ring "K[X]" "(Rupt K p)" "(rupture_surj K p)"
    using assms subfieldE by (intro rupture_surj_hom) auto

  have a: "q pmod p ∈ (λq. q pmod p) ` carrier (K [X])" 
    using assms(3) by simp
  have "𝟬⇘K[X]⇙ = 𝟬⇘K[X]⇙ pmod p" 
    using assms(1,2) long_division_zero(2)
    by (simp add:univ_poly_zero)
  hence b: "𝟬⇘K[X]⇙ ∈ (λq. q pmod p) ` carrier (K[X])" 
    by (simp add:image_iff) auto

  have "?lhs ⟷ rupture_surj K p (q pmod p) = 
    rupture_surj K p (𝟬⇘K[X]⇙)" 
    by (subst rupture_surj_composed_with_pmod[OF assms]) simp
  also have "... ⟷ q pmod p = 𝟬⇘K[X]⇙"
    using assms(3)
    by (intro inj_on_eq_iff[OF rupture_surj_inj_on[OF assms(1,2)]] a b)
  also have "... ⟷ ?rhs"
    unfolding univ_poly_zero
    by (intro pmod_zero_iff_pdivides[OF assms(1)] assms(2,3))
  finally show "?thesis" by simp
qed

subsection ‹Ring Isomorphisms›

text ‹The following lemma shows that an isomorphism between domains also induces an isomorphism
between the corresponding polynomial rings.›

lemma lift_iso_to_poly_ring:
  assumes "h ∈ ring_iso R S" "domain R" "domain S"
  shows "map h ∈ ring_iso (poly_ring R) (poly_ring S)"
proof (rule ring_iso_memI)
  interpret dr: domain "R" using assms(2) by blast
  interpret ds: domain "S" using assms(3) by blast
  interpret pdr: domain "poly_ring R"
    using dr.univ_poly_is_domain[OF dr.carrier_is_subring] by simp
  interpret pds: domain "poly_ring S"
    using ds.univ_poly_is_domain[OF ds.carrier_is_subring] by simp
  interpret h: ring_hom_ring "R" "S" h
    using dr.ring_axioms ds.ring_axioms assms(1)
    by (intro ring_hom_ringI2, simp_all add:ring_iso_def)
  let ?R = "poly_ring R"
  let ?S = "poly_ring S"

  have h_img: "h ` (carrier R) = carrier S" 
    using assms(1) unfolding ring_iso_def bij_betw_def by auto
  have h_inj: "inj_on h (carrier R)" 
    using assms(1) unfolding ring_iso_def bij_betw_def by auto
  hence h_non_zero_iff:  "h x ≠ 𝟬⇘S⇙"
    if "x ≠ 𝟬⇘R⇙" "x ∈ carrier R" for x
    using h.hom_zero dr.zero_closed inj_onD that by metis

  have norm_elim: "ds.normalize (map h x) = map h x" 
    if "x ∈ carrier (poly_ring R)" for x 
  proof (cases "x")
    case Nil then show ?thesis by simp
  next
    case (Cons xh xt)
    have "xh ∈ carrier R" "xh ≠ 𝟬⇘R⇙"
      using that unfolding Cons univ_poly_carrier[symmetric] 
      unfolding polynomial_def by auto
    hence "h xh ≠ 𝟬⇘S⇙" using h_non_zero_iff by simp
    then show ?thesis unfolding Cons by simp
  qed

  show t_1: "map h x ∈ carrier ?S" 
    if "x ∈ carrier ?R" for x
    using that hd_in_set h_non_zero_iff hd_map
    unfolding univ_poly_carrier[symmetric] polynomial_def 
    by (cases x, auto)

  show "map h (x ⊗⇘?R⇙ y) = map h x ⊗⇘?S⇙ map h y" 
    if "x ∈ carrier ?R" "y ∈ carrier ?R" for x y
  proof -
    have "map h (x ⊗⇘?R⇙ y) = ds.normalize (map h (x ⊗⇘?R⇙ y))"
      using that by (intro norm_elim[symmetric],simp) 
    also have "... = map h x ⊗⇘?S⇙ map h y"
      using that unfolding univ_poly_mult univ_poly_carrier[symmetric] 
      unfolding polynomial_def
      by (intro h.poly_mult_hom'[of x y] , auto)
    finally show ?thesis by simp
  qed

  show "map h (x ⊕⇘?R⇙ y) = map h x ⊕⇘?S⇙ map h y"
    if "x ∈ carrier ?R" "y ∈ carrier ?R" for x y
  proof -
    have "map h (x ⊕⇘?R⇙ y) = ds.normalize (map h (x ⊕⇘?R⇙ y))"
      using that by (intro norm_elim[symmetric],simp) 
    also have "... = map h x ⊕⇘?S⇙ map h y"
      using that
      unfolding univ_poly_add univ_poly_carrier[symmetric] 
      unfolding polynomial_def
      by (intro h.poly_add_hom'[of x y], auto)
    finally show ?thesis by simp
  qed

  show "map h 𝟭⇘?R⇙ = 𝟭⇘?S⇙" 
    unfolding univ_poly_one by simp

  let ?hinv = "map (the_inv_into (carrier R) h)"

  have "map h ∈ carrier ?R → carrier ?S" 
    using t_1 by simp
  moreover have "?hinv x ∈ carrier ?R" 
    if "x ∈ carrier ?S" for x
  proof (cases "x = []")
    case True
    then show ?thesis 
      by (simp add:univ_poly_carrier[symmetric] polynomial_def)
  next
    case False
    have set_x: "set x ⊆ h ` carrier R" 
      using that h_img unfolding univ_poly_carrier[symmetric]
      unfolding polynomial_def by auto
    have "lead_coeff x ≠ 𝟬⇘S⇙" "lead_coeff x ∈ carrier S"
      using that False unfolding univ_poly_carrier[symmetric]
      unfolding polynomial_def by auto
    hence "the_inv_into (carrier R) h (lead_coeff x) ≠ 
      the_inv_into (carrier R) h 𝟬⇘S⇙" 
      using inj_on_the_inv_into[OF h_inj] inj_onD 
      using ds.zero_closed h_img by metis
    hence "the_inv_into (carrier R) h (lead_coeff x) ≠ 𝟬⇘R⇙" 
      unfolding h.hom_zero[symmetric] 
      unfolding the_inv_into_f_f[OF h_inj dr.zero_closed] by simp
    hence "lead_coeff (?hinv x) ≠ 𝟬⇘R⇙" 
      using False by (simp add:hd_map)
    moreover have "the_inv_into (carrier R) h ` set x ⊆ carrier R" 
      using the_inv_into_into[OF h_inj] set_x
      by (intro image_subsetI) auto
    hence "set (?hinv x) ⊆ carrier R" by simp 
    ultimately show ?thesis
      by (simp add:univ_poly_carrier[symmetric] polynomial_def)
  qed
  moreover have "?hinv (map h x) = x" if "x ∈ carrier ?R" for x 
  proof -
    have set_x: "set x ⊆ carrier R" 
      using that unfolding univ_poly_carrier[symmetric]
      unfolding polynomial_def by auto
    have "?hinv (map h x) = 
      map (λy. the_inv_into (carrier R) h (h y)) x"
      by simp
    also have "... = map id x"
      using set_x by (intro map_cong)
        (auto simp add:the_inv_into_f_f[OF h_inj])
    also have "... = x" by simp
    finally show ?thesis by simp
  qed
  moreover have "map h (?hinv x) = x" 
    if "x ∈ carrier ?S" for x
  proof -
    have set_x: "set x ⊆ h ` carrier R" 
      using that h_img unfolding univ_poly_carrier[symmetric]
      unfolding polynomial_def by auto
    have "map h (?hinv x) = 
      map (λy. h (the_inv_into (carrier R) h y)) x"
      by simp
    also have "... = map id x"
      using set_x by (intro map_cong)
        (auto simp add:f_the_inv_into_f[OF h_inj])
    also have "... = x" by simp
    finally show ?thesis by simp
  qed
  ultimately show "bij_betw (map h) (carrier ?R) (carrier ?S)" 
    by (intro bij_betwI[where g="?hinv"], auto) 
qed

lemma carrier_hom:
  assumes "f ∈ carrier (poly_ring R)"
  assumes "h ∈ ring_iso R S" "domain R" "domain S"
  shows "map h f ∈ carrier (poly_ring S)"
proof -
  note poly_iso = lift_iso_to_poly_ring[OF assms(2,3,4)] 
  show ?thesis
    using ring_iso_memE(1)[OF poly_iso assms(1)] by simp
qed

lemma carrier_hom':
  assumes "f ∈ carrier (poly_ring R)"
  assumes "h ∈ ring_hom R S"
  assumes "domain R" "domain S" 
  assumes "inj_on h (carrier R)"
  shows "map h f ∈ carrier (poly_ring S)"
proof -
  let ?S = "S ⦇ carrier := h ` carrier R ⦈"

  interpret dr: domain "R" using assms(3) by blast
  interpret ds: domain "S" using assms(4) by blast
  interpret h1: ring_hom_ring R S h
    using assms(2) ring_hom_ringI2 dr.ring_axioms 
    using ds.ring_axioms by blast 
  have subr: "subring (h ` carrier R) S" 
    using h1.img_is_subring[OF dr.carrier_is_subring] by blast
  interpret h: ring_hom_ring "((h ` carrier R)[X]⇘S⇙)" "poly_ring S" "id"
    using ds.embed_hom[OF subr] by simp

  let ?S = "S ⦇ carrier := h ` carrier R ⦈"
  have "h ∈ ring_hom R ?S"
    using assms(2) unfolding ring_hom_def by simp
  moreover have "bij_betw h (carrier R) (carrier ?S)"
    using assms(5) bij_betw_def by auto
  ultimately have h_iso: "h ∈ ring_iso R ?S"
    unfolding ring_iso_def by simp

  have dom_S: "domain ?S" 
    using ds.subring_is_domain[OF subr] by simp

  note poly_iso = lift_iso_to_poly_ring[OF h_iso assms(3) dom_S]
  have "map h f ∈ carrier (poly_ring ?S)"
    using ring_iso_memE(1)[OF poly_iso assms(1)] by simp
  also have "carrier (poly_ring ?S) = 
    carrier (univ_poly S (h ` carrier R))"
    using ds.univ_poly_consistent[OF subr] by simp
  also have "... ⊆ carrier (poly_ring S)"
    using h.hom_closed by auto
  finally show ?thesis by simp
qed

text ‹The following lemmas transfer properties like divisibility, irreducibility etc. between
ring isomorphisms.›

lemma divides_hom:
  assumes "h ∈ ring_iso R S" 
  assumes "domain R" "domain S" 
  assumes "x ∈ carrier R" "y ∈ carrier R"
  shows "x divides⇘R⇙ y ⟷ (h x) divides⇘S⇙ (h y)"  (is "?lhs ⟷ ?rhs")
proof -
  interpret dr: domain "R" using assms(2) by blast
  interpret ds: domain "S" using assms(3) by blast
  interpret pdr: domain "poly_ring R"
    using dr.univ_poly_is_domain[OF dr.carrier_is_subring] by simp
  interpret pds: domain "poly_ring S"
    using ds.univ_poly_is_domain[OF ds.carrier_is_subring] by simp
  interpret h: ring_hom_ring "R" "S" h
    using dr.ring_axioms ds.ring_axioms assms(1)
    by (intro ring_hom_ringI2, simp_all add:ring_iso_def)

  have h_inj_on: "inj_on h (carrier R)" 
    using assms(1) unfolding ring_iso_def bij_betw_def by auto
  have h_img: "h ` (carrier R) = carrier S" 
    using assms(1) unfolding ring_iso_def bij_betw_def by auto

  have "?lhs ⟷ (∃c ∈ carrier R. y = x ⊗⇘R⇙ c)"
    unfolding factor_def by simp
  also have "... ⟷ (∃c ∈ carrier R. h y = h x ⊗⇘S⇙ h c)"
    using assms(4,5) inj_onD[OF h_inj_on]
    by (intro bex_cong, auto simp flip:h.hom_mult) 
  also have "... ⟷ (∃c ∈ carrier S. h y = h x  ⊗⇘S⇙ c)"
    unfolding h_img[symmetric] by simp
  also have "... ⟷ ?rhs" 
    unfolding factor_def by simp
  finally show ?thesis by simp
qed

lemma properfactor_hom:
  assumes "h ∈ ring_iso R S" 
  assumes "domain R" "domain S" 
  assumes "x ∈ carrier R" "b ∈ carrier R"
  shows "properfactor R b x ⟷ properfactor S (h b) (h x)" 
  using divides_hom[OF assms(1,2,3)] assms(4,5)
  unfolding properfactor_def by simp

lemma Units_hom:
  assumes "h ∈ ring_iso R S" 
  assumes "domain R" "domain S" 
  assumes "x ∈ carrier R"
  shows "x ∈ Units R ⟷  h x ∈ Units S"
proof -

  interpret dr: domain "R" using assms(2) by blast
  interpret ds: domain "S" using assms(3) by blast
  interpret pdr: domain "poly_ring R"
    using dr.univ_poly_is_domain[OF dr.carrier_is_subring] by simp
  interpret pds: domain "poly_ring S"
    using ds.univ_poly_is_domain[OF ds.carrier_is_subring] by simp
  interpret h: ring_hom_ring "R" "S" h
    using dr.ring_axioms ds.ring_axioms assms(1)
    by (intro ring_hom_ringI2, simp_all add:ring_iso_def)

  have h_img: "h ` (carrier R) = carrier S" 
    using assms(1) unfolding ring_iso_def bij_betw_def by auto

  have h_inj_on: "inj_on h (carrier R)" 
    using assms(1) unfolding ring_iso_def bij_betw_def by auto

  hence h_one_iff: "h x = 𝟭⇘S⇙ ⟷ x = 𝟭⇘R⇙" if "x ∈ carrier R" for x
    using h.hom_one that by (metis dr.one_closed inj_onD)

  have "x ∈ Units R ⟷ 
    (∃y∈carrier R. x ⊗⇘R⇙ y = 𝟭⇘R⇙ ∧ y ⊗⇘R⇙ x = 𝟭⇘R⇙)"
    using assms unfolding Units_def by auto
  also have "... ⟷ 
    (∃y∈carrier R. h x ⊗⇘S⇙ h y = h 𝟭⇘R⇙ ∧ h y ⊗⇘S⇙ h x = h 𝟭⇘R⇙)"
    using h_one_iff assms by (intro bex_cong, simp_all flip:h.hom_mult)
  also have "... ⟷ 
    (∃y∈carrier S. h x ⊗⇘S⇙ y = h 𝟭⇘R⇙ ∧ y ⊗⇘S⇙ h x = 𝟭⇘S⇙)"
    unfolding h_img[symmetric] by simp
  also have "... ⟷ h x ∈ Units S"
    using assms h.hom_closed unfolding Units_def by auto
  finally show ?thesis by simp
qed

lemma irreducible_hom:
  assumes "h ∈ ring_iso R S" 
  assumes "domain R" "domain S" 
  assumes "x ∈ carrier R"
  shows "irreducible R x = irreducible S (h x)"
proof -
  have h_img: "h ` (carrier R) = carrier S" 
    using assms(1) unfolding ring_iso_def bij_betw_def by auto

  have "irreducible R x ⟷ (x ∉ Units R ∧ 
    (∀b∈carrier R. properfactor R b x ⟶ b ∈ Units R))"
    unfolding Divisibility.irreducible_def by simp
  also have "... ⟷ (x ∉ Units R ∧ 
    (∀b∈carrier R. properfactor S (h b) (h x) ⟶ b ∈ Units R))"
    using properfactor_hom[OF assms(1,2,3)] assms(4) by simp
  also have "... ⟷ (h x ∉ Units S ∧ 
    (∀b∈carrier R. properfactor S (h b) (h x) ⟶ h b ∈ Units S))"
    using assms(4) Units_hom[OF assms(1,2,3)] by simp
  also have "...⟷ (h x ∉ Units S ∧ 
    (∀b∈h ` carrier R. properfactor S b (h x) ⟶ b ∈ Units S))"
    by simp
  also have "... ⟷ irreducible S (h x)"
    unfolding h_img Divisibility.irreducible_def by simp
  finally show ?thesis by simp
qed

lemma pirreducible_hom:
  assumes "h ∈ ring_iso R S" 
  assumes "domain R" "domain S"
  assumes "f ∈ carrier (poly_ring R)"
  shows "pirreducible⇘R⇙ (carrier R) f = 
    pirreducible⇘S⇙ (carrier S) (map h f)" 
    (is "?lhs = ?rhs")
proof -
  note lift_iso = lift_iso_to_poly_ring[OF assms(1,2,3)]
  interpret dr: domain "R" using assms(2) by blast
  interpret ds: domain "S" using assms(3) by blast
  interpret pdr: domain "poly_ring R"
    using dr.univ_poly_is_domain[OF dr.carrier_is_subring] by simp
  interpret pds: domain "poly_ring S"
    using ds.univ_poly_is_domain[OF ds.carrier_is_subring] by simp

  have mh_inj_on: "inj_on (map h) (carrier (poly_ring R))" 
    using lift_iso unfolding ring_iso_def bij_betw_def by auto
  moreover have "map h 𝟬⇘poly_ring R⇙ = 𝟬⇘poly_ring S⇙"
    by (simp add:univ_poly_zero)
  ultimately have mh_zero_iff: 
    "map h f = 𝟬⇘poly_ring S⇙ ⟷ f = 𝟬⇘poly_ring R⇙"
    using assms(4) by (metis pdr.zero_closed inj_onD)

  have "?lhs ⟷ (f ≠ 𝟬⇘poly_ring R⇙ ∧ irreducible (poly_ring R) f)"
    unfolding ring_irreducible_def by simp
  also have "... ⟷ 
    (f ≠ 𝟬⇘poly_ring R⇙ ∧ irreducible (poly_ring S) (map h f))"
    using irreducible_hom[OF lift_iso] pdr.domain_axioms
    using assms(4) pds.domain_axioms by simp
  also have "... ⟷ 
    (map h f ≠ 𝟬⇘poly_ring S⇙ ∧ irreducible (poly_ring S) (map h f))"
    using mh_zero_iff by simp
  also have "... ⟷ ?rhs"
    unfolding ring_irreducible_def by simp
  finally show ?thesis by simp
qed


lemma ring_hom_cong:
  assumes "⋀x. x ∈ carrier R ⟹ f' x = f x" 
  assumes "ring R"
  assumes "f ∈ ring_hom R S"
  shows "f' ∈ ring_hom R S"
proof -
  interpret ring "R" using assms(2) by simp
  show ?thesis 
    using assms(1) ring_hom_memE[OF assms(3)]
    by (intro ring_hom_memI, auto) 
qed

text ‹The natural homomorphism between factor rings, where one ideal is a subset of the other.›

lemma (in ring) quot_quot_hom: 
  assumes "ideal I R"
  assumes "ideal J R"
  assumes "I ⊆ J"
  shows "(λx. (J <+>⇘R⇙ x)) ∈ ring_hom (R Quot I) (R Quot J)"  
proof (rule ring_hom_memI)
  interpret ji: ideal J R
    using assms(2) by simp
  interpret ii: ideal I R
    using assms(1) by simp

  have a:"J <+>⇘R⇙ I = J"
    using assms(3) unfolding set_add_def set_mult_def by auto

  show "J <+>⇘R⇙ x ∈ carrier (R Quot J)"
    if "x ∈ carrier (R Quot I)" for x
  proof -
    have " ∃y∈carrier R. x = I +> y" 
      using that unfolding FactRing_def A_RCOSETS_def' by simp
    then obtain y where y_def: "y ∈ carrier R" "x = I +> y"
      by auto
    have "J <+>⇘R⇙ (I +> y) = (J <+>⇘R⇙ I) +> y"
      using y_def(1) by (subst a_setmult_rcos_assoc) auto
    also have "... = J +> y" using a by simp
    finally have "J <+>⇘R⇙ (I +> y) = J +> y" by simp
    thus ?thesis
      using y_def unfolding FactRing_def A_RCOSETS_def' by auto 
  qed

  show "J <+>⇘R⇙ x ⊗⇘R Quot I⇙ y = 
    (J <+>⇘R⇙ x) ⊗⇘R Quot J⇙ (J <+>⇘R⇙ y)"
    if "x ∈ carrier (R Quot I)" "y ∈ carrier (R Quot I)" 
    for x y
  proof -
    have "∃x1∈carrier R. x = I +> x1" "∃y1∈carrier R. y = I +> y1" 
      using that unfolding FactRing_def A_RCOSETS_def' by auto
    then obtain x1 y1 
      where x1_def: "x1 ∈ carrier R" "x = I +> x1"
        and y1_def: "y1 ∈ carrier R" "y = I +> y1"
      by auto
    have "J <+>⇘R⇙ x ⊗⇘R Quot I⇙ y = J <+>⇘R⇙ (I +> x1 ⊗ y1)"
      using x1_def y1_def
      by (simp add: FactRing_def ii.rcoset_mult_add)
    also have "... = (J <+>⇘R⇙ I) +> x1 ⊗ y1"
      using x1_def(1) y1_def(1)
      by (subst a_setmult_rcos_assoc) auto
    also have "... = J +> x1 ⊗ y1"
      using a by simp
    also have "... = [mod J:] (J +> x1) ⨂ (J +> y1)" 
      using x1_def(1) y1_def(1) by (subst ji.rcoset_mult_add, auto)
    also have "... = 
      [mod J:] ((J <+>⇘R⇙ I) +> x1) ⨂ ((J <+>⇘R⇙ I) +> y1)" 
      using a by simp
    also have "... = 
      [mod J:] (J <+>⇘R⇙ (I +> x1)) ⨂ (J <+>⇘R⇙ (I +> y1))"
      using x1_def(1) y1_def(1)
      by (subst (1 2) a_setmult_rcos_assoc) auto
    also have "... = (J <+>⇘R⇙ x) ⊗⇘R Quot J⇙ (J <+>⇘R⇙ y)"
      using x1_def y1_def by (simp add: FactRing_def)
    finally show ?thesis by simp
  qed

  show "J <+>⇘R⇙ x ⊕⇘R Quot I⇙ y = 
    (J <+>⇘R⇙ x) ⊕⇘R Quot J⇙ (J <+>⇘R⇙ y)"
    if "x ∈ carrier (R Quot I)" "y ∈ carrier (R Quot I)"
    for x y
  proof -
    have "∃x1∈carrier R. x = I +> x1" "∃y1∈carrier R. y = I +> y1" 
      using that unfolding FactRing_def A_RCOSETS_def' by auto
    then obtain x1 y1 
      where x1_def: "x1 ∈ carrier R" "x = I +> x1"
        and y1_def: "y1 ∈ carrier R" "y = I +> y1"
      by auto
    have "J <+>⇘R⇙ x ⊕⇘R Quot I⇙ y = 
      J <+>⇘R⇙ ((I +> x1) <+>⇘R⇙ (I +> y1))"
      using x1_def y1_def by (simp add:FactRing_def)
    also have "... = J <+>⇘R⇙ (I +> (x1 ⊕ y1))"
      using x1_def y1_def ii.a_rcos_sum by simp
    also have "... = (J <+>⇘R⇙ I) +> (x1 ⊕ y1)"
      using x1_def y1_def by (subst a_setmult_rcos_assoc) auto
    also have "... = J +> (x1 ⊕ y1)"
      using a by simp
    also have "... = 
      ((J <+>⇘R⇙ I) +> x1) <+>⇘R⇙ ((J <+>⇘R⇙ I) +> y1)"
      using x1_def y1_def ji.a_rcos_sum a by simp
    also have "... = 
      J <+>⇘R⇙ (I +> x1) <+>⇘R⇙ (J <+>⇘R⇙ (I +> y1))" 
      using x1_def y1_def by (subst (1 2) a_setmult_rcos_assoc) auto
    also have "... = (J <+>⇘R⇙ x) ⊕⇘R Quot J⇙ (J <+>⇘R⇙ y)"
      using x1_def y1_def by (simp add:FactRing_def)
    finally show ?thesis by simp
  qed

  have "J <+>⇘R⇙ 𝟭⇘R Quot I⇙ = J <+>⇘R⇙ (I +> 𝟭)"
    unfolding FactRing_def by simp
  also have "... = (J <+>⇘R⇙ I) +> 𝟭" 
    by (subst a_setmult_rcos_assoc) auto
  also have "... = J +> 𝟭" using a by simp
  also have "... = 𝟭⇘R Quot J⇙"
    unfolding FactRing_def by simp
  finally show "J <+>⇘R⇙ 𝟭⇘R Quot I⇙ = 𝟭⇘R Quot J⇙" 
    by simp
qed

lemma (in ring) quot_carr:
  assumes "ideal I R"
  assumes "y ∈ carrier (R Quot I)"
  shows "y ⊆ carrier R"
proof -
  interpret ideal I R using assms(1) by simp
  have "y ∈ a_rcosets I"
    using assms(2) unfolding FactRing_def by simp
  then obtain v where y_def: "y = I +> v" "v ∈ carrier R"
    unfolding A_RCOSETS_def' by auto
  have "I +> v ⊆ carrier R" 
    using y_def(2) a_r_coset_subset_G a_subset by presburger
  thus "y ⊆ carrier R" unfolding y_def by simp
qed

lemma (in ring) set_add_zero:
  assumes "A ⊆ carrier R"
  shows "{𝟬} <+>⇘R⇙ A = A"
proof -
  have "{𝟬} <+>⇘R⇙ A = (⋃x∈A. {𝟬 ⊕ x})"
    using assms unfolding set_add_def set_mult_def by simp
  also have "... = (⋃x∈A. {x})"
    using assms by (intro arg_cong[where f="Union"] image_cong, auto)
  also have "... = A" by simp
  finally show ?thesis by simp
qed

text ‹Adapted from the proof of @{thm [source] domain.polynomial_rupture}›

lemma (in domain) rupture_surj_as_eval:
  assumes "subring K R" 
  assumes "p ∈ carrier (K[X])" "q ∈ carrier (K[X])"
  shows "rupture_surj K p q = 
    ring.eval (Rupt K p) (map ((rupture_surj K p) ∘ poly_of_const) q) 
    (rupture_surj K p X)"
proof -
  let ?surj = "rupture_surj K p"

  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] .
  interpret h: ring_hom_ring "K[X]" "Rupt K p" ?surj
    using rupture_surj_hom(2)[OF assms(1,2)] .

  have "(h.S.eval) (map (?surj ∘ poly_of_const) q) (?surj X) = 
    ?surj ((UP.eval) (map poly_of_const q) X)"
    using h.eval_hom[OF UP.carrier_is_subring var_closed(1)[OF assms(1)]
          map_norm_in_poly_ring_carrier[OF assms(1,3)]] by simp
  also have " ... = ?surj q"
    unfolding sym[OF eval_rewrite[OF assms(1,3)]] ..
  finally show ?thesis by simp
qed

subsection ‹Divisibility›

lemma  (in field) f_comm_group_1:
  assumes "x ∈ carrier R" "y ∈ carrier R"
  assumes "x ≠ 𝟬" "y ≠ 𝟬"
  assumes "x ⊗ y = 𝟬"
  shows "False" 
  using integral assms by auto

lemma (in field) f_comm_group_2:
  assumes "x ∈ carrier R"
  assumes "x ≠ 𝟬"
  shows " ∃y∈carrier R - {𝟬}. y ⊗ x = 𝟭"
proof -
  have x_unit: "x ∈ Units R" using field_Units assms by simp
  thus ?thesis unfolding Units_def by auto
qed

sublocale field < mult_of: comm_group "mult_of R"
  rewrites "mult (mult_of R) = mult R"
       and "one  (mult_of R) = one R"
  using f_comm_group_1 f_comm_group_2
  by (auto intro!:comm_groupI m_assoc m_comm)

lemma (in domain) div_neg:
  assumes "a ∈ carrier R" "b ∈ carrier R"
  assumes "a divides b"
  shows "a divides (⊖ b)"
proof -
  obtain r1 where r1_def: "r1 ∈ carrier R" "a ⊗ r1 = b"
    using assms by (auto simp:factor_def) 

  have "a ⊗ (⊖ r1) = ⊖ (a ⊗ r1)"
    using assms(1) r1_def(1) by algebra
  also have "... = ⊖ b"
    using r1_def(2) by simp
  finally have "⊖b = a ⊗ (⊖ r1)" by simp
  moreover have "⊖r1 ∈ carrier R"
    using r1_def(1) by simp
  ultimately show ?thesis
    by (auto simp:factor_def) 
qed

lemma (in domain) div_sum:
  assumes "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R"
  assumes "a divides b"
  assumes "a divides c"
  shows "a divides (b ⊕ c)"
proof -
  obtain r1 where r1_def: "r1 ∈ carrier R" "a ⊗ r1 = b"
    using assms by (auto simp:factor_def) 

  obtain r2 where r2_def: "r2 ∈ carrier R" "a ⊗ r2 = c"
    using assms by (auto simp:factor_def) 

  have "a ⊗ (r1 ⊕ r2) = (a ⊗ r1) ⊕ (a ⊗ r2)"
    using assms(1) r1_def(1) r2_def(1) by algebra
  also have "... = b ⊕ c"
    using r1_def(2) r2_def(2) by simp
  finally have "b ⊕ c = a ⊗ (r1 ⊕ r2)" by simp
  moreover have "r1 ⊕ r2 ∈ carrier R"
    using r1_def(1) r2_def(1) by simp
  ultimately show ?thesis
    by (auto simp:factor_def) 
qed

lemma (in domain) div_sum_iff:
  assumes "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R"
  assumes "a divides b"
  shows "a divides (b ⊕ c) ⟷ a divides c"
proof 
  assume "a divides (b ⊕ c)"
  moreover have "a divides (⊖ b)"
    using div_neg assms(1,2,4) by simp
  ultimately have "a divides ((b ⊕ c) ⊕ (⊖ b))"
    using div_sum assms by simp
  also have "... = c" using assms(1,2,3) by algebra
  finally show "a divides c" by simp
next
  assume "a divides c"
  thus "a divides (b ⊕ c)"
    using assms by (intro div_sum) auto
qed

end