Theory Closure_Algebraic

section ‹The Algebraic Closure of a Field›

theory Closure_Algebraic
  imports Closure_Extension Poly_Typeclass Algebraic_Transitivity Extension_Properties
    Finite_Generated_Extension Linear_System
    "HOL-Computational_Algebra.Polynomial_Factorial" "HOL-Computational_Algebra.Field_as_Ring"
begin

text ‹
  ‹Closure_Extension› produces, for any field, an extension inside the indexed
  polynomial ring in which every polynomial over the base field splits.  That extension is not yet an
  algebraic closure: it is far too big, being generated by one indeterminate for every polynomial and
  root index, and it is not algebraic over the base.  The closure is cut out of it as the set of
  elements algebraic over the base.

  Rather than redo the theory of algebraicity over a subfield for locale fields, we transport the
  extension onto a type.  The development's field-extension and Galois theory already works with an
  ambient type-class field and subfields as carrier sets, and once the extension is a type all of it
  applies --- in particular @{thm [source] subfield_algebraic_elements}, which is the statement that
  the algebraic elements form a subfield.
›

subsection ‹An extension of the whole type in which every polynomial splits›

context poly_TC
begin

text ‹A definite choice among the extensions supplied by @{thm [source] exists_extension_with_roots},
  so that the type constructed from it below depends on nothing but @{typ 'a}.›

definition wide_extension
  where "wide_extension ≡
    (SOME M. is_extension M
             ∧ (∀P ∈ poly_carrier.
                  Field.splits (ecarrier M) (eadd M) (emult M) ipoly_zero ipoly_one (lift_poly P)))"

lemma wide_extension_spec:
  "is_extension wide_extension
   ∧ (∀P ∈ poly_carrier.
        Field.splits (ecarrier wide_extension) (eadd wide_extension) (emult wide_extension)
                     ipoly_zero ipoly_one (lift_poly P))"
  unfolding wide_extension_def
  by (rule someI_ex) (metis exists_extension_with_roots)

lemmas is_extension_wide_extension = wide_extension_spec [THEN conjunct1]

lemma wide_extension_splits:
  "P ∈ poly_carrier
   ⟹ Field.splits (ecarrier wide_extension) (eadd wide_extension) (emult wide_extension)
                    ipoly_zero ipoly_one (lift_poly P)"
  using wide_extension_spec by blast

text ‹The field structure of the chosen extension, named once for the transport below.›
lemma field_wide_extension:
  "Field (ecarrier wide_extension) (eadd wide_extension) (emult wide_extension)
         ipoly_zero ipoly_one"
  by (rule is_extension_field [OF is_extension_wide_extension])

lemma wide_extension_nonempty: "ipoly_zero ∈ ecarrier wide_extension"
proof -
  interpret W: Field "ecarrier wide_extension" "eadd wide_extension" "emult wide_extension"
                    ipoly_zero ipoly_one
    by (rule field_wide_extension)
  show ?thesis by (rule W.additive.unit_closed)
qed

text ‹How the base field sits inside the extension.  These are restatements of the extension
  conditions at the chosen extension: only facts proved ∗‹in this locale› are available once it is
  left, and the type constructed below can only be spoken of outside it.›

lemma wide_const_mem: "ipoly_const a ∈ ecarrier wide_extension"
  by (simp add: is_extension_const_mem [OF is_extension_wide_extension])

lemma wide_const_add:
  "eadd wide_extension (ipoly_const a) (ipoly_const b) = ipoly_const (a + b)"
  by (simp add: is_extension_const_add [OF is_extension_wide_extension])

lemma wide_const_mult:
  "emult wide_extension (ipoly_const a) (ipoly_const b) = ipoly_const (a * b)"
  by (simp add: is_extension_const_mult [OF is_extension_wide_extension])

lemmas wide_const_inj = ipoly_const_inj_on
lemmas wide_lift_poly_apply = lift_poly_apply
lemmas wide_const_zero = ipoly_const_zero
lemmas wide_const_one = ipoly_const_one

end


subsection ‹The extension as a type›

text ‹The extension is a field, but a locale one, on a carrier set inside the indexed polynomial
  ring.  Carving that carrier out as a type and transporting the operations onto it makes it a
  type-class field, which is what the rest of the development can use.›

typedef (overloaded) 'a :: field wide = "ecarrier (poly_TC.wide_extension :: 'a iext)"
  using wide_extension_nonempty by blast

setup_lifting type_definition_wide

text ‹Names for the transported structure.  The locale's constants must be spelled out here because
  @{locale poly_TC} fixes no parameters, so its abbreviations do not reach outside it; each takes
  only the parameters occurring in its definition.›

abbreviation wcarrier :: "'a :: field ipoly set"
  where "wcarrier ≡ ecarrier (poly_TC.wide_extension :: 'a iext)"

abbreviation wadd :: "'a :: field ipoly ⇒ 'a ipoly ⇒ 'a ipoly"
  where "wadd ≡ eadd (poly_TC.wide_extension :: 'a iext)"

abbreviation wmult :: "'a :: field ipoly ⇒ 'a ipoly ⇒ 'a ipoly"
  where "wmult ≡ emult (poly_TC.wide_extension :: 'a iext)"

abbreviation wzero :: "'a :: field ipoly"
  where "wzero ≡ Ring.ipoly_zero 0"

abbreviation wone :: "'a :: field ipoly"
  where "wone ≡ Ring.ipoly_one 0 1"

abbreviation wneg :: "'a :: field ipoly ⇒ 'a ipoly"
  where "wneg ≡ Monoid.inverse wcarrier wadd wzero"

abbreviation winv :: "'a :: field ipoly ⇒ 'a ipoly"
  where "winv ≡ Monoid.inverse wcarrier wmult wone"

interpretation W: Field wcarrier wadd wmult wzero wone
  by (rule field_wide_extension)

instantiation wide :: (field) field
begin

lift_definition zero_wide :: "'a wide" is "wzero :: 'a ipoly"
  by (rule W.additive.unit_closed)

lift_definition one_wide :: "'a wide" is "wone :: 'a ipoly"
  by (rule W.multiplicative.unit_closed)

lift_definition plus_wide :: "'a wide ⇒ 'a wide ⇒ 'a wide" is "wadd :: 'a ipoly ⇒ _"
  by (rule W.additive.composition_closed)

lift_definition times_wide :: "'a wide ⇒ 'a wide ⇒ 'a wide" is "wmult :: 'a ipoly ⇒ _"
  by (rule W.multiplicative.composition_closed)

lift_definition uminus_wide :: "'a wide ⇒ 'a wide" is "wneg :: 'a ipoly ⇒ _"
  by simp

lift_definition minus_wide :: "'a wide ⇒ 'a wide ⇒ 'a wide"
  is "λx y. wadd x (wneg y) :: 'a ipoly"
  by simp

text ‹HOL's field class requires @{term "inverse 0 = 0"}, where the locale leaves the inverse of
  @{term wzero} unspecified; the two are reconciled by the case split.›
lift_definition inverse_wide :: "'a wide ⇒ 'a wide"
  is "λx. if x = wzero then wzero else winv x :: 'a ipoly"
  by (auto intro: W.multiplicative.invertible_inverse_closed W.field_inverse)

lift_definition divide_wide :: "'a wide ⇒ 'a wide ⇒ 'a wide"
  is "λx y. if y = wzero then wzero else wmult x (winv y) :: 'a ipoly"
  by (auto intro: W.multiplicative.invertible_inverse_closed W.field_inverse)

instance
proof (standard, goal_cases)
  case 1 show ?case by transfer (rule W.multiplicative.associative)
next
  case 2 show ?case by transfer (rule W.multiplicative.commutative)
next
  case 3 show ?case by transfer (rule W.multiplicative.left_unit)
next
  case 4 show ?case by transfer (rule W.additive.associative)
next
  case 5 show ?case by transfer (rule W.additive.commutative)
next
  case 6 show ?case by transfer (rule W.additive.left_unit)
next
  case 7 show ?case by transfer simp
next
  case 8 show ?case by transfer simp
next
  case 9 show ?case by transfer (rule W.distributive)
next
  case 10 show ?case by transfer (rule not_sym [OF W.nontrivial])
next
  case 11 then show ?case
    by transfer (auto intro: W.field_inverse W.multiplicative.invertible_left_inverse)
next
  case 12 then show ?case by transfer auto
next
  case 13 then show ?case by transfer auto
qed

end

text ‹A field is a Euclidean ring in a trivial way.  Spelling that out for @{typ "'a wide"} --- as
  HOL-Algebra's ‹Algebraic_Closure_Type› does for its own closure type --- is what puts
  @{typ "'a wide poly"} in @{class factorial_semiring}, and so makes HOL's factorisation machinery,
  in particular the primality of a monic linear polynomial, available over the extension.›

instantiation wide :: (field)
  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
begin

definition [simp]: "normalize_wide = (normalize_field :: 'a wide ⇒ _)"
definition [simp]: "unit_factor_wide = (unit_factor_field :: 'a wide ⇒ _)"
definition [simp]: "modulo_wide = (mod_field :: 'a wide ⇒ _)"
definition [simp]: "euclidean_size_wide = (euclidean_size_field :: 'a wide ⇒ _)"
definition [simp]: "division_segment (x :: 'a wide) = 1"

instance
  by standard (simp_all add: dvd_field_iff field_split_simps split: if_splits)

end

instantiation wide :: (field) euclidean_ring_gcd
begin

definition gcd_wide :: "'a wide ⇒ 'a wide ⇒ 'a wide"
  where "gcd_wide = Euclidean_Algorithm.gcd"
definition lcm_wide :: "'a wide ⇒ 'a wide ⇒ 'a wide"
  where "lcm_wide = Euclidean_Algorithm.lcm"
definition Gcd_wide :: "'a wide set ⇒ 'a wide"
  where "Gcd_wide = Euclidean_Algorithm.Gcd"
definition Lcm_wide :: "'a wide set ⇒ 'a wide"
  where "Lcm_wide = Euclidean_Algorithm.Lcm"

instance
  by standard (simp_all add: gcd_wide_def lcm_wide_def Gcd_wide_def Lcm_wide_def)

end

instance wide :: (field) semiring_gcd_mult_normalize ..

text ‹The four instances above are exactly @{class field_gcd}, which is the sort under which HOL states
  the primality of a monic linear polynomial.›
instance wide :: (field) field_gcd ..


subsection ‹The base field inside the extension›

text ‹The base field sits in the extension as the constants.  This is the embedding along which the
  algebraic closure will be described: a subfield of @{typ "'a wide"} isomorphic to @{typ 'a}.›

lift_definition to_wide :: "'a :: field ⇒ 'a wide" is "Ring.ipoly_const 0 :: 'a ⇒ 'a ipoly"
  by (rule wide_const_mem)

lemma to_wide_zero [simp]: "to_wide 0 = 0"
  by transfer (rule wide_const_zero)

lemma to_wide_one [simp]: "to_wide 1 = 1"
  by transfer (rule wide_const_one)

lemma to_wide_add [simp]: "to_wide (x + y) = to_wide x + to_wide y"
  by transfer (rule wide_const_add [symmetric])

lemma to_wide_mult [simp]: "to_wide (x * y) = to_wide x * to_wide y"
  by transfer (rule wide_const_mult [symmetric])

lemma inj_to_wide: "inj (to_wide :: 'a :: field ⇒ 'a wide)"
  by (metis UNIV_I injI inj_on_eq_iff to_wide.rep_eq wide_const_inj)

lemma to_wide_eq_iff [simp]: "to_wide x = to_wide y ⟷ x = y"
  using inj_to_wide by (auto dest: injD)

text ‹Being a ring homomorphism between fields, the embedding automatically respects negation and
  inversion: each is pinned by the equation it solves.›

lemma to_wide_uminus [simp]: "to_wide (- x) = - to_wide x"    
  using to_wide_add [of "- x" x] eq_neg_iff_add_eq_0 by auto

lemma to_wide_inverse [simp]: "to_wide (inverse x) = inverse (to_wide x)"
  using to_wide_mult [of x "inverse x"] inverse_unique right_inverse[of x] by fastforce

lemma to_wide_diff [simp]: "to_wide (x - y) = to_wide x - to_wide y"
  using to_wide_add [of x "- y"] by simp

theorem subfield_range_to_wide: "Subfield (range (to_wide :: 'a :: field ⇒ 'a wide))"
proof
  show "(0 :: 'a wide) ∈ range to_wide" using rangeI [of to_wide 0] by simp
  show "(1 :: 'a wide) ∈ range to_wide" using rangeI [of to_wide 1] by simp
qed (auto simp flip: to_wide_add to_wide_uminus to_wide_mult to_wide_inverse)

text ‹The inverse of the embedding, so that a polynomial over the base subfield can be read back as
  a polynomial over @{typ 'a}.›

definition of_wide :: "'a :: field wide ⇒ 'a"
  where "of_wide = inv to_wide"

lemma of_wide_to_wide [simp]: "of_wide (to_wide x) = x"
  by (simp add: of_wide_def inj_to_wide)

lemma to_wide_of_wide [simp]: "x ∈ range to_wide ⟹ to_wide (of_wide x) = x"
  by (auto simp: of_wide_def f_inv_into_f)

lemma of_wide_zero [simp]: "of_wide 0 = 0"
  by (metis of_wide_to_wide to_wide_zero)


subsection ‹Every polynomial over the base subfield splits›

text ‹@{const Abs_wide} is a field isomorphism from the carrier onto the type, so
  @{thm [source] splits_hom} carries the splitting of a base polynomial across.  Each equation below
  is read off from the corresponding ‹rep_eq› of the transported operation.›

lemma Abs_wide_zero [simp]: "Abs_wide wzero = 0"
  using Rep_wide_inverse [of 0] by (simp add: zero_wide.rep_eq)

lemma Abs_wide_one [simp]: "Abs_wide wone = 1"
  using Rep_wide_inverse [of 1] by (simp add: one_wide.rep_eq)

lemma Abs_wide_add:
  assumes "x ∈ wcarrier" and "y ∈ wcarrier"
  shows "Abs_wide (wadd x y) = Abs_wide x + Abs_wide y"
  using Rep_wide_inverse [of "Abs_wide x + Abs_wide y"]
  by (simp add: plus_wide.rep_eq Abs_wide_inverse assms)

lemma Abs_wide_mult:
  assumes "x ∈ wcarrier" and "y ∈ wcarrier"
  shows "Abs_wide (wmult x y) = Abs_wide x * Abs_wide y"
  using Rep_wide_inverse [of "Abs_wide x * Abs_wide y"]
  by (simp add: times_wide.rep_eq Abs_wide_inverse assms)

lemma Abs_wide_const [simp]: "Abs_wide (Ring.ipoly_const 0 a) = to_wide a"
  by (simp add: to_wide.abs_eq)

text ‹A polynomial whose coefficients lie in the base subfield, read back as a polynomial over the
  base field itself.›

definition wide_pull :: "'a :: field wide poly ⇒ nat ⇒ 'a"
  where "wide_pull p ≡ (λk. of_wide (Polynomial.coeff p k))"

lemma wide_pull_carrier: "wide_pull p ∈ Ring.poly_carrier (UNIV :: 'a :: field set) 0"
proof -
  have "{k. wide_pull p k ≠ 0} ⊆ {k. Polynomial.coeff p k ≠ 0}"
    by (auto simp: wide_pull_def)
  then have "finite {k. wide_pull p k ≠ (0 :: 'a)}"
    by (rule finite_subset) simp
  then show ?thesis by (simp add: poly_carrier_iff)
qed

lemma to_wide_wide_pull:
  assumes p: "p ∈ poly_over (range (to_wide :: 'a :: field ⇒ 'a wide))"
  shows "to_wide (wide_pull p k) = Polynomial.coeff p k"
  by (simp add: Subfield.poly_over_coeff p subfield_range_to_wide wide_pull_def)

theorem wide_splits:
  fixes p :: "'a :: field wide poly"
  assumes p: "p ∈ poly_over (range to_wide)"
  obtains c as where "p = [:c:] * (∏a←as. [:uminus a, 1:])"
proof -
  have RA: "Ring wcarrier wadd wmult (wzero :: 'a ipoly) wone"
    using W.Ring_axioms by simp
  have RB: "Ring (UNIV :: 'a wide set) (+) (*) 0 1"
    using field_TC.Ring_axioms by simp
  have lift: "Ring.lift_poly 0 (wide_pull p) k ∈ wcarrier" for k
    by (simp add: wide_lift_poly_apply wide_const_mem)
  have spB: "Field.splits (UNIV :: 'a wide set) (+) (*) 0 1
               (λk. Abs_wide (Ring.lift_poly 0 (wide_pull p) k))"
  proof (intro splits_hom [OF RA RB])
    show "⋀y y'. ⟦ y ∈ wcarrier; y' ∈ wcarrier ⟧ ⟹ Abs_wide (wadd y y') = Abs_wide y + Abs_wide y'"
      by (rule Abs_wide_add)
    show "⋀y y'. ⟦ y ∈ wcarrier; y' ∈ wcarrier ⟧ ⟹ Abs_wide (wmult y y') = Abs_wide y * Abs_wide y'"
      by (rule Abs_wide_mult)
    show "Field wcarrier wadd wmult (wzero :: 'a ipoly) wone"
      by (rule field_wide_extension)
    show "Field (UNIV :: 'a wide set) (+) (*) 0 1"
      by (rule field_TC.Field_axioms)
    show "Field.splits wcarrier wadd wmult wzero wone (Ring.lift_poly 0 (wide_pull p))"
      by (rule wide_extension_splits [OF wide_pull_carrier])
  qed auto
  have "(λk. Abs_wide (Ring.lift_poly 0 (wide_pull p) k)) = Polynomial.coeff p"
    by (simp add: wide_lift_poly_apply to_wide_wide_pull [OF p])
  with spB have "Field.splits (UNIV :: 'a wide set) (+) (*) 0 1 (Polynomial.coeff p)"
    by simp
  then show thesis 
    using splits_coeff_iff that by blast
qed


subsection ‹The algebraic closure›

text ‹The splitting extension is far larger than an algebraic closure --- it has an indeterminate
  for every polynomial and root index, and is not algebraic over the base.  Cutting it down to the
  elements algebraic over the base gives the closure.  Nothing has to be proved about that set here:
  @{thm [source] subfield_algebraic_elements} already says it is a subfield, which is exactly what
  transporting the extension onto a type bought.›

definition alg_closure :: "'a :: field wide set"
  where "alg_closure = algebraic_elements (range to_wide)"

theorem subfield_alg_closure: "Subfield (alg_closure :: 'a :: field wide set)"
  unfolding alg_closure_def by (rule subfield_algebraic_elements [OF subfield_range_to_wide])

lemma alg_closure_iff: "x ∈ alg_closure ⟷ algebraic_over (range to_wide) x"
  by (simp add: alg_closure_def algebraic_elements_def)

theorem base_subset_alg_closure: "range (to_wide :: 'a :: field ⇒ 'a wide) ⊆ alg_closure"
    using Subfield.algebraic_over_self [OF subfield_range_to_wide] alg_closure_iff by blast

theorem algebraic_extension_alg_closure:
  "algebraic_extension (alg_closure :: 'a :: field wide set) (range to_wide)"
  by (simp add: algebraic_extension_def alg_closure_iff)

text ‹Two facts about a product of linear factors: it is monic, and its roots are exactly the
  elements of the list.›

lemma lead_coeff_linear_prod: "lead_coeff (∏a←as. [:uminus a, 1:]) = (1 :: 'b :: idom)"
proof (induct as)
  case Nil
  show ?case by simp
next
  case (Cons a as)
  have "lead_coeff ([:uminus a, 1:] * (∏b←as. [:uminus b, 1:]))
        = lead_coeff [:uminus a, 1:] * lead_coeff (∏b←as. [:uminus b, 1:])"
    by (rule lead_coeff_mult)
  with Cons show ?case by simp
qed

lemma poly_linear_prod_eq_0_iff:
  "poly (∏a←as. [:uminus a, 1:]) z = (0 :: 'b :: idom) ⟷ z ∈ set as"
  by (induct as) auto

text ‹A root of a nonzero polynomial over the base is algebraic over it, so lies in the closure ---
  that polynomial is its own witness.›
lemma alg_closure_root:
  fixes p :: "'a :: field wide poly"
  assumes "p ∈ poly_over (range to_wide)" and "p ≠ 0" and "poly p z = 0"
  shows "z ∈ alg_closure"
  using assms by (auto simp: alg_closure_iff algebraic_over_def)

text ‹Every nonzero polynomial over the base splits, with all of its roots and its leading
  coefficient inside the closure.  Because ‹splits› carries an explicit list of roots, the
  descent from the splitting extension to the closure is immediate: the very same product works,
  every factor being a root of a base polynomial and hence algebraic.›
theorem alg_closure_splits:
  fixes p :: "'a :: field wide poly"
  assumes p: "p ∈ poly_over (range to_wide)" and nz: "p ≠ 0"
  obtains c as where "c ∈ alg_closure" and "set as ⊆ alg_closure"
    and "p = [:c:] * (∏a←as. [:uminus a, 1:])"
proof -
  obtain c as where peq: "p = [:c:] * (∏a←as. [:uminus a, 1:])"
    using wide_splits [OF p] by blast
  have "c = lead_coeff p"
    by (simp add: peq lead_coeff_mult lead_coeff_linear_prod)
  then have "c ∈ range to_wide"
    using Subfield.lead_coeff_closed [OF subfield_range_to_wide p] by simp
  then have cA: "c ∈ alg_closure"
    using base_subset_alg_closure by blast
  have "a ∈ alg_closure" if "a ∈ set as" for a
    using that alg_closure_root [OF p nz] by (simp add: peq poly_linear_prod_eq_0_iff)
  then have asA: "set as ⊆ alg_closure" by blast
  show thesis by (rule that [OF cA asA peq])
qed

corollary poly_root_set_subset_alg_closure:
  fixes p :: "'a :: field wide poly"
  assumes "p ∈ poly_over (range to_wide)" and "p ≠ 0"
  shows "poly_root_set p ⊆ alg_closure"
  using alg_closure_root [OF assms] by (auto simp: poly_root_set_def)

text ‹The existence statement, in the shape of HOL-Algebra's ‹exists_closure›: every field has an
  algebraic extension in which each of its polynomials splits.›
theorem exists_closure:
  obtains L :: "'a :: field wide set"
  where "Subfield L" and "range to_wide ⊆ L" and "algebraic_extension L (range to_wide)"
    and "⋀p. ⟦ p ∈ poly_over (range to_wide); p ≠ 0 ⟧
              ⟹ ∃c as. c ∈ L ∧ set as ⊆ L ∧ p = [:c:] * (∏a←as. [:uminus a, 1:])"
  by (metis alg_closure_splits algebraic_extension_alg_closure base_subset_alg_closure
      subfield_alg_closure)


subsection ‹The closure is algebraically closed›

text ‹A divisor of a split polynomial of positive degree has a root among its factors.  Peeling one
  factor at a time: either it is a root of the divisor, or the divisor is coprime to it (linear
  monic polynomials are prime) and the factor can be cancelled.›

lemma dvd_split_imp_root:
  fixes q :: "'b :: field_gcd poly"
  assumes "q dvd [:γ:] * (∏a←as. [:uminus a, 1:])" and "γ ≠ 0" and "0 < degree q"
  shows "∃a ∈ set as. poly q a = 0"
  using assms
proof (induct as arbitrary: γ)
  case Nil
  then have "[:γ:] ≠ 0" by simp
  with Nil have "degree q ≤ degree [:γ:]"
    by (metis dvd_imp_degree_le list.map(1) mult_cancel_left1 prod_list.Nil)
  with Nil.prems(3) show ?case by simp
next
  case (Cons a as)
  then have dvd1: "q dvd [:uminus a, 1:] * ([:γ:] * (∏b←as. [:uminus b, 1:]))"
    by simp
  show ?case
  proof (cases "poly q a = 0")
    case True
    then show ?thesis by auto
  next
    case False
    then have nd: "¬ [:uminus a, 1:] dvd q"
      by (simp add: poly_eq_0_iff_dvd)
    have pe: "prime_elem [:uminus a, 1 :: 'b:]"
      by (rule prime_elem_linear_poly) simp_all
    have copq: "coprime q [:uminus a, 1 :: 'b:]"
      using coprime_commute prime_elem_imp_coprime [OF pe nd] by blast
    have "q dvd [:γ:] * (∏b←as. [:uminus b, 1:])"
      using dvd1 coprime_dvd_mult_right_iff [OF copq] by blast
    then show ?thesis
      using Cons by auto
  qed
qed

text ‹
  Every polynomial over the closure of positive degree has a root there, so the closure is
  algebraically closed.

  This is the one step of the construction that needs a dimension count, and it is HOL-Algebra's
  rupture argument in elementary form.  Normalise the polynomial to be monic and let ‹L› be a finite
  extension of the base containing its coefficients, which exists because those coefficients are
  algebraic (@{thm [source] exists_finite_subfield_tower}).  Divide ‹Xi› by the polynomial for
  ‹i ≤ n * card B›, where ‹B› is a basis of ‹L›: each remainder has degree below ‹n› and coefficients
  in ‹L›, so it is described by ‹n * card B› scalars from the base field, while there are
  ‹n * card B + 1› of them.  @{thm [source] Subfield.underdetermined_solution} therefore supplies a
  nontrivial vanishing combination, whose coefficients assemble into a nonzero polynomial ∗‹over the
  base› that the given polynomial divides.  That one splits in the closure, and a divisor of a split
  polynomial has a root.

  Where HOL-Algebra forms the quotient ‹A[X]/(P)› and compares its dimension with that of ‹K[X]›, the
  linear system does the same counting directly, so no quotient (which would change the type) is
  ever constructed.
›
theorem alg_closure_alg_closed:
  fixes p :: "'a :: field wide poly"
  assumes p: "p ∈ poly_over alg_closure" and dp: "0 < degree p"
  obtains z where "z ∈ alg_closure" and "poly p z = 0"
proof -
  interpret K: Subfield "range (to_wide :: 'a ⇒ 'a wide)" by (rule subfield_range_to_wide)
  interpret A: Subfield "alg_closure :: 'a wide set" by (rule subfield_alg_closure)

  ― ‹Normalise to a monic polynomial with the same roots.›
  define q where "q ≡ smult (inverse (lead_coeff p)) p"
  have pnz: "p ≠ 0" using dp by auto
  then have lc: "lead_coeff p ≠ 0" by simp
  have lcA: "lead_coeff p ∈ alg_closure" by (rule A.lead_coeff_closed [OF p])
  have qA: "q ∈ poly_over alg_closure"
    unfolding q_def using p lcA by (auto intro: A.poly_over_smult A.inverse_closed)
  have dq: "degree q = degree p" by (simp add: q_def lc)
  have monic: "lead_coeff q = 1" by (simp add: q_def lc pnz)
  have roots: "poly q z = 0 ⟷ poly p z = 0" for z
    using lc by (auto simp: q_def)
  define n where "n ≡ degree q"
  have npos: "0 < n" using dp dq by (simp add: n_def)

  ― ‹A finite extension of the base containing the coefficients.›
  define S where "S ≡ (λi. coeff q i) ` {..n}"
  have finS: "finite S" by (simp add: S_def)
  have SA: "S ⊆ alg_closure" using qA by (auto simp: S_def A.poly_over_coeff)
  then have algS: "algebraic_over (range to_wide) x" if "x ∈ S" for x
    using that by (auto simp: alg_closure_iff)
  obtain L where L: "finite_subfield_tower (range (to_wide :: 'a ⇒ 'a wide)) L"
    and KL: "range to_wide ⊆ L" and SL: "S ⊆ L"
    using exists_finite_subfield_tower [OF subfield_range_to_wide finS algS] by blast
  interpret T: finite_subfield_tower "range (to_wide :: 'a ⇒ 'a wide)" L by (rule L)
  have sfL: "Subfield L" by (rule T.ext.Subfield_axioms)
  have qL: "q ∈ poly_over L"
  proof (rule Subfield.poly_overI [OF sfL])
    fix i
    show "coeff q i ∈ L"
    proof (cases "i ≤ n")
      case True then show ?thesis using SL by (auto simp: S_def)
    next
      case False
      then show ?thesis using Subfield.zero_closed [OF sfL] by (simp add: coeff_eq_0 n_def)
    qed
  qed

  ― ‹Coordinates with respect to a basis of ‹L› over the base.›
  obtain B coord where finB: "finite B" and BL: "B ⊆ L"
    and coordK: "⋀x. x ∈ L ⟹ (∀b∈B. coord x b ∈ range to_wide)"
    and coordS: "⋀x. x ∈ L ⟹ x = (∑b∈B. coord x b * b)"
    using T.exists_coordinates by blast

  ― ‹Divide each power of the indeterminate by ‹q›.›
  define N where "N ≡ n * card B"
  have "∃s r. s ∈ poly_over L ∧ r ∈ poly_over L ∧ monom 1 i = s * q + r ∧ degree r < n" for i
    using T.ext.one_closed T.ext.poly_over_divmod_exists T.ext.poly_over_monom monic n_def npos qL
    by presburger
  then obtain s r where sr: "⋀i. s i ∈ poly_over L ∧ r i ∈ poly_over L
                                  ∧ monom 1 i = s i * q + r i ∧ degree (r i) < n"
    by metis
  have rL: "r i ∈ poly_over L" and rdeg: "degree (r i) < n"
    and divid: "monom (1 :: 'a wide) i = s i * q + r i" for i
    using sr by blast+
  have rcoeffL: "coeff (r i) j ∈ L" for i j
    using rL by (simp add: Subfield.poly_over_coeff [OF sfL])

  ― ‹More unknowns than equations, so a nontrivial vanishing combination exists.›
  define I where "I ≡ {..<n} × B"
  define Amat where "Amat ≡ (λ(j, b) i. coord (coeff (r i) j) b)"
  have finI: "finite I" by (simp add: I_def finB)
  have cardI: "card I = N" by (simp add: I_def N_def card_cartesian_product)
  have "card I < card {..N}" by (simp add: cardI)
  moreover have "Amat e i ∈ range to_wide" if "e ∈ I" for e i
    using that coordK [OF rcoeffL] by (auto simp: Amat_def I_def)
  ultimately obtain c where cKall: "∀j. c j ∈ range (to_wide :: 'a ⇒ 'a wide)"
    and cnz: "∃j ∈ {..N}. c j ≠ 0"
    and sysall: "∀e ∈ I. (∑i ≤ N. Amat e i * c i) = 0"
    using K.underdetermined_solution [OF finI, of "{..N}" Amat] by blast
  have cK: "c i ∈ range (to_wide :: 'a ⇒ 'a wide)" for i using cKall by blast
  have sys: "(∑i ≤ N. Amat e i * c i) = 0" if "e ∈ I" for e using sysall that by blast

  ― ‹The combination of remainders vanishes identically.›
  define R where "R = (∑i ≤ N. smult (c i) (r i))"
  have Rdeg: "degree R < n"
    using rdeg R_def by (simp add: degree_sum_less npos)
  have Rcoeff: "coeff R j = 0" if j: "j < n" for j
  proof -
    have "coeff R j = (∑i ≤ N. c i * (∑b∈B. coord (coeff (r i) j) b * b))"
      using coordS [OF rcoeffL] by (simp add: R_def coeff_sum)
    also have "… = (∑i ≤ N. ∑b∈B. c i * (coord (coeff (r i) j) b * b))"
      by (simp add: sum_distrib_left)
    also have "… = (∑b∈B. ∑i ≤ N. c i * (coord (coeff (r i) j) b * b))"
      by (rule sum.swap)
    also have "… = (∑b∈B. (∑i ≤ N. Amat (j, b) i * c i) * b)"
    proof (rule sum.cong [OF refl])
      fix b assume "b ∈ B"
      have "(∑i ≤ N. c i * (coord (coeff (r i) j) b * b)) = (∑i ≤ N. Amat (j, b) i * c i * b)"
        by (simp add: Amat_def ac_simps)
      also have "… = (∑i ≤ N. Amat (j, b) i * c i) * b"
        by (simp add: sum_distrib_right)
      finally show "(∑i ≤ N. c i * (coord (coeff (r i) j) b * b))
                    = (∑i ≤ N. Amat (j, b) i * c i) * b" .
    qed
    also have "… = 0"
      using sys j by (intro sum.neutral) (simp add: I_def)
    finally show ?thesis .
  qed
  have "R = 0"
    using Rcoeff Rdeg by fastforce

  ― ‹Hence ‹q› divides a nonzero polynomial over the base field.›
  define Q where "Q ≡ (∑i ≤ N. monom (c i) i)"
  have QK: "Q ∈ poly_over (range (to_wide :: 'a ⇒ 'a wide))"
    unfolding Q_def using cK by (auto intro!: K.poly_over_sum K.poly_over_monom)
  have coeffQ: "coeff Q i = c i" if "i ≤ N" for i
    using that by (simp add: Q_def coeff_sum)
  have Qnz: "Q ≠ 0" using cnz coeffQ by force
  have Qsplit: "Q = (∑i ≤ N. smult (c i) (s i)) * q + R"
  proof -
    have "monom (c i) i = smult (c i) (s i) * q + smult (c i) (r i)" for i
    proof -
      have "monom (c i) i = smult (c i) (monom 1 i)" by (simp add: smult_monom)
      also have "… = smult (c i) (s i) * q + smult (c i) (r i)"
        by (simp add: smult_monom divid [of i] smult_add_right mult_smult_left)
      finally show ?thesis .
    qed
    then have "Q = (∑i ≤ N. smult (c i) (s i) * q + smult (c i) (r i))"
      by (simp add: Q_def)
    also have "… = (∑i ≤ N. smult (c i) (s i)) * q + R"
      by (simp add: R_def sum.distrib sum_distrib_right)
    finally show ?thesis .
  qed
  with ‹R = 0› have qdvd: "q dvd Q" by auto

  ― ‹That polynomial splits in the closure, so ‹q› has a root there.›
  obtain γ as where γ: "γ ∈ alg_closure" and as: "set as ⊆ alg_closure"
    and Qeq: "Q = [:γ:] * (∏a←as. [:uminus a, 1:])"
    using alg_closure_splits [OF QK Qnz] by blast
  have "γ ≠ 0" using Qnz Qeq by auto
  then obtain z where z: "z ∈ set as" and "poly q z = 0"
    using dvd_split_imp_root [OF qdvd [unfolded Qeq]] npos by (auto simp: n_def)
  then show thesis
    using as roots by (blast intro: that)
qed

end