Theory Indexed_Polynomials

(*  Title:      HOL/Algebra/Indexed_Polynomials.thy
    Author:     Paulo Emílio de Vilhena
*)

theory Indexed_Polynomials
  imports Weak_Morphisms "HOL-Library.Multiset" Polynomial_Divisibility
    
begin

section ‹Indexed Polynomials›

text ‹In this theory, we build a basic framework to the study of polynomials on letters
      indexed by a set. The main interest is to then apply these concepts to the construction
      of the algebraic closure of a field. ›


subsection ‹Definitions›

text ‹We formalize indexed monomials as multisets with its support a subset of the index set.
      On top of those, we build indexed polynomials which are simply functions mapping a monomial
      to its coefficient. ›

definition (in ring) indexed_const :: "'a ⇒ ('c multiset ⇒ 'a)" 
  where "indexed_const k = (λm. if m = {#} then k else 𝟬)"

definition (in ring) indexed_pmult :: "('c multiset ⇒ 'a) ⇒ 'c ⇒ ('c multiset ⇒ 'a)" (infixl ‹⨂› 65)
  where "indexed_pmult P i = (λm. if i ∈# m then P (m - {# i #}) else 𝟬)"

definition (in ring) indexed_padd :: "_ ⇒ _ ⇒ ('c multiset ⇒ 'a)" (infixl ‹⨁› 65)
  where "indexed_padd P Q = (λm. (P m) ⊕ (Q m))"

definition (in ring) indexed_var :: "'c ⇒ ('c multiset ⇒ 'a)" (‹𝒳ı›)
  where "indexed_var i = (indexed_const 𝟭) ⨂ i"

definition (in ring) index_free :: "('c multiset ⇒ 'a) ⇒ 'c ⇒ bool"
  where "index_free P i ⟷ (∀m. i ∈# m ⟶ P m = 𝟬)"

definition (in ring) carrier_coeff :: "('c multiset ⇒ 'a) ⇒ bool"
  where "carrier_coeff P ⟷ (∀m. P m ∈ carrier R)"

inductive_set (in ring) indexed_pset :: "'c set ⇒ 'a set ⇒ ('c multiset ⇒ 'a) set"
  (‹(‹open_block notation=‹postfix 𝒳››_ [𝒳ı])› 80)
  for I and K where
    indexed_const:  "k ∈ K ⟹ indexed_const k ∈ (K[𝒳⇘I⇙])"
  | indexed_padd:  "⟦ P ∈ (K[𝒳⇘I⇙]); Q ∈ (K[𝒳⇘I⇙]) ⟧ ⟹ P ⨁ Q ∈ (K[𝒳⇘I⇙])"
  | indexed_pmult: "⟦ P ∈ (K[𝒳⇘I⇙]); i ∈ I ⟧ ⟹ P ⨂ i ∈ (K[𝒳⇘I⇙])"

fun (in ring) indexed_eval_aux :: "('c multiset ⇒ 'a) list ⇒ 'c ⇒ ('c multiset ⇒ 'a)"
  where "indexed_eval_aux Ps i = foldr (λP Q. (Q ⨂ i) ⨁ P) Ps (indexed_const 𝟬)"

fun (in ring) indexed_eval :: "('c multiset ⇒ 'a) list ⇒ 'c ⇒ ('c multiset ⇒ 'a)"
  where "indexed_eval Ps i = indexed_eval_aux (rev Ps) i"


subsection ‹Basic Properties›

lemma (in ring) carrier_coeffE:
  assumes "carrier_coeff P" shows "P m ∈ carrier R"
  using assms unfolding carrier_coeff_def by simp

lemma (in ring) indexed_zero_def: "indexed_const 𝟬 = (λ_. 𝟬)"
  unfolding indexed_const_def by simp

lemma (in ring) indexed_const_index_free: "index_free (indexed_const k) i"
  unfolding index_free_def indexed_const_def by auto

lemma (in domain) indexed_var_not_index_free: "¬ index_free 𝒳⇘i⇙ i"
proof -
  have "𝒳⇘i⇙ {# i #} = 𝟭"
    unfolding indexed_var_def indexed_pmult_def indexed_const_def by simp
  thus ?thesis
    using one_not_zero unfolding index_free_def by fastforce 
qed

lemma (in ring) indexed_pmult_zero [simp]:
  shows "indexed_pmult (indexed_const 𝟬) i = indexed_const 𝟬"
  unfolding indexed_zero_def indexed_pmult_def by auto

lemma (in ring) indexed_padd_zero:
  assumes "carrier_coeff P" shows "P ⨁ (indexed_const 𝟬) = P" and "(indexed_const 𝟬) ⨁ P = P"
  using assms unfolding carrier_coeff_def indexed_zero_def indexed_padd_def by auto

lemma (in ring) indexed_padd_const:
  shows "(indexed_const k1) ⨁ (indexed_const k2) = indexed_const (k1 ⊕ k2)"
  unfolding indexed_padd_def indexed_const_def by auto

lemma (in ring) indexed_const_in_carrier:
  assumes "K ⊆ carrier R" and "k ∈ K" shows "⋀m. (indexed_const k) m ∈ carrier R"
  using assms unfolding indexed_const_def by auto

lemma (in ring) indexed_padd_in_carrier:
  assumes "carrier_coeff P" and "carrier_coeff Q" shows "carrier_coeff (indexed_padd P Q)"
  using assms unfolding carrier_coeff_def indexed_padd_def by simp

lemma (in ring) indexed_pmult_in_carrier:
  assumes "carrier_coeff P" shows "carrier_coeff (P ⨂ i)"
  using assms unfolding carrier_coeff_def indexed_pmult_def by simp

lemma (in ring) indexed_eval_aux_in_carrier:
  assumes "list_all carrier_coeff Ps" shows "carrier_coeff (indexed_eval_aux Ps i)"
  using assms unfolding carrier_coeff_def
  by (induct Ps) (auto simp add: indexed_zero_def indexed_padd_def indexed_pmult_def)

lemma (in ring) indexed_eval_in_carrier:
  assumes "list_all carrier_coeff Ps" shows "carrier_coeff (indexed_eval Ps i)"
  using assms indexed_eval_aux_in_carrier[of "rev Ps"] by auto

lemma (in ring) indexed_pset_in_carrier:
  assumes "K ⊆ carrier R" and "P ∈ (K[𝒳⇘I⇙])" shows "carrier_coeff P"
  using assms(2,1) indexed_const_in_carrier unfolding carrier_coeff_def
  by (induction) (auto simp add: indexed_zero_def indexed_padd_def indexed_pmult_def)


subsection ‹Indexed Eval›

lemma (in ring) exists_indexed_eval_aux_monomial:
  assumes "carrier_coeff P" and "list_all carrier_coeff Qs"
    and "count n i = k" and "P n ≠ 𝟬" and "list_all (λQ. index_free Q i) Qs"
  obtains m where "count m i = length Qs + k" and "(indexed_eval_aux (Qs @ [ P ]) i) m ≠ 𝟬"
proof -
  from assms(2,5) have "∃m. count m i = length Qs + k ∧ (indexed_eval_aux (Qs @ [ P ]) i) m ≠ 𝟬"
  proof (induct Qs)
    case Nil thus ?case
      using indexed_padd_zero(2)[OF assms(1)] assms(3-4) by auto
  next
    case (Cons Q Qs)
    then obtain m where m: "count m i = length Qs + k" "(indexed_eval_aux (Qs @ [ P ]) i) m ≠ 𝟬"
      by auto
    define m' where "m' = m + {# i #}"
    hence "Q m' = 𝟬"
      using Cons(3) unfolding index_free_def by simp
    moreover have "(indexed_eval_aux (Qs @ [ P ]) i) m ∈ carrier R"
      using indexed_eval_aux_in_carrier[of "Qs @ [ P ]" i] Cons(2) assms(1) carrier_coeffE by auto
    hence "((indexed_eval_aux (Qs @ [ P ]) i) ⨂ i) m' ∈ carrier R - { 𝟬 }"
      using m unfolding indexed_pmult_def m'_def by simp
    ultimately have "(indexed_eval_aux (Q # (Qs @ [ P ])) i) m' ≠ 𝟬"
      by (auto simp add: indexed_padd_def)
    moreover from ‹count m i = length Qs + k› have "count m' i = length (Q # Qs) + k"
      unfolding m'_def by simp
    ultimately show ?case
      by auto
  qed
  thus thesis
    using that by blast
qed

lemma (in ring) indexed_eval_aux_monomial_degree_le:
  assumes "list_all carrier_coeff Ps" and "list_all (λP. index_free P i) Ps"
    and "(indexed_eval_aux Ps i) m ≠ 𝟬" shows "count m i ≤ length Ps - 1"
  using assms(1-3)
proof (induct Ps arbitrary: m, simp add: indexed_zero_def)
  case (Cons P Ps) show ?case
  proof (cases "count m i = 0", simp)
    assume "count m i ≠ 0"
    hence "P m = 𝟬"
      using Cons(3) unfolding index_free_def by simp
    moreover have "(indexed_eval_aux Ps i) m ∈ carrier R"
      using carrier_coeffE[OF indexed_eval_aux_in_carrier[of Ps i]] Cons(2) by simp 
    ultimately have "((indexed_eval_aux Ps i) ⨂ i) m ≠ 𝟬"
      using Cons(4) by (auto simp add: indexed_padd_def)
    with ‹count m i ≠ 0› have "(indexed_eval_aux Ps i) (m - {# i #}) ≠ 𝟬"
      unfolding indexed_pmult_def by (auto simp del: indexed_eval_aux.simps)
    hence "count m i - 1 ≤ length Ps - 1"
      using Cons(1)[of "m - {# i #}"] Cons(2-3) by auto
    moreover from ‹(indexed_eval_aux Ps i) (m - {# i #}) ≠ 𝟬› have "length Ps > 0"
      by (auto simp add: indexed_zero_def)
    moreover from ‹count m i ≠ 0› have "count m i > 0"
      by simp
    ultimately show ?thesis
      by (simp add: Suc_leI le_diff_iff)
  qed
qed

lemma (in ring) indexed_eval_aux_is_inj:
  assumes "list_all carrier_coeff Ps" and "list_all (λP. index_free P i) Ps"
      and "list_all carrier_coeff Qs" and "list_all (λQ. index_free Q i) Qs"
    and "indexed_eval_aux Ps i = indexed_eval_aux Qs i" and "length Ps = length Qs"
  shows "Ps = Qs"
  using assms
proof (induct Ps arbitrary: Qs, simp)
  case (Cons P Ps)
  from ‹length (P # Ps) = length Qs› obtain Q' Qs' where Qs: "Qs = Q' # Qs'" and "length Ps = length Qs'"
    by (metis Suc_length_conv)

  have in_carrier:
    "((indexed_eval_aux Ps  i) ⨂ i) m ∈ carrier R" "P  m ∈ carrier R"
    "((indexed_eval_aux Qs' i) ⨂ i) m ∈ carrier R" "Q' m ∈ carrier R" for m
    using indexed_eval_aux_in_carrier[of Ps  i]
          indexed_eval_aux_in_carrier[of Qs' i] Cons(2,4) carrier_coeffE
    unfolding Qs indexed_pmult_def by auto

  have "(indexed_eval_aux (P # Ps) i) m = (indexed_eval_aux (Q' # Qs') i) m" for m
    using Cons(6) unfolding Qs by simp
  hence eq: "((indexed_eval_aux Ps i) ⨂ i) m ⊕ P m = ((indexed_eval_aux Qs' i) ⨂ i) m ⊕ Q' m" for m
    by (simp add: indexed_padd_def)

  have "P m = Q' m" if "i ∈# m" for m
    using that Cons(3,5) unfolding index_free_def Qs by auto
  moreover have "P m = Q' m" if "i ∉# m" for m
    using in_carrier(2,4) eq[of m] that by (auto simp add: indexed_pmult_def)
  ultimately have "P = Q'"
    by auto

  hence "(indexed_eval_aux Ps i) m = (indexed_eval_aux Qs' i) m" for m
    using eq[of "m + {# i #}"] in_carrier[of "m + {# i #}"] unfolding indexed_pmult_def by auto
  with ‹length Ps = length Qs'› have "Ps = Qs'"
    using Cons(1)[of Qs'] Cons(2-5) unfolding Qs by auto
  with ‹P = Q'› show ?case
    unfolding Qs by simp
qed

lemma (in ring) indexed_eval_aux_is_inj':
  assumes "list_all carrier_coeff Ps" and "list_all (λP. index_free P i) Ps"
      and "list_all carrier_coeff Qs" and "list_all (λQ. index_free Q i) Qs"
      and "carrier_coeff P" and "index_free P i" "P ≠ indexed_const 𝟬"
      and "carrier_coeff Q" and "index_free Q i" "Q ≠ indexed_const 𝟬"
    and "indexed_eval_aux (Ps @ [ P ]) i = indexed_eval_aux (Qs @ [ Q ]) i"
  shows "Ps = Qs" and "P = Q"
proof -
  obtain m n where "P m ≠ 𝟬" and "Q n ≠ 𝟬"
    using assms(7,10) unfolding indexed_zero_def by blast
  hence "count m i = 0" and "count n i = 0"
    using assms(6,9) unfolding index_free_def by (meson count_inI)+ 
  with ‹P m ≠ 𝟬› and ‹Q n ≠ 𝟬› obtain m' n'
    where m': "count m' i = length Ps" "(indexed_eval_aux (Ps @ [ P ]) i) m' ≠ 𝟬"
      and n': "count n' i = length Qs" "(indexed_eval_aux (Qs @ [ Q ]) i) n' ≠ 𝟬"
    using exists_indexed_eval_aux_monomial[of P Ps m i 0]
          exists_indexed_eval_aux_monomial[of Q Qs n i 0] assms(1-5,8)
    by (metis (no_types, lifting) add.right_neutral)
  have "(indexed_eval_aux (Qs @ [ Q ]) i) m' ≠ 𝟬"
    using m'(2) assms(11) by simp
  with ‹count m' i = length Ps› have "length Ps ≤ length Qs"
    using indexed_eval_aux_monomial_degree_le[of "Qs @ [ Q ]" i m'] assms(3-4,8-9) by auto
  moreover have "(indexed_eval_aux (Ps @ [ P ]) i) n' ≠ 𝟬"
    using n'(2) assms(11) by simp
  with ‹count n' i = length Qs› have "length Qs ≤ length Ps"
    using indexed_eval_aux_monomial_degree_le[of "Ps @ [ P ]" i n'] assms(1-2,5-6) by auto
  ultimately have same_len: "length (Ps @ [ P ]) = length (Qs @ [ Q ])"
    by simp
  thus "Ps = Qs" and "P = Q"
    using indexed_eval_aux_is_inj[of "Ps @ [ P ]" i "Qs @ [ Q ]"] assms(1-6,8-9,11) by auto
qed

lemma (in ring) exists_indexed_eval_monomial:
  assumes "carrier_coeff P" and "list_all carrier_coeff Qs"
    and "P n ≠ 𝟬" and "list_all (λQ. index_free Q i) Qs"
  obtains m where "count m i = length Qs + (count n i)" and "(indexed_eval (P # Qs) i) m ≠ 𝟬"
  using exists_indexed_eval_aux_monomial[OF assms(1) _ _ assms(3), of "rev Qs"] assms(2,4) by auto

corollary (in ring) exists_indexed_eval_monomial':
  assumes "carrier_coeff P" and "list_all carrier_coeff Qs"
    and "P ≠ indexed_const 𝟬" and "list_all (λQ. index_free Q i) Qs"
  obtains m where "count m i ≥ length Qs" and "(indexed_eval (P # Qs) i) m ≠ 𝟬"
proof -
  from ‹P ≠ indexed_const 𝟬› obtain n where "P n ≠ 𝟬"
    unfolding indexed_const_def by auto
  then obtain m where "count m i = length Qs + (count n i)" and "(indexed_eval (P # Qs) i) m ≠ 𝟬"
    using exists_indexed_eval_monomial[OF assms(1-2) _ assms(4)] by auto
  thus thesis
    using that by force
qed

lemma (in ring) indexed_eval_monomial_degree_le:
  assumes "list_all carrier_coeff Ps" and "list_all (λP. index_free P i) Ps"
    and "(indexed_eval Ps i) m ≠ 𝟬" shows "count m i ≤ length Ps - 1"
  using indexed_eval_aux_monomial_degree_le[of "rev Ps"] assms by auto

lemma (in ring) indexed_eval_is_inj:
  assumes "list_all carrier_coeff Ps" and "list_all (λP. index_free P i) Ps"
      and "list_all carrier_coeff Qs" and "list_all (λQ. index_free Q i) Qs"
      and "carrier_coeff P" and "index_free P i" "P ≠ indexed_const 𝟬"
      and "carrier_coeff Q" and "index_free Q i" "Q ≠ indexed_const 𝟬"
    and "indexed_eval (P # Ps) i = indexed_eval (Q # Qs) i"
  shows "Ps = Qs" and "P = Q"
proof -
  have rev_cond:
    "list_all carrier_coeff (rev Ps)" "list_all (λP. index_free P i) (rev Ps)"
    "list_all carrier_coeff (rev Qs)" "list_all (λQ. index_free Q i) (rev Qs)"
    using assms(1-4) by auto
  show "Ps = Qs" and "P = Q"
    using indexed_eval_aux_is_inj'[OF rev_cond assms(5-10)] assms(11) by auto
qed

lemma (in ring) indexed_eval_inj_on_carrier:
  assumes "⋀P. P ∈ carrier L ⟹ carrier_coeff P" and "⋀P. P ∈ carrier L ⟹ index_free P i" and "𝟬⇘L⇙ = indexed_const 𝟬"
  shows "inj_on (λPs. indexed_eval Ps i) (carrier (poly_ring L))"
proof -
  have aux_lemma: "Ps = []"
    if "Ps ∈ carrier (poly_ring L)" and "indexed_eval Ps i = indexed_const 𝟬" for Ps
  proof (rule ccontr)
    assume "¬ ?thesis"
    then obtain P' Ps' where Ps: "Ps = P' # Ps'"
      using list.exhaust by blast
    with ‹Ps ∈ carrier (poly_ring L)›
    have "P' ≠ indexed_const 𝟬" and "list_all carrier_coeff Ps" and "list_all (λP. index_free P i) Ps"
      using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def
      by (simp add: list.pred_set subset_code(1))+
    then obtain m where "(indexed_eval Ps i) m ≠ 𝟬"
      using exists_indexed_eval_monomial'[of P' Ps'] unfolding Ps by auto
    hence "indexed_eval Ps i ≠ indexed_const 𝟬"
      unfolding indexed_const_def by auto
    with ‹indexed_eval Ps i = indexed_const 𝟬› show False by simp
  qed

  show ?thesis
  proof (rule inj_onI)
    fix Ps Qs
    assume "Ps ∈ carrier (poly_ring L)" and "Qs ∈ carrier (poly_ring L)"
    show "indexed_eval Ps i = indexed_eval Qs i ⟹ Ps = Qs"
    proof (cases)
      assume "Qs = []" and "indexed_eval Ps i = indexed_eval Qs i"
      with ‹Ps ∈ carrier (poly_ring L)› show "Ps = Qs"
        using aux_lemma by simp
    next
      assume "Qs ≠ []" and eq: "indexed_eval Ps i = indexed_eval Qs i"
      with ‹Qs ∈ carrier (poly_ring L)› have "Ps ≠ []"
        using aux_lemma by auto
      from ‹Ps ≠ []› and ‹Qs ≠ []› obtain P' Ps' Q' Qs' where Ps: "Ps = P' # Ps'" and Qs: "Qs = Q' # Qs'"
        using list.exhaust by metis

      from ‹Ps ∈ carrier (poly_ring L)› and ‹Ps = P' # Ps'›
      have "carrier_coeff P'" and "index_free P' i" "P' ≠ indexed_const 𝟬"
       and "list_all carrier_coeff Ps'" and "list_all (λP. index_free P i) Ps'"
        using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def
        by (simp add: list.pred_set subset_code(1))+
      moreover 
      from ‹Qs ∈ carrier (poly_ring L)› and ‹Qs = Q' # Qs'›
      have "carrier_coeff Q'" and "index_free Q' i" "Q' ≠ indexed_const 𝟬"
       and "list_all carrier_coeff Qs'" and "list_all (λP. index_free P i) Qs'"
        using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def
        by (simp add: list.pred_set subset_code(1))+
      ultimately show ?thesis
        using indexed_eval_is_inj[of Ps' i Qs' P' Q'] eq unfolding Ps Qs by auto
    qed
  qed
qed


subsection ‹Link with Weak Morphisms›

text ‹We study some elements of the contradiction needed in the algebraic closure existence proof. ›

context ring
begin

lemma (in ring) indexed_padd_index_free:
  assumes "index_free P i" and "index_free Q i" shows "index_free (P ⨁ Q) i"
  using assms unfolding indexed_padd_def index_free_def by auto

lemma (in ring) indexed_pmult_index_free:
  assumes "index_free P j" and "i ≠ j" shows "index_free (P ⨂ i) j"
  using assms unfolding index_free_def indexed_pmult_def
  by (metis insert_DiffM insert_noteq_member)

lemma (in ring) indexed_eval_index_free:
  assumes "list_all (λP. index_free P j) Ps" and "i ≠ j" shows "index_free (indexed_eval Ps i) j"
proof -
  have "index_free (indexed_eval_aux Ps i) j" if "list_all (λP. index_free P j) Ps" for Ps
    using that indexed_padd_index_free[OF indexed_pmult_index_free[OF _ assms(2)]]
    by (induct Ps) (auto simp add: indexed_zero_def index_free_def)
  thus ?thesis
    using assms(1) by auto
qed

context
  fixes L :: "(('c multiset) ⇒ 'a) ring" and i :: 'c
  assumes hyps:
    ― ‹i›   "field L"
    ― ‹ii›  "⋀P. P ∈ carrier L ⟹ carrier_coeff P"
    ― ‹iii› "⋀P. P ∈ carrier L ⟹ index_free P i"
    ― ‹iv›  "𝟬⇘L⇙ = indexed_const 𝟬"
begin

interpretation L: field L
  using ‹field L› .

interpretation UP: principal_domain "poly_ring L"
  using L.univ_poly_is_principal[OF L.carrier_is_subfield] .


abbreviation eval_pmod
  where "eval_pmod q ≡ (λp. indexed_eval (L.pmod p q) i)"

abbreviation image_poly
  where "image_poly q ≡ image_ring (eval_pmod q) (poly_ring L)"


lemma indexed_eval_is_weak_ring_morphism:
  assumes "q ∈ carrier (poly_ring L)" shows "weak_ring_morphism (eval_pmod q) (PIdl⇘poly_ring L⇙ q) (poly_ring L)"
proof (rule weak_ring_morphismI)
  show "ideal (PIdl⇘poly_ring L⇙ q) (poly_ring L)"
    using UP.cgenideal_ideal[OF assms] .
next
  fix a b assume in_carrier: "a ∈ carrier (poly_ring L)" "b ∈ carrier (poly_ring L)"
  note ldiv_closed = in_carrier[THEN L.long_division_closed(2)[OF L.carrier_is_subfield _ assms]]

  have "(eval_pmod q) a = (eval_pmod q) b ⟷ L.pmod a q = L.pmod b q"
    using inj_onD[OF indexed_eval_inj_on_carrier[OF hyps(2-4)] _ ldiv_closed] by fastforce
  also have " ... ⟷ q pdivides⇘L⇙ (a ⊖⇘poly_ring L⇙ b)"
    unfolding L.same_pmod_iff_pdivides[OF L.carrier_is_subfield in_carrier assms] ..
  also have " ... ⟷ PIdl⇘poly_ring L⇙ (a ⊖⇘poly_ring L⇙ b) ⊆ PIdl⇘poly_ring L⇙ q"
    unfolding UP.to_contain_is_to_divide[OF assms UP.minus_closed[OF in_carrier]] pdivides_def ..
  also have " ... ⟷ a ⊖⇘poly_ring L⇙ b ∈ PIdl⇘poly_ring L⇙ q"
    unfolding UP.cgenideal_eq_genideal[OF assms] UP.cgenideal_eq_genideal[OF UP.minus_closed[OF in_carrier]]
              UP.Idl_subset_ideal'[OF UP.minus_closed[OF in_carrier] assms] ..
  finally show "(eval_pmod q) a = (eval_pmod q) b ⟷ a ⊖⇘poly_ring L⇙ b ∈ PIdl⇘poly_ring L⇙ q" .
qed

lemma eval_norm_eq_id:
  assumes "q ∈ carrier (poly_ring L)" and "degree q > 0" and "a ∈ carrier L"
  shows "((eval_pmod q) ∘ (ring.poly_of_const L)) a = a"
proof (cases)
  assume "a = 𝟬⇘L⇙" thus ?thesis
    using L.long_division_zero(2)[OF L.carrier_is_subfield assms(1)] hyps(4)
    unfolding ring.poly_of_const_def[OF L.ring_axioms] by auto
next
  assume "a ≠ 𝟬⇘L⇙" then have in_carrier: "[ a ] ∈ carrier (poly_ring L)"
    using assms(3) unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def by simp
  from ‹a ≠ 𝟬⇘L⇙› show ?thesis
    using L.pmod_const(2)[OF L.carrier_is_subfield in_carrier assms(1)] assms(2)
          indexed_padd_zero(2)[OF hyps(2)[OF assms(3)]]
    unfolding ring.poly_of_const_def[OF L.ring_axioms] by auto
qed

lemma image_poly_iso_incl:
  assumes "q ∈ carrier (poly_ring L)" and "degree q > 0" shows "id ∈ ring_hom L (image_poly q)"
proof -
  have "((eval_pmod q) ∘ L.poly_of_const) ∈ ring_hom L (image_poly q)"
    using ring_hom_trans[OF L.canonical_embedding_is_hom[OF L.carrier_is_subring]
          UP.weak_ring_morphism_is_hom[OF indexed_eval_is_weak_ring_morphism[OF assms(1)]]]
    by simp
  thus ?thesis
    using eval_norm_eq_id[OF assms(1-2)] L.ring_hom_restrict[of _ "image_poly q" id] by auto
qed

lemma image_poly_is_field:
  assumes "q ∈ carrier (poly_ring L)" and "pirreducible⇘L⇙ (carrier L) q" shows "field (image_poly q)"
  using UP.image_ring_is_field[OF indexed_eval_is_weak_ring_morphism[OF assms(1)]] assms(2)
  unfolding sym[OF L.rupture_is_field_iff_pirreducible[OF L.carrier_is_subfield assms(1)]] rupture_def
  by simp

lemma image_poly_index_free:
  assumes "q ∈ carrier (poly_ring L)" and "P ∈ carrier (image_poly q)" and "¬ index_free P j" "i ≠ j"
  obtains Q where "Q ∈ carrier L" and "¬ index_free Q j"
proof -
  from ‹P ∈ carrier (image_poly q)› obtain p where p: "p ∈ carrier (poly_ring L)" and P: "P = (eval_pmod q) p"
    unfolding image_ring_carrier by blast
  from ‹¬ index_free P j› have "¬ list_all (λP. index_free P j) (L.pmod p q)"
    using indexed_eval_index_free[OF _ assms(4), of "L.pmod p q"] unfolding sym[OF P] by auto
  then obtain Q where "Q ∈ set (L.pmod p q)" and "¬ index_free Q j"
    unfolding list_all_iff by auto
  thus ?thesis
    using L.long_division_closed(2)[OF L.carrier_is_subfield p assms(1)] that
    unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def
    by auto
qed

lemma eval_pmod_var:
  assumes "indexed_const ∈ ring_hom R L" and "q ∈ carrier (poly_ring L)" and "degree q > 1"
  shows "(eval_pmod q) X⇘L⇙ = 𝒳⇘i⇙" and "𝒳⇘i⇙ ∈ carrier (image_poly q)"
proof -
  have "X⇘L⇙ = [ indexed_const 𝟭, indexed_const 𝟬 ]" and "X⇘L⇙ ∈ carrier (poly_ring L)"
    using ring_hom_one[OF assms(1)] hyps(4) L.var_closed(1) L.carrier_is_subring unfolding var_def by auto
  thus "(eval_pmod q) X⇘L⇙ = 𝒳⇘i⇙"
    using L.pmod_const(2)[OF L.carrier_is_subfield _ assms(2), of "X⇘L⇙"] assms(3)
    by (auto simp add: indexed_pmult_def indexed_padd_def indexed_const_def indexed_var_def)
  with ‹X⇘L⇙ ∈ carrier (poly_ring L)› show "𝒳⇘i⇙ ∈ carrier (image_poly q)"
    using image_iff unfolding image_ring_carrier by fastforce
qed

lemma image_poly_eval_indexed_var:
  assumes "indexed_const ∈ ring_hom R L"
    and "q ∈ carrier (poly_ring L)" and "degree q > 1" and "pirreducible⇘L⇙ (carrier L) q"
  shows "(ring.eval (image_poly q)) q 𝒳⇘i⇙ = 𝟬⇘image_poly q⇙"
proof -
  let ?surj = "L.rupture_surj (carrier L) q"
  let ?Rupt = "Rupt⇘L⇙ (carrier L) q"
  let ?f = "eval_pmod q"

  interpret UP: ring "poly_ring L"
    using L.univ_poly_is_ring[OF L.carrier_is_subring] .
  from ‹pirreducible⇘L⇙ (carrier L) q› interpret Rupt: field ?Rupt
    using L.rupture_is_field_iff_pirreducible[OF L.carrier_is_subfield assms(2)] by simp

  have weak_morphism: "weak_ring_morphism ?f (PIdl⇘poly_ring L⇙ q) (poly_ring L)"
    using indexed_eval_is_weak_ring_morphism[OF assms(2)] .
  then interpret I: ideal "PIdl⇘poly_ring L⇙ q" "poly_ring L"
    using weak_ring_morphism.axioms(1) by auto
  interpret Hom: ring_hom_ring ?Rupt "image_poly q" "λx. the_elem (?f ` x)"
    using ring_hom_ring.intro[OF I.quotient_is_ring UP.image_ring_is_ring[OF weak_morphism]]
          UP.weak_ring_morphism_is_iso[OF weak_morphism]
    unfolding ring_iso_def symmetric[OF ring_hom_ring_axioms_def] rupture_def
    by auto

  have "set q ⊆ carrier L" and lc: "q ≠ [] ⟹ lead_coeff q ∈ carrier L - { 𝟬⇘L⇙ }"
    using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by auto

  have map_surj: "set (map (?surj ∘ L.poly_of_const) q) ⊆ carrier ?Rupt"
  proof -
    have "L.poly_of_const a ∈ carrier (poly_ring L)" if "a ∈ carrier L" for a
      using that L.normalize_gives_polynomial[of "[ a ]"]
      unfolding univ_poly_carrier ring.poly_of_const_def[OF L.ring_axioms] by simp
    hence "(?surj ∘ L.poly_of_const) a ∈ carrier ?Rupt" if "a ∈ carrier L" for a
      using ring_hom_memE(1)[OF L.rupture_surj_hom(1)[OF L.carrier_is_subring assms(2)]] that by simp
    with ‹set q ⊆ carrier L› show ?thesis
      by (induct q) (auto)
  qed

  have "?surj X⇘L⇙ ∈ carrier ?Rupt"
    using ring_hom_memE(1)[OF L.rupture_surj_hom(1)[OF _ assms(2)] L.var_closed(1)] L.carrier_is_subring by simp
  moreover have "map (λx. the_elem (?f ` x)) (map (?surj ∘ L.poly_of_const) q) = q"
  proof -
    define g where "g = (?surj ∘ L.poly_of_const)"
    define f where "f = (λx. the_elem (?f ` x))"

    have "the_elem (?f ` ((?surj ∘ L.poly_of_const) a)) = ((eval_pmod q) ∘ L.poly_of_const) a"
      if "a ∈ carrier L" for a
      using that L.normalize_gives_polynomial[of "[ a ]"] UP.weak_ring_morphism_range[OF weak_morphism]
      unfolding univ_poly_carrier ring.poly_of_const_def[OF L.ring_axioms] by auto
    hence "the_elem (?f ` ((?surj ∘ L.poly_of_const) a)) = a" if "a ∈ carrier L" for a
      using eval_norm_eq_id[OF assms(2)] that assms(3) by simp
    hence "f (g a) = a" if "a ∈ carrier L" for a
      using that unfolding f_def g_def by simp
    with ‹set q ⊆ carrier L› have "map f (map g q) = q"
      by (induct q) (auto)
    thus ?thesis
      unfolding f_def g_def by simp
  qed
  moreover have "(λx. the_elem (?f ` x)) (?surj X⇘L⇙) = 𝒳⇘i⇙"
    using UP.weak_ring_morphism_range[OF weak_morphism L.var_closed(1)[OF L.carrier_is_subring]]
    unfolding eval_pmod_var(1)[OF assms(1-3)] by simp
  ultimately have "Hom.S.eval q 𝒳⇘i⇙ = (λx. the_elem (?f ` x)) (Rupt.eval (map (?surj ∘ L.poly_of_const) q) (?surj X⇘L⇙))"
    using Hom.eval_hom'[OF _ map_surj] by auto
  moreover have "𝟬⇘?Rupt⇙ = ?surj 𝟬⇘poly_ring L⇙"
    unfolding rupture_def FactRing_def by (simp add: I.a_rcos_const)
  hence "the_elem (?f ` 𝟬⇘?Rupt⇙) = 𝟬⇘image_poly q⇙"
    using UP.weak_ring_morphism_range[OF weak_morphism UP.zero_closed]
    unfolding image_ring_zero by simp 
  hence "(λx. the_elem (?f ` x)) (Rupt.eval (map (?surj ∘ L.poly_of_const) q) (?surj X⇘L⇙)) = 𝟬⇘image_poly q⇙"
    using L.polynomial_rupture[OF L.carrier_is_subring assms(2)] by simp
  ultimately show ?thesis
    by simp
qed

end (* of fixed L context. *)

end (* of ring context. *)

end