Theory Nullstellensatz
section ‹Hilbert's Nullstellensatz›
theory Nullstellensatz
imports Algebraically_Closed_Fields
"HOL-Computational_Algebra.Fraction_Field"
Lex_Order_PP
Univariate_PM
Groebner_Bases.Groebner_PM
begin
text ‹We prove the geometric version of Hilbert's Nullstellensatz, i.e. the precise correspondence
between algebraic varieties and radical ideals.
The field-theoretic version of the Nullstellensatz is proved in theory ‹Nullstellensatz_Field›.›
subsection ‹Preliminaries›
lemma finite_linorder_induct [consumes 1, case_names empty insert]:
assumes "finite (A::'a::linorder set)" and "P {}"
and "⋀a A. finite A ⟹ A ⊆ {..<a} ⟹ P A ⟹ P (insert a A)"
shows "P A"
proof -
define k where "k = card A"
thus ?thesis using assms(1)
proof (induct k arbitrary: A)
case 0
with assms(2) show ?case by simp
next
case (Suc k)
define a where "a = Max A"
from Suc.prems(1) have "A ≠ {}" by auto
with Suc.prems(2) have "a ∈ A" unfolding a_def by (rule Max_in)
with Suc.prems have "k = card (A - {a})" by simp
moreover from Suc.prems(2) have "finite (A - {a})" by simp
ultimately have "P (A - {a})" by (rule Suc.hyps)
with ‹finite (A - {a})› _ have "P (insert a (A - {a}))"
proof (rule assms(3))
show "A - {a} ⊆ {..<a}"
proof
fix b
assume "b ∈ A - {a}"
hence "b ∈ A" and "b ≠ a" by simp_all
moreover from Suc.prems(2) this(1) have "b ≤ a" unfolding a_def by (rule Max_ge)
ultimately show "b ∈ {..<a}" by simp
qed
qed
with ‹a ∈ A› show ?case by (simp add: insert_absorb)
qed
qed
lemma Fract_same: "Fract a a = (1 when a ≠ 0)"
by (simp add: One_fract_def Zero_fract_def eq_fract when_def)
lemma Fract_eq_zero_iff: "Fract a b = 0 ⟷ a = 0 ∨ b = 0"
by (metis (no_types, lifting) Zero_fract_def eq_fract(1) eq_fract(2) mult_eq_0_iff one_neq_zero)
lemma poly_plus_rightE:
obtains c where "poly p (x + y) = poly p x + c * y"
proof (induct p arbitrary: thesis)
case 0
have "poly 0 (x + y) = poly 0 x + 0 * y" by simp
thus ?case by (rule 0)
next
case (pCons a p)
obtain c where "poly p (x + y) = poly p x + c * y" by (rule pCons.hyps)
hence "poly (pCons a p) (x + y) = a + (x + y) * (poly p x + c * y)" by simp
also have "… = poly (pCons a p) x + (x * c + (poly p x + c * y)) * y" by (simp add: algebra_simps)
finally show ?case by (rule pCons.prems)
qed
lemma poly_minus_rightE:
obtains c where "poly p (x - y) = poly p x - c * (y::_::comm_ring)"
by (metis add_diff_cancel_right' diff_add_cancel poly_plus_rightE)
lemma map_poly_plus:
assumes "f 0 = 0" and "⋀a b. f (a + b) = f a + f b"
shows "map_poly f (p + q) = map_poly f p + map_poly f q"
by (rule Polynomial.poly_eqI) (simp add: coeff_map_poly assms)
lemma map_poly_minus:
assumes "f 0 = 0" and "⋀a b. f (a - b) = f a - f b"
shows "map_poly f (p - q) = map_poly f p - map_poly f q"
by (rule Polynomial.poly_eqI) (simp add: coeff_map_poly assms)
lemma map_poly_sum:
assumes "f 0 = 0" and "⋀a b. f (a + b) = f a + f b"
shows "map_poly f (sum g A) = (∑a∈A. map_poly f (g a))"
by (induct A rule: infinite_finite_induct) (simp_all add: map_poly_plus assms)
lemma map_poly_times:
assumes "f 0 = 0" and "⋀a b. f (a + b) = f a + f b" and "⋀a b. f (a * b) = f a * f b"
shows "map_poly f (p * q) = map_poly f p * map_poly f q"
proof (induct p)
case 0
show ?case by simp
next
case (pCons c p)
show ?case by (simp add: assms map_poly_plus map_poly_smult map_poly_pCons pCons)
qed
lemma poly_Fract:
assumes "set (Polynomial.coeffs p) ⊆ range (λx. Fract x 1)"
obtains q m where "poly p (Fract a b) = Fract q (b ^ m)"
using assms
proof (induct p arbitrary: thesis)
case 0
have "poly 0 (Fract a b) = Fract 0 (b ^ 1)" by (simp add: fract_collapse)
thus ?case by (rule 0)
next
case (pCons c p)
from pCons.hyps(1) have "insert c (set (Polynomial.coeffs p)) = set (Polynomial.coeffs (pCons c p))"
by auto
with pCons.prems(2) have "c ∈ range (λx. Fract x 1)" and "set (Polynomial.coeffs p) ⊆ range (λx. Fract x 1)"
by blast+
from this(2) obtain q0 m0 where poly_p: "poly p (Fract a b) = Fract q0 (b ^ m0)"
using pCons.hyps(2) by blast
from ‹c ∈ _› obtain c0 where c: "c = Fract c0 1" ..
show ?case
proof (cases "b = 0")
case True
hence "poly (pCons c p) (Fract a b) = Fract c0 (b ^ 0)" by (simp add: c fract_collapse)
thus ?thesis by (rule pCons.prems)
next
case False
hence "poly (pCons c p) (Fract a b) = Fract (c0 * b ^ Suc m0 + a * q0) (b ^ Suc m0)"
by (simp add: poly_p c)
thus ?thesis by (rule pCons.prems)
qed
qed
lemma (in ordered_term) lt_sum_le_Max: "lt (sum f A) ≼⇩t ord_term_lin.Max {lt (f a) | a. a ∈ A}"
proof (induct A rule: infinite_finite_induct)
case (infinite A)
thus ?case by (simp add: min_term_min)
next
case empty
thus ?case by (simp add: min_term_min)
next
case (insert a A)
show ?case
proof (cases "A = {}")
case True
thus ?thesis by simp
next
case False
from insert.hyps(1, 2) have "lt (sum f (insert a A)) = lt (f a + sum f A)" by simp
also have "… ≼⇩t ord_term_lin.max (lt (f a)) (lt (sum f A))" by (rule lt_plus_le_max)
also have "… ≼⇩t ord_term_lin.max (lt (f a)) (ord_term_lin.Max {lt (f a) |a. a ∈ A})"
using insert.hyps(3) ord_term_lin.max.mono by blast
also from insert.hyps(1) False have "… = ord_term_lin.Max (insert (lt (f a)) {lt (f x) |x. x ∈ A})"
by simp
also have "… = ord_term_lin.Max {lt (f x) |x. x ∈ insert a A}"
by (rule arg_cong[where f=ord_term_lin.Max]) blast
finally show ?thesis .
qed
qed
subsection ‹Ideals and Varieties›
definition variety_of :: "(('x ⇒⇩0 nat) ⇒⇩0 'a) set ⇒ ('x ⇒ 'a::comm_semiring_1) set"
where "variety_of F = {a. ∀f∈F. poly_eval a f = 0}"
definition ideal_of :: "('x ⇒ 'a::comm_semiring_1) set ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) set"
where "ideal_of A = {f. ∀a∈A. poly_eval a f = 0}"
abbreviation "𝒱 ≡ variety_of"
abbreviation "ℐ ≡ ideal_of"
lemma variety_ofI: "(⋀f. f ∈ F ⟹ poly_eval a f = 0) ⟹ a ∈ 𝒱 F"
by (simp add: variety_of_def)
lemma variety_ofI_alt: "poly_eval a ` F ⊆ {0} ⟹ a ∈ 𝒱 F"
by (auto intro: variety_ofI)
lemma variety_ofD: "a ∈ 𝒱 F ⟹ f ∈ F ⟹ poly_eval a f = 0"
by (simp add: variety_of_def)
lemma variety_of_empty [simp]: "𝒱 {} = UNIV"
by (simp add: variety_of_def)
lemma variety_of_UNIV [simp]: "𝒱 UNIV = {}"
by (metis (mono_tags, lifting) Collect_empty_eq UNIV_I one_neq_zero poly_eval_one variety_of_def)
lemma variety_of_antimono: "F ⊆ G ⟹ 𝒱 G ⊆ 𝒱 F"
by (auto simp: variety_of_def)
lemma variety_of_ideal [simp]: "𝒱 (ideal F) = 𝒱 F"
proof
show "𝒱 (ideal F) ⊆ 𝒱 F" by (intro variety_of_antimono ideal.span_superset)
next
show "𝒱 F ⊆ 𝒱 (ideal F)"
proof (intro subsetI variety_ofI)
fix a f
assume "a ∈ 𝒱 F" and "f ∈ ideal F"
from this(2) show "poly_eval a f = 0"
proof (induct f rule: ideal.span_induct_alt)
case base
show ?case by simp
next
case (step c f g)
with ‹a ∈ 𝒱 F› show ?case by (auto simp: poly_eval_plus poly_eval_times dest: variety_ofD)
qed
qed
qed
lemma ideal_ofI: "(⋀a. a ∈ A ⟹ poly_eval a f = 0) ⟹ f ∈ ℐ A"
by (simp add: ideal_of_def)
lemma ideal_ofD: "f ∈ ℐ A ⟹ a ∈ A ⟹ poly_eval a f = 0"
by (simp add: ideal_of_def)
lemma ideal_of_empty [simp]: "ℐ {} = UNIV"
by (simp add: ideal_of_def)
lemma ideal_of_antimono: "A ⊆ B ⟹ ℐ B ⊆ ℐ A"
by (auto simp: ideal_of_def)
lemma ideal_ideal_of [simp]: "ideal (ℐ A) = ℐ A"
unfolding ideal.span_eq_iff
proof (rule ideal.subspaceI)
show "0 ∈ ℐ A" by (rule ideal_ofI) simp
next
fix f g
assume "f ∈ ℐ A"
hence f: "poly_eval a f = 0" if "a ∈ A" for a using that by (rule ideal_ofD)
assume "g ∈ ℐ A"
hence g: "poly_eval a g = 0" if "a ∈ A" for a using that by (rule ideal_ofD)
show "f + g ∈ ℐ A" by (rule ideal_ofI) (simp add: poly_eval_plus f g)
next
fix c f
assume "f ∈ ℐ A"
hence f: "poly_eval a f = 0" if "a ∈ A" for a using that by (rule ideal_ofD)
show "c * f ∈ ℐ A" by (rule ideal_ofI) (simp add: poly_eval_times f)
qed
lemma ideal_of_UN: "ℐ (⋃ (A ` J)) = (⋂j∈J. ℐ (A j))"
proof (intro set_eqI iffI ideal_ofI INT_I)
fix p j a
assume "p ∈ ℐ (⋃ (A ` J))"
assume "j ∈ J" and "a ∈ A j"
hence "a ∈ ⋃ (A ` J)" ..
with ‹p ∈ _› show "poly_eval a p = 0" by (rule ideal_ofD)
next
fix p a
assume "a ∈ ⋃ (A ` J)"
then obtain j where "j ∈ J" and "a ∈ A j" ..
assume "p ∈ (⋂j∈J. ℐ (A j))"
hence "p ∈ ℐ (A j)" using ‹j ∈ J› ..
thus "poly_eval a p = 0" using ‹a ∈ A j› by (rule ideal_ofD)
qed
corollary ideal_of_Un: "ℐ (A ∪ B) = ℐ A ∩ ℐ B"
using ideal_of_UN[of id "{A, B}"] by simp
lemma variety_of_ideal_of_variety [simp]: "𝒱 (ℐ (𝒱 F)) = 𝒱 F" (is "_ = ?V")
proof
have "F ⊆ ℐ (𝒱 F)" by (auto intro!: ideal_ofI dest: variety_ofD)
thus "𝒱 (ℐ ?V) ⊆ ?V" by (rule variety_of_antimono)
next
show "?V ⊆ 𝒱 (ℐ ?V)" by (auto intro!: variety_ofI dest: ideal_ofD)
qed
lemma ideal_of_inj_on: "inj_on ℐ (range (𝒱::(('x ⇒⇩0 nat) ⇒⇩0 'a::comm_semiring_1) set ⇒ _))"
proof (rule inj_onI)
fix A B :: "('x ⇒ 'a) set"
assume "A ∈ range 𝒱"
then obtain F where A: "A = 𝒱 F" ..
assume "B ∈ range 𝒱"
then obtain G where B: "B = 𝒱 G" ..
assume "ℐ A = ℐ B"
hence "𝒱 (ℐ A) = 𝒱 (ℐ B)" by simp
thus "A = B" by (simp add: A B)
qed
lemma ideal_of_variety_of_ideal [simp]: "ℐ (𝒱 (ℐ A)) = ℐ A" (is "_ = ?I")
proof
have "A ⊆ 𝒱 (ℐ A)" by (auto intro!: variety_ofI dest: ideal_ofD)
thus "ℐ (𝒱 ?I) ⊆ ?I" by (rule ideal_of_antimono)
next
show "?I ⊆ ℐ (𝒱 ?I)" by (auto intro!: ideal_ofI dest: variety_ofD)
qed
lemma variety_of_inj_on: "inj_on 𝒱 (range (ℐ::('x ⇒ 'a::comm_semiring_1) set ⇒ _))"
proof (rule inj_onI)
fix F G :: "(('x ⇒⇩0 nat) ⇒⇩0 'a) set"
assume "F ∈ range ℐ"
then obtain A where F: "F = ℐ A" ..
assume "G ∈ range ℐ"
then obtain B where G: "G = ℐ B" ..
assume "𝒱 F = 𝒱 G"
hence "ℐ (𝒱 F) = ℐ (𝒱 G)" by simp
thus "F = G" by (simp add: F G)
qed
lemma image_map_indets_ideal_of:
assumes "inj f"
shows "map_indets f ` ℐ A = ℐ ((λa. a ∘ f) -` (A::('x ⇒ 'a::comm_semiring_1) set)) ∩ P[range f]"
proof -
{
fix p and a::"'x ⇒ 'a"
assume "∀a∈(λa. a ∘ f) -` A. poly_eval (a ∘ f) p = 0"
hence eq: "poly_eval (a ∘ f) p = 0" if "a ∘ f ∈ A" for a using that by simp
have "the_inv f ∘ f = id" by (rule ext) (simp add: assms the_inv_f_f)
hence a: "a = a ∘ the_inv f ∘ f" by (simp add: comp_assoc)
moreover assume "a ∈ A"
ultimately have "(a ∘ the_inv f) ∘ f ∈ A" by simp
hence "poly_eval ((a ∘ the_inv f) ∘ f) p = 0" by (rule eq)
hence "poly_eval a p = 0" by (simp flip: a)
}
thus ?thesis
by (auto simp: ideal_of_def poly_eval_map_indets simp flip: range_map_indets intro!: imageI)
qed
lemma variety_of_map_indets: "𝒱 (map_indets f ` F) = (λa. a ∘ f) -` 𝒱 F"
by (auto simp: variety_of_def poly_eval_map_indets)
subsection ‹Radical Ideals›
definition radical :: "'a::monoid_mult set ⇒ 'a set" (‹√(_)› [999] 999)
where "radical F = {f. ∃m. f ^ m ∈ F}"
lemma radicalI: "f ^ m ∈ F ⟹ f ∈ √F"
by (auto simp: radical_def)
lemma radicalE:
assumes "f ∈ √F"
obtains m where "f ^ m ∈ F"
using assms by (auto simp: radical_def)
lemma radical_empty [simp]: "√{} = {}"
by (simp add: radical_def)
lemma radical_UNIV [simp]: "√UNIV = UNIV"
by (simp add: radical_def)
lemma radical_ideal_eq_UNIV_iff: "√ideal F = UNIV ⟷ ideal F = UNIV"
proof
assume "√ideal F = UNIV"
hence "1 ∈ √ideal F" by simp
then obtain m where "1 ^ m ∈ ideal F" by (rule radicalE)
thus "ideal F = UNIV" by (simp add: ideal_eq_UNIV_iff_contains_one)
qed simp
lemma zero_in_radical_ideal [simp]: "0 ∈ √ideal F"
proof (rule radicalI)
show "0 ^ 1 ∈ ideal F" by (simp add: ideal.span_zero)
qed
lemma radical_mono: "F ⊆ G ⟹ √F ⊆ √G"
by (auto elim!: radicalE intro: radicalI)
lemma radical_superset: "F ⊆ √F"
proof
fix f
assume "f ∈ F"
hence "f ^ 1 ∈ F" by simp
thus "f ∈ √F" by (rule radicalI)
qed
lemma radical_idem [simp]: "√√F = √F"
proof
show "√√F ⊆ √F" by (auto elim!: radicalE intro: radicalI simp flip: power_mult)
qed (fact radical_superset)
lemma radical_Int_subset: "√(A ∩ B) ⊆ √A ∩ √B"
by (auto intro: radicalI elim: radicalE)
lemma radical_ideal_Int: "√(ideal F ∩ ideal G) = √ideal F ∩ √ideal G"
using radical_Int_subset
proof (rule subset_antisym)
show "√ideal F ∩ √ideal G ⊆ √(ideal F ∩ ideal G)"
proof
fix p
assume "p ∈ √ideal F ∩ √ideal G"
hence "p ∈ √ideal F" and "p ∈ √ideal G" by simp_all
from this(1) obtain m1 where p1: "p ^ m1 ∈ ideal F" by (rule radicalE)
from ‹p ∈ √ideal G› obtain m2 where "p ^ m2 ∈ ideal G" by (rule radicalE)
hence "p ^ m1 * p ^ m2 ∈ ideal G" by (rule ideal.span_scale)
moreover from p1 have "p ^ m2 * p ^ m1 ∈ ideal F" by (rule ideal.span_scale)
ultimately have "p ^ (m1 + m2) ∈ ideal F ∩ ideal G" by (simp add: power_add mult.commute)
thus "p ∈ √(ideal F ∩ ideal G)" by (rule radicalI)
qed
qed
lemma ideal_radical_ideal [simp]: "ideal (√ideal F) = √ideal F" (is "_ = ?R")
unfolding ideal.span_eq_iff
proof (rule ideal.subspaceI)
have "0 ^ 1 ∈ ideal F" by (simp add: ideal.span_zero)
thus "0 ∈ ?R" by (rule radicalI)
next
fix a b
assume "a ∈ ?R"
then obtain m where "a ^ m ∈ ideal F" by (rule radicalE)
have a: "a ^ k ∈ ideal F" if "m ≤ k" for k
proof -
from ‹a ^ m ∈ _› have "a ^ (k - m + m) ∈ ideal F" by (simp only: power_add ideal.span_scale)
with that show ?thesis by simp
qed
assume "b ∈ ?R"
then obtain n where "b ^ n ∈ ideal F" by (rule radicalE)
have b: "b ^ k ∈ ideal F" if "n ≤ k" for k
proof -
from ‹b ^ n ∈ _› have "b ^ (k - n + n) ∈ ideal F" by (simp only: power_add ideal.span_scale)
with that show ?thesis by simp
qed
have "(a + b) ^ (m + n) ∈ ideal F" unfolding binomial_ring
proof (rule ideal.span_sum)
fix k
show "of_nat (m + n choose k) * a ^ k * b ^ (m + n - k) ∈ ideal F"
proof (cases "k ≤ m")
case True
hence "n ≤ m + n - k" by simp
hence "b ^ (m + n - k) ∈ ideal F" by (rule b)
thus ?thesis by (rule ideal.span_scale)
next
case False
hence "m ≤ k" by simp
hence "a ^ k ∈ ideal F" by (rule a)
hence "of_nat (m + n choose k) * b ^ (m + n - k) * a ^ k ∈ ideal F" by (rule ideal.span_scale)
thus ?thesis by (simp only: ac_simps)
qed
qed
thus "a + b ∈ ?R" by (rule radicalI)
next
fix c a
assume "a ∈ ?R"
then obtain m where "a ^ m ∈ ideal F" by (rule radicalE)
hence "(c * a) ^ m ∈ ideal F" by (simp only: power_mult_distrib ideal.span_scale)
thus "c * a ∈ ?R" by (rule radicalI)
qed
lemma radical_ideal_of [simp]: "√ℐ A = ℐ (A::(_ ⇒ _::semiring_1_no_zero_divisors) set)"
proof
show "√ℐ A ⊆ ℐ A" by (auto elim!: radicalE dest!: ideal_ofD intro!: ideal_ofI simp: poly_eval_power)
qed (fact radical_superset)
lemma variety_of_radical_ideal [simp]: "𝒱 (√ideal F) = 𝒱 (F::(_ ⇒⇩0 _::semiring_1_no_zero_divisors) set)"
proof
have "F ⊆ ideal F" by (rule ideal.span_superset)
also have "… ⊆ √ideal F" by (rule radical_superset)
finally show "𝒱 (√ideal F) ⊆ 𝒱 F" by (rule variety_of_antimono)
next
show "𝒱 F ⊆ 𝒱 (√ideal F)"
proof (intro subsetI variety_ofI)
fix a f
assume "a ∈ 𝒱 F"
hence "a ∈ 𝒱 (ideal F)" by simp
assume "f ∈ √ideal F"
then obtain m where "f ^ m ∈ ideal F" by (rule radicalE)
with ‹a ∈ 𝒱 (ideal F)› have "poly_eval a (f ^ m) = 0" by (rule variety_ofD)
thus "poly_eval a f = 0" by (simp add: poly_eval_power)
qed
qed
lemma image_map_indets_radical:
assumes "inj f"
shows "map_indets f ` √F = √(map_indets f ` (F::(_ ⇒⇩0 'a::comm_ring_1) set)) ∩ P[range f]"
proof
show "map_indets f ` √F ⊆ √(map_indets f ` F) ∩ P[range f]"
by (auto simp: radical_def simp flip: map_indets_power range_map_indets intro!: imageI)
next
show "√(map_indets f ` F) ∩ P[range f] ⊆ map_indets f ` √F"
proof
fix p
assume "p ∈ √(map_indets f ` F) ∩ P[range f]"
hence "p ∈ √(map_indets f ` F)" and "p ∈ range (map_indets f)"
by (simp_all add: range_map_indets)
from this(1) obtain m where "p ^ m ∈ map_indets f ` F" by (rule radicalE)
then obtain q where "q ∈ F" and p_m: "p ^ m = map_indets f q" ..
from assms obtain g where "g ∘ f = id" and "map_indets g ∘ map_indets f = (id::_ ⇒ _ ⇒⇩0 'a)"
by (rule map_indets_inverseE)
hence eq: "map_indets g (map_indets f p') = p'" for p'::"_ ⇒⇩0 'a"
by (simp add: pointfree_idE)
from p_m have "map_indets g (p ^ m) = map_indets g (map_indets f q)" by (rule arg_cong)
hence "(map_indets g p) ^ m = q" by (simp add: eq)
from ‹p ∈ range _› obtain p' where "p = map_indets f p'" ..
hence "p = map_indets f (map_indets g p)" by (simp add: eq)
moreover have "map_indets g p ∈ √F"
proof (rule radicalI)
from ‹q ∈ F› show "map_indets g p ^ m ∈ F" by (simp add: p_m eq flip: map_indets_power)
qed
ultimately show "p ∈ map_indets f ` √F" by (rule image_eqI)
qed
qed
subsection ‹Geometric Version of the Nullstellensatz›
lemma weak_Nullstellensatz_aux_1:
assumes "⋀i. i ∈ I ⟹ g i ∈ ideal B"
obtains c where "c ∈ ideal B" and "(∏i∈I. (f i + g i) ^ m i) = (∏i∈I. f i ^ m i) + c"
using assms
proof (induct I arbitrary: thesis rule: infinite_finite_induct)
case (infinite I)
from ideal.span_zero show ?case by (rule infinite) (simp add: infinite(1))
next
case empty
from ideal.span_zero show ?case by (rule empty) simp
next
case (insert j I)
have "g i ∈ ideal B" if "i ∈ I" for i by (rule insert.prems) (simp add: that)
with insert.hyps(3) obtain c where c: "c ∈ ideal B"
and 1: "(∏i∈I. (f i + g i) ^ m i) = (∏i∈I. f i ^ m i) + c" by blast
define k where "k = m j"
obtain d where 2: "(f j + g j) ^ m j = f j ^ m j + d * g j" unfolding k_def[symmetric]
proof (induct k arbitrary: thesis)
case 0
have "(f j + g j) ^ 0 = f j ^ 0 + 0 * g j" by simp
thus ?case by (rule 0)
next
case (Suc k)
obtain d where "(f j + g j) ^ k = f j ^ k + d * g j" by (rule Suc.hyps)
hence "(f j + g j) ^ Suc k = (f j ^ k + d * g j) * (f j + g j)" by simp
also have "… = f j ^ Suc k + (f j ^ k + d * (f j + g j)) * g j" by (simp add: algebra_simps)
finally show ?case by (rule Suc.prems)
qed
from c have *: "f j ^ m j * c + (((∏i∈I. f i ^ m i) + c) * d) * g j ∈ ideal B" (is "?c ∈ _")
by (intro ideal.span_add ideal.span_scale insert.prems insertI1)
from insert.hyps(1, 2) have "(∏i∈insert j I. (f i + g i) ^ m i) =
(f j ^ m j + d * g j) * ((∏i∈I. f i ^ m i) + c)"
by (simp add: 1 2)
also from insert.hyps(1, 2) have "… = (∏i∈insert j I. f i ^ m i) + ?c" by (simp add: algebra_simps)
finally have "(∏i∈insert j I. (f i + g i) ^ m i) = (∏i∈insert j I. f i ^ m i) + ?c" .
with * show ?case by (rule insert.prems)
qed
lemma weak_Nullstellensatz_aux_2:
assumes "finite X" and "F ⊆ P[insert x X]" and "X ⊆ {..<x::'x::{countable,linorder}}"
and "1 ∉ ideal F" and "ideal F ∩ P[{x}] ⊆ {0}"
obtains a::"'a::alg_closed_field" where "1 ∉ ideal (poly_eval (λ_. monomial a 0) ` focus {x} ` F)"
proof -
let ?x = "monomial 1 (Poly_Mapping.single x 1)"
from assms(3) have "x ∉ X" by blast
hence eq1: "insert x X - {x} = X" and eq2: "insert x X - X = {x}" by blast+
interpret i: pm_powerprod lex_pm "lex_pm_strict::('x ⇒⇩0 nat) ⇒ _"
unfolding lex_pm_def lex_pm_strict_def
by standard (simp_all add: lex_pm_zero_min lex_pm_plus_monotone flip: lex_pm_def)
have lpp_focus: "i.lpp (focus X g) = except (i.lpp g) {x}" if "g ∈ P[insert x X]" for g::"_ ⇒⇩0 'a"
proof (cases "g = 0")
case True
thus ?thesis by simp
next
case False
have keys_focus_g: "keys (focus X g) = (λt. except t {x}) ` keys g"
unfolding keys_focus using refl
proof (rule image_cong)
fix t
assume "t ∈ keys g"
also from that have "… ⊆ .[insert x X]" by (rule PolysD)
finally have "keys t ⊆ insert x X" by (rule PPsD)
hence "except t (- X) = except t (insert x X ∩ - X)"
by (metis (no_types, lifting) Int_commute except_keys_Int inf.orderE inf_left_commute)
also from ‹x ∉ X› have "insert x X ∩ - X = {x}" by simp
finally show "except t (- X) = except t {x}" .
qed
show ?thesis
proof (rule i.punit.lt_eqI_keys)
from False have "i.lpp g ∈ keys g" by (rule i.punit.lt_in_keys)
thus "except (i.lpp g) {x} ∈ keys (focus X g)" unfolding keys_focus_g by (rule imageI)
fix t
assume "t ∈ keys (focus X g)"
then obtain s where "s ∈ keys g" and t: "t = except s {x}" unfolding keys_focus_g ..
from this(1) have "lex_pm s (i.lpp g)" by (rule i.punit.lt_max_keys)
moreover have "keys s ∪ keys (i.lpp g) ⊆ {..x}"
proof (rule Un_least)
from ‹g ∈ P[_]› have "keys g ⊆ .[insert x X]" by (rule PolysD)
with ‹s ∈ keys g› have "s ∈ .[insert x X]" ..
hence "keys s ⊆ insert x X" by (rule PPsD)
thus "keys s ⊆ {..x}" using assms(3) by auto
from ‹i.lpp g ∈ keys g› ‹keys g ⊆ _› have "i.lpp g ∈ .[insert x X]" ..
hence "keys (i.lpp g) ⊆ insert x X" by (rule PPsD)
thus "keys (i.lpp g) ⊆ {..x}" using assms(3) by auto
qed
ultimately show "lex_pm t (except (i.lpp g) {x})" unfolding t by (rule lex_pm_except_max)
qed
qed
define G where "G = i.punit.reduced_GB F"
from assms(1) have "finite (insert x X)" by simp
hence fin_G: "finite G" and G_sub: "G ⊆ P[insert x X]" and ideal_G: "ideal G = ideal F"
and "0 ∉ G" and G_isGB: "i.punit.is_Groebner_basis G" unfolding G_def using assms(2)
by (rule i.finite_reduced_GB_Polys, rule i.reduced_GB_Polys, rule i.reduced_GB_ideal_Polys,
rule i.reduced_GB_nonzero_Polys, rule i.reduced_GB_is_GB_Polys)
define G' where "G' = focus X ` G"
from fin_G ‹0 ∉ G› have fin_G': "finite G'" and "0 ∉ G'" by (auto simp: G'_def)
have G'_sub: "G' ⊆ P[X]" by (auto simp: G'_def intro: focus_in_Polys)
define G'' where "G'' = i.lcf ` G'"
from ‹0 ∉ G'› have "0 ∉ G''" by (auto simp: G''_def i.punit.lc_eq_zero_iff)
have lookup_focus_in: "lookup (focus X g) t ∈ P[{x}]" if "g ∈ G" for g t
proof -
have "lookup (focus X g) t ∈ range (lookup (focus X g))" by (rule rangeI)
from that G_sub have "g ∈ P[insert x X]" ..
hence "range (lookup (focus X g)) ⊆ P[insert x X - X]" by (rule focus_coeffs_subset_Polys')
with ‹_ ∈ range _› have "lookup (focus X g) t ∈ P[insert x X - X]" ..
also have "insert x X - X = {x}" by (simp only: eq2)
finally show ?thesis .
qed
hence lcf_in: "i.lcf (focus X g) ∈ P[{x}]" if "g ∈ G" for g
unfolding i.punit.lc_def using that by blast
have G''_sub: "G'' ⊆ P[{x}]"
proof
fix c
assume "c ∈ G''"
then obtain g' where "g' ∈ G'" and c: "c = i.lcf g'" unfolding G''_def ..
from ‹g' ∈ G'› obtain g where "g ∈ G" and g': "g' = focus X g" unfolding G'_def ..
from this(1) show "c ∈ P[{x}]" unfolding c g' by (rule lcf_in)
qed
define P where "P = poly_of_pm x ` G''"
from fin_G' have fin_P: "finite P" by (simp add: P_def G''_def)
have "0 ∉ P"
proof
assume "0 ∈ P"
then obtain g'' where "g'' ∈ G''" and "0 = poly_of_pm x g''" unfolding P_def ..
from this(2) have *: "keys g'' ∩ .[{x}] = {}" by (simp add: poly_of_pm_eq_zero_iff)
from ‹g'' ∈ G''› G''_sub have "g'' ∈ P[{x}]" ..
hence "keys g'' ⊆ .[{x}]" by (rule PolysD)
with * have "keys g'' = {}" by blast
with ‹g'' ∈ G''› ‹0 ∉ G''› show False by simp
qed
define Z where "Z = (⋃p∈P. {z. poly p z = 0})"
have "finite Z" unfolding Z_def using fin_P
proof (rule finite_UN_I)
fix p
assume "p ∈ P"
with ‹0 ∉ P› have "p ≠ 0" by blast
thus "finite {z. poly p z = 0}" by (rule poly_roots_finite)
qed
with infinite_UNIV[where 'a='a] have "- Z ≠ {}" using finite_compl by fastforce
then obtain a where "a ∉ Z" by blast
have a_nz: "poly_eval (λ_. a) (i.lcf (focus X g)) ≠ 0" if "g ∈ G" for g
proof -
from that G_sub have "g ∈ P[insert x X]" ..
have "poly_eval (λ_. a) (i.lcf (focus X g)) = poly (poly_of_pm x (i.lcf (focus X g))) a"
by (rule sym, intro poly_eq_poly_eval' lcf_in that)
moreover have "poly_of_pm x (i.lcf (focus X g)) ∈ P"
by (auto simp: P_def G''_def G'_def that intro!: imageI)
ultimately show ?thesis using ‹a ∉ Z› by (simp add: Z_def)
qed
let ?e = "poly_eval (λ_. monomial a 0)"
have lookup_e_focus: "lookup (?e (focus {x} g)) t = poly_eval (λ_. a) (lookup (focus X g) t)"
if "g ∈ P[insert x X]" for g t
proof -
have "focus (- {x}) g = focus (- {x} ∩ insert x X) g" by (rule sym) (rule focus_Int, fact)
also have "… = focus X g" by (simp add: Int_commute eq1 flip: Diff_eq)
finally show ?thesis by (simp add: lookup_poly_eval_focus)
qed
have lpp_e_focus: "i.lpp (?e (focus {x} g)) = except (i.lpp g) {x}" if "g ∈ G" for g
proof (rule i.punit.lt_eqI_keys)
from that G_sub have "g ∈ P[insert x X]" ..
hence "lookup (?e (focus {x} g)) (except (i.lpp g) {x}) = poly_eval (λ_. a) (i.lcf (focus X g))"
by (simp only: lookup_e_focus lpp_focus i.punit.lc_def)
also from that have "… ≠ 0" by (rule a_nz)
finally show "except (i.lpp g) {x} ∈ keys (?e (focus {x} g))" by (simp add: in_keys_iff)
fix t
assume "t ∈ keys (?e (focus {x} g))"
hence "0 ≠ lookup (?e (focus {x} g)) t" by (simp add: in_keys_iff)
also from ‹g ∈ P[_]› have "lookup (?e (focus {x} g)) t = poly_eval (λ_. a) (lookup (focus X g) t)"
by (rule lookup_e_focus)
finally have "t ∈ keys (focus X g)" by (auto simp flip: lookup_not_eq_zero_eq_in_keys)
hence "lex_pm t (i.lpp (focus X g))" by (rule i.punit.lt_max_keys)
with ‹g ∈ P[_]› show "lex_pm t (except (i.lpp g) {x})" by (simp only: lpp_focus)
qed
show ?thesis
proof
define G3 where "G3 = ?e ` focus {x} ` G"
have "G3 ⊆ P[X]"
proof
fix h
assume "h ∈ G3"
then obtain h0 where "h0 ∈ G" and h: "h = ?e (focus {x} h0)" by (auto simp: G3_def)
from this(1) G_sub have "h0 ∈ P[insert x X]" ..
hence "h ∈ P[insert x X - {x}]" unfolding h by (rule poly_eval_focus_in_Polys)
thus "h ∈ P[X]" by (simp only: eq1)
qed
from fin_G have "finite G3" by (simp add: G3_def)
have "ideal G3 ∩ P[- {x}] = ?e ` focus {x} ` ideal G"
by (simp only: G3_def image_poly_eval_focus_ideal)
also have "… = ideal (?e ` focus {x} ` F) ∩ P[- {x}]"
by (simp only: ideal_G image_poly_eval_focus_ideal)
finally have eq3: "ideal G3 ∩ P[- {x}] = ideal (?e ` focus {x} ` F) ∩ P[- {x}]" .
from assms(1) ‹G3 ⊆ P[X]› ‹finite G3› have G3_isGB: "i.punit.is_Groebner_basis G3"
proof (rule i.punit.isGB_I_spoly_rep[simplified, OF dickson_grading_varnum,
where m=0, simplified i.dgrad_p_set_varnum])
fix g1 g2
assume "g1 ∈ G3"
then obtain g1' where "g1' ∈ G" and g1: "g1 = ?e (focus {x} g1')"
unfolding G3_def by blast
from this(1) have lpp1: "i.lpp g1 = except (i.lpp g1') {x}" unfolding g1 by (rule lpp_e_focus)
from ‹g1' ∈ G› G_sub have "g1' ∈ P[insert x X]" ..
assume "g2 ∈ G3"
then obtain g2' where "g2' ∈ G" and g2: "g2 = ?e (focus {x} g2')"
unfolding G3_def by blast
from this(1) have lpp2: "i.lpp g2 = except (i.lpp g2') {x}" unfolding g2 by (rule lpp_e_focus)
from ‹g2' ∈ G› G_sub have "g2' ∈ P[insert x X]" ..
define l where "l = lcs (except (i.lpp g1') {x}) (except (i.lpp g2') {x})"
define c1 where "c1 = i.lcf (focus X g1')"
define c2 where "c2 = i.lcf (focus X g2')"
define c where "c = poly_eval (λ_. a) c1 * poly_eval (λ_. a) c2"
define s where "s = c2 * punit.monom_mult 1 (l - except (i.lpp g1') {x}) g1' -
c1 * punit.monom_mult 1 (l - except (i.lpp g2') {x}) g2'"
have "c1 ∈ P[{x}]" unfolding c1_def using ‹g1' ∈ G› by (rule lcf_in)
hence eval_c1: "poly_eval (λ_. monomial a 0) (focus {x} c1) = monomial (poly_eval (λ_. a) c1) 0"
by (simp add: focus_Polys poly_eval_sum poly_eval_monomial monomial_power_map_scale
times_monomial_monomial flip: punit.monomial_prod_sum monomial_sum)
(simp add: poly_eval_alt)
have "c2 ∈ P[{x}]" unfolding c2_def using ‹g2' ∈ G› by (rule lcf_in)
hence eval_c2: "poly_eval (λ_. monomial a 0) (focus {x} c2) = monomial (poly_eval (λ_. a) c2) 0"
by (simp add: focus_Polys poly_eval_sum poly_eval_monomial monomial_power_map_scale
times_monomial_monomial flip: punit.monomial_prod_sum monomial_sum)
(simp add: poly_eval_alt)
assume spoly_nz: "i.punit.spoly g1 g2 ≠ 0"
assume "g1 ≠ 0" and "g2 ≠ 0"
hence "g1' ≠ 0" and "g2' ≠ 0" by (auto simp: g1 g2)
have c1_nz: "poly_eval (λ_. a) c1 ≠ 0" unfolding c1_def using ‹g1' ∈ G› by (rule a_nz)
moreover have c2_nz: "poly_eval (λ_. a) c2 ≠ 0" unfolding c2_def using ‹g2' ∈ G› by (rule a_nz)
ultimately have "c ≠ 0" by (simp add: c_def)
hence "inverse c ≠ 0" by simp
from ‹g1' ∈ P[_]› have "except (i.lpp g1') {x} ∈ .[insert x X - {x}]"
by (intro PPs_closed_except' i.PPs_closed_lpp)
moreover from ‹g2' ∈ P[_]› have "except (i.lpp g2') {x} ∈ .[insert x X - {x}]"
by (intro PPs_closed_except' i.PPs_closed_lpp)
ultimately have "l ∈ .[insert x X - {x}]" unfolding l_def by (rule PPs_closed_lcs)
hence "l ∈ .[X]" by (simp only: eq1)
hence "l ∈ .[insert x X]" by rule (rule PPs_mono, blast)
moreover from ‹c1 ∈ P[{x}]› have "c1 ∈ P[insert x X]" by rule (intro Polys_mono, simp)
moreover from ‹c2 ∈ P[{x}]› have "c2 ∈ P[insert x X]" by rule (intro Polys_mono, simp)
ultimately have "s ∈ P[insert x X]" using ‹g1' ∈ P[_]› ‹g2' ∈ P[_]› unfolding s_def
by (intro Polys_closed_minus Polys_closed_times Polys_closed_monom_mult PPs_closed_minus)
have "s ∈ ideal G" unfolding s_def times_monomial_left[symmetric]
by (intro ideal.span_diff ideal.span_scale ideal.span_base ‹g1' ∈ G› ‹g2' ∈ G›)
with G_isGB have "(i.punit.red G)⇧*⇧* s 0" by (rule i.punit.GB_imp_zero_reducibility[simplified])
with ‹finite (insert x X)› G_sub fin_G ‹s ∈ P[_]›
obtain q0 where 1: "s = 0 + (∑g∈G. q0 g * g)" and 2: "⋀g. q0 g ∈ P[insert x X]"
and 3: "⋀g. lex_pm (i.lpp (q0 g * g)) (i.lpp s)"
by (rule i.punit.red_rtrancl_repE[simplified, OF dickson_grading_varnum, where m=0,
simplified i.dgrad_p_set_varnum]) blast
define q where "q = (λg. inverse c ⋅ (∑h∈{y∈G. ?e (focus {x} y) = g}. ?e (focus {x} (q0 h))))"
have eq4: "?e (focus {x} (monomial 1 (l - t))) = monomial 1 (l - t)" for t
proof -
have "focus {x} (monomial (1::'a) (l - t)) = monomial (monomial 1 (l - t)) 0"
proof (intro focus_Polys_Compl Polys_closed_monomial PPs_closed_minus)
from ‹x ∉ X› have "X ⊆ - {x}" by simp
hence ".[X] ⊆ .[- {x}]" by (rule PPs_mono)
with ‹l ∈ .[X]› show "l ∈ .[- {x}]" ..
qed
thus ?thesis by (simp add: poly_eval_monomial)
qed
from c2_nz have eq5: "inverse c * poly_eval (λ_. a) c2 = 1 / lookup g1 (i.lpp g1)"
unfolding lpp1 using ‹g1' ∈ P[_]›
by (simp add: c_def mult.assoc divide_inverse_commute g1 lookup_e_focus
flip: lpp_focus i.punit.lc_def c1_def)
from c1_nz have eq6: "inverse c * poly_eval (λ_. a) c1 = 1 / lookup g2 (i.lpp g2)"
unfolding lpp2 using ‹g2' ∈ P[_]›
by (simp add: c_def mult.assoc mult.left_commute[of "inverse (poly_eval (λ_. a) c1)"]
divide_inverse_commute g2 lookup_e_focus flip: lpp_focus i.punit.lc_def c2_def)
have l_alt: "l = lcs (i.lpp g1) (i.lpp g2)" by (simp only: l_def lpp1 lpp2)
have spoly_eq: "i.punit.spoly g1 g2 = (inverse c) ⋅ ?e (focus {x} s)"
by (simp add: s_def focus_minus focus_times poly_eval_minus poly_eval_times eval_c1 eval_c2
eq4 eq5 eq6 map_scale_eq_times times_monomial_monomial right_diff_distrib
i.punit.spoly_def Let_def
flip: mult.assoc times_monomial_left g1 g2 lpp1 lpp2 l_alt)
also have "… = (∑g∈G. inverse c ⋅ (?e (focus {x} (q0 g)) * ?e (focus {x} g)))"
by (simp add: 1 focus_sum poly_eval_sum focus_times poly_eval_times map_scale_sum_distrib_left)
also have "… = (∑g∈G3. ∑h∈{y∈G. ?e (focus{x} y) = g}.
inverse c ⋅ (?e (focus {x} (q0 h)) * ?e (focus {x} h)))"
unfolding G3_def image_image using fin_G by (rule sum.image_gen)
also have "… = (∑g∈G3. inverse c ⋅ (∑h∈{y∈G. ?e (focus{x} y) = g}. ?e (focus {x} (q0 h))) * g)"
by (intro sum.cong refl) (simp add: map_scale_eq_times sum_distrib_left sum_distrib_right mult.assoc)
also from refl have "… = (∑g∈G3. q g * g)" by (rule sum.cong) (simp add: q_def sum_distrib_right)
finally have "i.punit.spoly g1 g2 = (∑g∈G3. q g * g)" .
thus "i.punit.spoly_rep (varnum X) 0 G3 g1 g2"
proof (rule i.punit.spoly_repI[simplified, where m=0 and d="varnum X",
simplified i.dgrad_p_set_varnum])
fix g
show "q g ∈ P[X]" unfolding q_def
proof (intro Polys_closed_map_scale Polys_closed_sum)
fix g0
from ‹q0 g0 ∈ P[insert x X]› have "?e (focus {x} (q0 g0)) ∈ P[insert x X - {x}]"
by (rule poly_eval_focus_in_Polys)
thus "?e (focus {x} (q0 g0)) ∈ P[X]" by (simp only: eq1)
qed
assume "q g ≠ 0 ∧ g ≠ 0"
hence "q g ≠ 0" ..
have "i.lpp (q g * g) = i.lpp (∑h∈{y∈G. ?e (focus {x} y) = g}. inverse c ⋅ ?e (focus {x} (q0 h)) * g)"
by (simp add: q_def map_scale_sum_distrib_left sum_distrib_right)
also have "lex_pm … (i.ordered_powerprod_lin.Max
{i.lpp (inverse c ⋅ ?e (focus {x} (q0 h)) * g) | h. h ∈ {y∈G. ?e (focus {x} y) = g}})"
(is "lex_pm _ (i.ordered_powerprod_lin.Max ?A)") by (fact i.punit.lt_sum_le_Max)
also have "lex_pm … (i.lpp s)"
proof (rule i.ordered_powerprod_lin.Max.boundedI)
from fin_G show "finite ?A" by simp
next
show "?A ≠ {}"
proof
assume "?A = {}"
hence "{h ∈ G. ?e (focus {x} h) = g} = {}" by simp
hence "q g = 0" by (simp only: q_def sum.empty map_scale_zero_right)
with ‹q g ≠ 0› show False ..
qed
next
fix t
assume "t ∈ ?A"
then obtain h where "h ∈ G" and g[symmetric]: "?e (focus {x} h) = g"
and "t = i.lpp (inverse c ⋅ ?e (focus {x} (q0 h)) * g)" by blast
note this(3)
also have "i.lpp (inverse c ⋅ ?e (focus {x} (q0 h)) * g) =
i.lpp (inverse c ⋅ (?e (focus {x} (q0 h * h))))"
by (simp only: map_scale_eq_times mult.assoc g poly_eval_times focus_times)
also from ‹inverse c ≠ 0› have "… = i.lpp (?e (focus {x} (q0 h * h)))"
by (rule i.punit.lt_map_scale)
also have "lex_pm … (i.lpp (q0 h * h))"
proof (rule i.punit.lt_le, rule ccontr)
fix u
assume "lookup (?e (focus {x} (q0 h * h))) u ≠ 0"
hence "u ∈ keys (?e (focus {x} (q0 h * h)))" by (simp add: in_keys_iff)
with keys_poly_eval_focus_subset have "u ∈ (λv. except v {x}) ` keys (q0 h * h)" ..
then obtain v where "v ∈ keys (q0 h * h)" and u: "u = except v {x}" ..
have "lex_pm u (Poly_Mapping.single x (lookup v x) + u)"
by (metis add.commute add.right_neutral i.plus_monotone_left lex_pm_zero_min)
also have "… = v" by (simp only: u flip: plus_except)
also from ‹v ∈ _› have "lex_pm v (i.lpp (q0 h * h))" by (rule i.punit.lt_max_keys)
finally have "lex_pm u (i.lpp (q0 h * h))" .
moreover assume "lex_pm_strict (i.lpp (q0 h * h)) u"
ultimately show False by simp
qed
also have "lex_pm … (i.lpp s)" by fact
finally show "lex_pm t (i.lpp s)" .
qed
also have "lex_pm_strict … l"
proof (rule i.punit.lt_less)
from spoly_nz show "s ≠ 0" by (auto simp: spoly_eq)
next
fix t
assume "lex_pm l t"
have "g1' = flatten (focus X g1')" by simp
also have "… = flatten (monomial c1 (i.lpp (focus X g1')) + i.punit.tail (focus X g1'))"
by (simp only: c1_def flip: i.punit.leading_monomial_tail)
also from ‹g1' ∈ P[_]› have "… = punit.monom_mult 1 (except (i.lpp g1') {x}) c1 +
flatten (i.punit.tail (focus X g1'))"
by (simp only: flatten_plus flatten_monomial lpp_focus)
finally have "punit.monom_mult 1 (except (i.lpp g1') {x}) c1 +
flatten (i.punit.tail (focus X g1')) = g1'" (is "?l = _") by (rule sym)
moreover have "c2 * punit.monom_mult 1 (l - except (i.lpp g1') {x}) ?l =
punit.monom_mult 1 l (c1 * c2) +
c2 * punit.monom_mult 1 (l - i.lpp (focus X g1'))
(flatten (i.punit.tail (focus X g1')))"
(is "_ = punit.monom_mult 1 l (c1 * c2) + ?a")
by (simp add: punit.monom_mult_dist_right punit.monom_mult_assoc l_def minus_plus adds_lcs)
(simp add: distrib_left lpp_focus ‹g1' ∈ P[_]› flip: times_monomial_left)
ultimately have a: "c2 * punit.monom_mult 1 (l - except (i.lpp g1') {x}) g1' =
punit.monom_mult 1 l (c1 * c2) + ?a" by simp
have "g2' = flatten (focus X g2')" by simp
also have "… = flatten (monomial c2 (i.lpp (focus X g2')) + i.punit.tail (focus X g2'))"
by (simp only: c2_def flip: i.punit.leading_monomial_tail)
also from ‹g2' ∈ P[_]› have "… = punit.monom_mult 1 (except (i.lpp g2') {x}) c2 +
flatten (i.punit.tail (focus X g2'))"
by (simp only: flatten_plus flatten_monomial lpp_focus)
finally have "punit.monom_mult 1 (except (i.lpp g2') {x}) c2 +
flatten (i.punit.tail (focus X g2')) = g2'" (is "?l = _") by (rule sym)
moreover have "c1 * punit.monom_mult 1 (l - except (i.lpp g2') {x}) ?l =
punit.monom_mult 1 l (c1 * c2) +
c1 * punit.monom_mult 1 (l - i.lpp (focus X g2'))
(flatten (i.punit.tail (focus X g2')))"
(is "_ = punit.monom_mult 1 l (c1 * c2) + ?b")
by (simp add: punit.monom_mult_dist_right punit.monom_mult_assoc l_def minus_plus adds_lcs_2)
(simp add: distrib_left lpp_focus ‹g2' ∈ P[_]› flip: times_monomial_left)
ultimately have b: "c1 * punit.monom_mult 1 (l - except (i.lpp g2') {x}) g2' =
punit.monom_mult 1 l (c1 * c2) + ?b" by simp
have lex_pm_strict_t: "lex_pm_strict t (l - i.lpp (focus X h) + i.lpp (focus X h))"
if "t ∈ keys (d * punit.monom_mult 1 (l - i.lpp (focus X h))
(flatten (i.punit.tail (focus X h))))"
and "h ∈ G" and "d ∈ P[{x}]" for d h
proof -
have 0: "lex_pm_strict (u + v) w" if "lex_pm_strict v w" and "w ∈ .[X]" and "u ∈ .[{x}]"
for u v w using that(1)
proof (rule lex_pm_strict_plus_left)
fix y z
assume "y ∈ keys w"
also from that(2) have "… ⊆ X" by (rule PPsD)
also have "… ⊆ {..<x}" by fact
finally have "y < x" by simp
assume "z ∈ keys u"
also from that(3) have "… ⊆ {x}" by (rule PPsD)
finally show "y < z" using ‹y < x› by simp
qed
let ?h = "focus X h"
from that(2) have "?h ∈ G'" by (simp add: G'_def)
with ‹G' ⊆ P[X]› have "?h ∈ P[X]" ..
hence "i.lpp ?h ∈ .[X]" by (rule i.PPs_closed_lpp)
from that(1) obtain t1 t2 where "t1 ∈ keys d"
and "t2 ∈ keys (punit.monom_mult 1 (l - i.lpp ?h) (flatten (i.punit.tail ?h)))"
and t: "t = t1 + t2" by (rule in_keys_timesE)
from this(2) obtain t3 where "t3 ∈ keys (flatten (i.punit.tail ?h))"
and t2: "t2 = l - i.lpp ?h + t3" by (auto simp: punit.keys_monom_mult)
from this(1) obtain t4 t5 where "t4 ∈ keys (i.punit.tail ?h)"
and t5_in: "t5 ∈ keys (lookup (i.punit.tail ?h) t4)" and t3: "t3 = t4 + t5"
using keys_flatten_subset by blast
from this(1) have 1: "lex_pm_strict t4 (i.lpp ?h)" by (rule i.punit.keys_tail_less_lt)
from that(2) have "lookup ?h t4 ∈ P[{x}]" by (rule lookup_focus_in)
hence "keys (lookup ?h t4) ⊆ .[{x}]" by (rule PolysD)
moreover from t5_in have t5_in: "t5 ∈ keys (lookup ?h t4)"
by (simp add: i.punit.lookup_tail split: if_split_asm)
ultimately have "t5 ∈ .[{x}]" ..
with 1 ‹i.lpp ?h ∈ _› have "lex_pm_strict (t5 + t4) (i.lpp ?h)" by (rule 0)
hence "lex_pm_strict t3 (i.lpp ?h)" by (simp only: t3 add.commute)
hence "lex_pm_strict t2 (l - i.lpp ?h + i.lpp ?h)" unfolding t2
by (rule i.plus_monotone_strict_left)
moreover from ‹l ∈ .[X]› ‹i.lpp ?h ∈ .[X]› have "l - i.lpp ?h + i.lpp ?h ∈ .[X]"
by (intro PPs_closed_plus PPs_closed_minus)
moreover from ‹t1 ∈ keys d› that(3) have "t1 ∈ .[{x}]" by (auto dest: PolysD)
ultimately show ?thesis unfolding t by (rule 0)
qed
show "lookup s t = 0"
proof (rule ccontr)
assume "lookup s t ≠ 0"
hence "t ∈ keys s" by (simp add: in_keys_iff)
also have "… = keys (?a - ?b)" by (simp add: s_def a b)
also have "… ⊆ keys ?a ∪ keys ?b" by (fact keys_minus)
finally show False
proof
assume "t ∈ keys ?a"
hence "lex_pm_strict t (l - i.lpp (focus X g1') + i.lpp (focus X g1'))"
using ‹g1' ∈ G› ‹c2 ∈ P[{x}]› by (rule lex_pm_strict_t)
with ‹g1' ∈ P[_]› have "lex_pm_strict t l"
by (simp add: lpp_focus l_def minus_plus adds_lcs)
with ‹lex_pm l t› show ?thesis by simp
next
assume "t ∈ keys ?b"
hence "lex_pm_strict t (l - i.lpp (focus X g2') + i.lpp (focus X g2'))"
using ‹g2' ∈ G› ‹c1 ∈ P[{x}]› by (rule lex_pm_strict_t)
with ‹g2' ∈ P[_]› have "lex_pm_strict t l"
by (simp add: lpp_focus l_def minus_plus adds_lcs_2)
with ‹lex_pm l t› show ?thesis by simp
qed
qed
qed
also have "… = lcs (i.lpp g1) (i.lpp g2)" by (simp only: l_def lpp1 lpp2)
finally show "lex_pm_strict (i.lpp (q g * g)) (lcs (i.lpp g1) (i.lpp g2))" .
qed
qed
have "1 ∈ ideal (?e ` focus {x} ` F) ⟷ 1 ∈ ideal (?e ` focus {x} ` F) ∩ P[- {x}]"
by (simp add: one_in_Polys)
also have "… ⟷ 1 ∈ ideal G3" by (simp add: one_in_Polys flip: eq3)
also have "¬ …"
proof
note G3_isGB
moreover assume "1 ∈ ideal G3"
moreover have "1 ≠ (0::_ ⇒⇩0 'a)" by simp
ultimately obtain g where "g ∈ G3" and "g ≠ 0" and "i.lpp g adds i.lpp (1::_ ⇒⇩0 'a)"
by (rule i.punit.GB_adds_lt[simplified])
from this(3) have "i.lpp g = 0" by (simp add: i.punit.lt_monomial adds_zero flip: single_one)
hence "monomial (i.lcf g) 0 = g" by (rule i.punit.lt_eq_min_term_monomial[simplified])
from ‹g ∈ G3› obtain g' where "g' ∈ G" and g: "g = ?e (focus {x} g')" by (auto simp: G3_def)
from this(1) have "i.lpp g = except (i.lpp g') {x}" unfolding g by (rule lpp_e_focus)
hence "keys (i.lpp g') ⊆ {x}" by (simp add: ‹i.lpp g = 0› except_eq_zero_iff)
have "g' ∈ P[{x}]"
proof (intro PolysI subsetI PPsI)
fix t y
assume "t ∈ keys g'"
hence "lex_pm t (i.lpp g')" by (rule i.punit.lt_max_keys)
moreover assume "y ∈ keys t"
ultimately obtain z where "z ∈ keys (i.lpp g')" and "z ≤ y" by (rule lex_pm_keys_leE)
with ‹keys (i.lpp g') ⊆ {x}› have "x ≤ y" by blast
from ‹g' ∈ G› G_sub have "g' ∈ P[insert x X]" ..
hence "indets g' ⊆ insert x X" by (rule PolysD)
moreover from ‹y ∈ _› ‹t ∈ _› have "y ∈ indets g'" by (rule in_indetsI)
ultimately have "y ∈ insert x X" ..
thus "y ∈ {x}"
proof
assume "y ∈ X"
with assms(3) have "y ∈ {..<x}" ..
with ‹x ≤ y› show ?thesis by simp
qed simp
qed
moreover from ‹g' ∈ G› have "g' ∈ ideal G" by (rule ideal.span_base)
ultimately have "g' ∈ ideal F ∩ P[{x}]" by (simp add: ideal_G)
with assms(5) have "g' = 0" by blast
hence "g = 0" by (simp add: g)
with ‹g ≠ 0› show False ..
qed
finally show "1 ∉ ideal (?e ` focus {x} ` F)" .
qed
qed
lemma weak_Nullstellensatz_aux_3:
assumes "F ⊆ P[insert x X]" and "x ∉ X" and "1 ∉ ideal F" and "¬ ideal F ∩ P[{x}] ⊆ {0}"
obtains a::"'a::alg_closed_field" where "1 ∉ ideal (poly_eval (λ_. monomial a 0) ` focus {x} ` F)"
proof -
let ?x = "monomial 1 (Poly_Mapping.single x 1)"
from assms(4) obtain f where "f ∈ ideal F" and "f ∈ P[{x}]" and "f ≠ 0" by blast
define p where "p = poly_of_pm x f"
from ‹f ∈ P[{x}]› ‹f ≠ 0› have "p ≠ 0"
by (auto simp: p_def poly_of_pm_eq_zero_iff simp flip: keys_eq_empty dest!: PolysD(1))
obtain c A m where A: "finite A" and p: "p = Polynomial.smult c (∏a∈A. [:- a, 1:] ^ m a)"
and "⋀x. m x = 0 ⟷ x ∉ A" and "c = 0 ⟷ p = 0" and "⋀z. poly p z = 0 ⟷ (c = 0 ∨ z ∈ A)"
by (rule linear_factorsE) blast
from this(4, 5) have "c ≠ 0" and "⋀z. poly p z = 0 ⟷ z ∈ A" by (simp_all add: ‹p ≠ 0›)
have "∃a∈A. 1 ∉ ideal (poly_eval (λ_. monomial a 0) ` focus {x} ` F)"
proof (rule ccontr)
assume asm: "¬ (∃a∈A. 1 ∉ ideal (poly_eval (λ_. monomial a 0) ` focus {x} ` F))"
obtain g h where "g a ∈ ideal F" and 1: "h a * (?x - monomial a 0) + g a = 1"
if "a ∈ A" for a
proof -
define P where "P = (λgh a. fst gh ∈ ideal F ∧ fst gh + snd gh * (?x - monomial a 0) = 1)"
define gh where "gh = (λa. SOME gh. P gh a)"
show ?thesis
proof
fix a
assume "a ∈ A"
with asm have "1 ∈ ideal (poly_eval (λ_. monomial a 0) ` focus {x} ` F)" by blast
hence "1 ∈ poly_eval (λ_. monomial a 0) ` focus {x} ` ideal F"
by (simp add: image_poly_eval_focus_ideal one_in_Polys)
then obtain g where "g ∈ ideal F" and "1 = poly_eval (λ_. monomial a 0) (focus {x} g)"
unfolding image_image ..
note this(2)
also have "poly_eval (λ_. monomial a 0) (focus {x} g) = poly (poly_of_focus x g) (monomial a 0)"
by (simp only: poly_poly_of_focus)
also have "… = poly (poly_of_focus x g) (?x - (?x - monomial a 0))" by simp
also obtain h where "… = poly (poly_of_focus x g) ?x - h * (?x - monomial a 0)"
by (rule poly_minus_rightE)
also have "… = g - h * (?x - monomial a 0)" by (simp only: poly_poly_of_focus_monomial)
finally have "g - h * (?x - monomial a 0) = 1" by (rule sym)
with ‹g ∈ ideal F› have "P (g, - h) a" by (simp add: P_def)
hence "P (gh a) a" unfolding gh_def by (rule someI)
thus "fst (gh a) ∈ ideal F" and "snd (gh a) * (?x - monomial a 0) + fst (gh a) = 1"
by (simp_all only: P_def add.commute)
qed
qed
from this(1) obtain g' where "g' ∈ ideal F"
and 2: "(∏a∈A. (h a * (?x - monomial a 0) + g a) ^ m a) =
(∏a∈A. (h a * (?x - monomial a 0)) ^ m a) + g'"
by (rule weak_Nullstellensatz_aux_1)
have "1 = (∏a∈A. (h a * (?x - monomial a 0) + g a) ^ m a)"
by (rule sym) (intro prod.neutral ballI, simp only: 1 power_one)
also have "… = (∏a∈A. h a ^ m a) * (∏a∈A. (?x - monomial a 0) ^ m a) + g'"
by (simp only: 2 power_mult_distrib prod.distrib)
also have "(∏a∈A. (?x - monomial a 0) ^ m a) = pm_of_poly x (∏a∈A. [:- a, 1:] ^ m a)"
by (simp add: pm_of_poly_prod pm_of_poly_pCons single_uminus punit.monom_mult_monomial
flip: single_one)
also from ‹c ≠ 0› have "… = monomial (inverse c) 0 * pm_of_poly x p"
by (simp add: p map_scale_assoc flip: map_scale_eq_times)
also from ‹f ∈ P[{x}]› have "… = monomial (inverse c) 0 * f"
by (simp only: ‹p = poly_of_pm x f› pm_of_poly_of_pm)
finally have "1 = ((∏a∈A. h a ^ m a) * monomial (inverse c) 0) * f + g'"
by (simp only: mult.assoc)
also from ‹f ∈ ideal F› ‹g' ∈ ideal F› have "… ∈ ideal F" by (intro ideal.span_add ideal.span_scale)
finally have "1 ∈ ideal F" .
with assms(3) show False ..
qed
then obtain a where "1 ∉ ideal (poly_eval (λ_. monomial a 0) ` focus {x} ` F)" ..
thus ?thesis ..
qed
theorem weak_Nullstellensatz:
assumes "finite X" and "F ⊆ P[X]" and "𝒱 F = ({}::('x::{countable,linorder} ⇒ 'a::alg_closed_field) set)"
shows "ideal F = UNIV"
unfolding ideal_eq_UNIV_iff_contains_one
proof (rule ccontr)
assume "1 ∉ ideal F"
with assms(1, 2) obtain a where "1 ∉ ideal (poly_eval a ` F)"
proof (induct X arbitrary: F thesis rule: finite_linorder_induct)
case empty
have "F ⊆ {0}"
proof
fix f
assume "f ∈ F"
with empty.prems(2) have "f ∈ P[{}]" ..
then obtain c where f: "f = monomial c 0" unfolding Polys_empty ..
also have "c = 0"
proof (rule ccontr)
assume "c ≠ 0"
from ‹f ∈ F› have "f ∈ ideal F" by (rule ideal.span_base)
hence "monomial (inverse c) 0 * f ∈ ideal F" by (rule ideal.span_scale)
with ‹c ≠ 0› have "1 ∈ ideal F" by (simp add: f times_monomial_monomial)
with empty.prems(3) show False ..
qed
finally show "f ∈ {0}" by simp
qed
hence "poly_eval 0 ` F ⊆ {0}" by auto
hence "ideal (poly_eval 0 ` F) = {0}" by simp
hence "1 ∉ ideal (poly_eval 0 ` F)" by (simp del: ideal_eq_zero_iff)
thus ?case by (rule empty.prems)
next
case (insert x X)
obtain a0 where "1 ∉ ideal (poly_eval (λ_. monomial a0 0) ` focus {x} ` F)" (is "_ ∉ ideal ?F")
proof (cases "ideal F ∩ P[{x}] ⊆ {0}")
case True
with insert.hyps(1) insert.prems(2) insert.hyps(2) insert.prems(3) obtain a0
where "1 ∉ ideal (poly_eval (λ_. monomial a0 0) ` focus {x} ` F)"
by (rule weak_Nullstellensatz_aux_2)
thus ?thesis ..
next
case False
from insert.hyps(2) have "x ∉ X" by blast
with insert.prems(2) obtain a0 where "1 ∉ ideal (poly_eval (λ_. monomial a0 0) ` focus {x} ` F)"
using insert.prems(3) False by (rule weak_Nullstellensatz_aux_3)
thus ?thesis ..
qed
moreover have "?F ⊆ P[X]"
proof -
{
fix f
assume "f ∈ F"
with insert.prems(2) have "f ∈ P[insert x X]" ..
hence "poly_eval (λ_. monomial a0 0) (focus {x} f) ∈ P[insert x X - {x}]"
by (rule poly_eval_focus_in_Polys)
also have "… ⊆ P[X]" by (rule Polys_mono) simp
finally have "poly_eval (λ_. monomial a0 0) (focus {x} f) ∈ P[X]" .
}
thus ?thesis by blast
qed
ultimately obtain a1 where "1 ∉ ideal (poly_eval a1 ` ?F)" using insert.hyps(3) by blast
also have "poly_eval a1 ` ?F = poly_eval (a1(x := poly_eval a1 (monomial a0 0))) ` F"
by (simp add: image_image poly_eval_poly_eval_focus fun_upd_def)
finally show ?case by (rule insert.prems)
qed
hence "ideal (poly_eval a ` F) ≠ UNIV" by (simp add: ideal_eq_UNIV_iff_contains_one)
hence "ideal (poly_eval a ` F) = {0}" using ideal_field_disj[of "poly_eval a ` F"] by blast
hence "poly_eval a ` F ⊆ {0}" by simp
hence "a ∈ 𝒱 F" by (rule variety_ofI_alt)
thus False by (simp add: assms(3))
qed
lemma radical_idealI:
assumes "finite X" and "F ⊆ P[X]" and "f ∈ P[X]" and "x ∉ X"
and "𝒱 (insert (1 - punit.monom_mult 1 (Poly_Mapping.single x 1) f) F) = {}"
shows "(f::('x::{countable,linorder} ⇒⇩0 nat) ⇒⇩0 'a::alg_closed_field) ∈ √ideal F"
proof (cases "f = 0")
case True
thus ?thesis by simp
next
case False
from assms(4) have "P[X] ⊆ P[- {x}]" by (auto simp: Polys_alt)
with assms(3) have "f ∈ P[- {x}]" ..
let ?x = "Poly_Mapping.single x 1"
let ?f = "punit.monom_mult 1 ?x f"
from assms(1) have "finite (insert x X)" by simp
moreover have "insert (1 - ?f) F ⊆ P[insert x X]" unfolding insert_subset
proof (intro conjI Polys_closed_minus one_in_Polys Polys_closed_monom_mult PPs_closed_single)
have "P[X] ⊆ P[insert x X]" by (rule Polys_mono) blast
with assms(2, 3) show "f ∈ P[insert x X]" and "F ⊆ P[insert x X]" by blast+
qed simp
ultimately have "ideal (insert (1 - ?f) F) = UNIV"
using assms(5) by (rule weak_Nullstellensatz)
hence "1 ∈ ideal (insert (1 - ?f) F)" by simp
then obtain F' q where fin': "finite F'" and F'_sub: "F' ⊆ insert (1 - ?f) F"
and eq: "1 = (∑f'∈F'. q f' * f')" by (rule ideal.spanE)
show "f ∈ √ideal F"
proof (cases "1 - ?f ∈ F'")
case True
define g where "g = (λx::('x ⇒⇩0 nat) ⇒⇩0 'a. Fract x 1)"
define F'' where "F'' = F' - {1 - ?f}"
define q0 where "q0 = q (1 - ?f)"
have g_0: "g 0 = 0" by (simp add: g_def fract_collapse)
have g_1: "g 1 = 1" by (simp add: g_def fract_collapse)
have g_plus: "g (a + b) = g a + g b" for a b by (simp add: g_def)
have g_minus: "g (a - b) = g a - g b" for a b by (simp add: g_def)
have g_times: "g (a * b) = g a * g b" for a b by (simp add: g_def)
from fin' have fin'': "finite F''" by (simp add: F''_def)
from F'_sub have F''_sub: "F'' ⊆ F" by (auto simp: F''_def)
have "focus {x} ?f = monomial 1 ?x * focus {x} f"
by (simp add: focus_times focus_monomial except_single flip: times_monomial_left)
also from ‹f ∈ P[- {x}]› have "focus {x} f = monomial f 0" by (rule focus_Polys_Compl)
finally have "focus {x} ?f = monomial f ?x" by (simp add: times_monomial_monomial)
hence eq1: "poly (map_poly g (poly_of_focus x (1 - ?f))) (Fract 1 f) = 0"
by (simp add: poly_of_focus_def focus_minus poly_of_pm_minus poly_of_pm_monomial
PPs_closed_single map_poly_minus g_0 g_1 g_minus map_poly_monom poly_monom)
(simp add: g_def Fract_same ‹f ≠ 0›)
have eq2: "poly (map_poly g (poly_of_focus x f')) (Fract 1 f) = Fract f' 1" if "f' ∈ F''" for f'
proof -
from that F''_sub have "f' ∈ F" ..
with assms(2) have "f' ∈ P[X]" ..
with ‹P[X] ⊆ _› have "f' ∈ P[- {x}]" ..
hence "focus {x} f' = monomial f' 0" by (rule focus_Polys_Compl)
thus ?thesis
by (simp add: poly_of_focus_def focus_minus poly_of_pm_minus poly_of_pm_monomial
zero_in_PPs map_poly_minus g_0 g_1 g_minus map_poly_monom poly_monom)
(simp only: g_def)
qed
define p0m0 where "p0m0 = (λf'. SOME z. poly (map_poly g (poly_of_focus x (q f'))) (Fract 1 f) =
Fract (fst z) (f ^ snd z))"
define p0 where "p0 = fst ∘ p0m0"
define m0 where "m0 = snd ∘ p0m0"
define m where "m = Max (m0 ` F'')"
have eq3: "poly (map_poly g (poly_of_focus x (q f'))) (Fract 1 f) = Fract (p0 f') (f ^ m0 f')"
for f'
proof -
have "g a = 0 ⟷ a = 0" for a by (simp add: g_def Fract_eq_zero_iff)
hence "set (Polynomial.coeffs (map_poly g (poly_of_focus x (q f')))) ⊆ range (λx. Fract x 1)"
by (auto simp: set_coeffs_map_poly g_def)
then obtain p m' where "poly (map_poly g (poly_of_focus x (q f'))) (Fract 1 f) = Fract p (f ^ m')"
by (rule poly_Fract)
hence "poly (map_poly g (poly_of_focus x (q f'))) (Fract 1 f) = Fract (fst (p, m')) (f ^ snd (p, m'))"
by simp
thus ?thesis unfolding p0_def m0_def p0m0_def o_def by (rule someI)
qed
note eq
also from True fin' have "(∑f'∈F'. q f' * f') = q0 * (1 - ?f) + (∑f'∈F''. q f' * f')"
by (simp add: q0_def F''_def sum.remove)
finally have "poly_of_focus x 1 = poly_of_focus x (q0 * (1 - ?f) + (∑f'∈F''. q f' * f'))"
by (rule arg_cong)
hence "1 = poly (map_poly g (poly_of_focus x (q0 * (1 - ?f) + (∑f'∈F''. q f' * f')))) (Fract 1 f)"
by (simp add: g_1)
also have "… = poly (map_poly g (poly_of_focus x (∑f'∈F''. q f' * f'))) (Fract 1 f)"
by (simp only: poly_of_focus_plus map_poly_plus g_0 g_plus g_times poly_add
poly_of_focus_times map_poly_times poly_mult eq1 mult_zero_right add_0_left)
also have "… = (∑f'∈F''. Fract (p0 f') (f ^ m0 f') * Fract f' 1)"
by (simp only: poly_of_focus_sum poly_of_focus_times map_poly_sum map_poly_times
g_0 g_plus g_times poly_sum poly_mult eq2 eq3 cong: sum.cong)
finally have "Fract (f ^ m) 1 = Fract (f ^ m) 1 * (∑f'∈F''. Fract (p0 f' * f') (f ^ m0 f'))"
by simp
also have "… = (∑f'∈F''. Fract (f ^ m * (p0 f' * f')) (f ^ m0 f'))"
by (simp add: sum_distrib_left)
also from refl have "… = (∑f'∈F''. Fract ((f ^ (m - m0 f') * p0 f') * f') 1)"
proof (rule sum.cong)
fix f'
assume "f' ∈ F''"
hence "m0 f' ∈ m0 ` F''" by (rule imageI)
with _ have "m0 f' ≤ m" unfolding m_def by (rule Max_ge) (simp add: fin'')
hence "f ^ m = f ^ (m0 f') * f ^ (m - m0 f')" by (simp flip: power_add)
hence "Fract (f ^ m * (p0 f' * f')) (f ^ m0 f') = Fract (f ^ m0 f') (f ^ m0 f') *
Fract (f ^ (m - m0 f') * (p0 f' * f')) 1"
by (simp add: ac_simps)
also from ‹f ≠ 0› have "Fract (f ^ m0 f') (f ^ m0 f') = 1" by (simp add: Fract_same)
finally show "Fract (f ^ m * (p0 f' * f')) (f ^ m0 f') = Fract (f ^ (m - m0 f') * p0 f' * f') 1"
by (simp add: ac_simps)
qed
also from fin'' have "… = Fract (∑f'∈F''. (f ^ (m - m0 f') * p0 f') * f') 1"
by (induct F'') (simp_all add: fract_collapse)
finally have "f ^ m = (∑f'∈F''. (f ^ (m - m0 f') * p0 f') * f')"
by (simp add: eq_fract)
also have "… ∈ ideal F''" by (rule ideal.sum_in_spanI)
also from ‹F'' ⊆ F› have "… ⊆ ideal F" by (rule ideal.span_mono)
finally show "f ∈ √ideal F" by (rule radicalI)
next
case False
with F'_sub have "F' ⊆ F" by blast
have "1 ∈ ideal F'" unfolding eq by (rule ideal.sum_in_spanI)
also from ‹F' ⊆ F› have "… ⊆ ideal F" by (rule ideal.span_mono)
finally have "ideal F = UNIV" by (simp only: ideal_eq_UNIV_iff_contains_one)
thus ?thesis by simp
qed
qed
corollary radical_idealI_extend_indets:
assumes "finite X" and "F ⊆ P[X]"
and "𝒱 (insert (1 - punit.monom_mult 1 (Poly_Mapping.single None 1) (extend_indets f))
(extend_indets ` F)) = {}"
shows "(f::(_::{countable,linorder} ⇒⇩0 nat) ⇒⇩0 _::alg_closed_field) ∈ √ideal F"
proof -
define Y where "Y = X ∪ indets f"
from assms(1) have fin_Y: "finite Y" by (simp add: Y_def finite_indets)
have "P[X] ⊆ P[Y]" by (rule Polys_mono) (simp add: Y_def)
with assms(2) have F_sub: "F ⊆ P[Y]" by (rule subset_trans)
have f_in: "f ∈ P[Y]" by (simp add: Y_def Polys_alt)
let ?F = "extend_indets ` F"
let ?f = "extend_indets f"
let ?X = "Some ` Y"
from fin_Y have "finite ?X" by (rule finite_imageI)
moreover from F_sub have "?F ⊆ P[?X]"
by (auto simp: indets_extend_indets intro!: PolysI_alt imageI dest!: PolysD(2) subsetD[of F])
moreover from f_in have "?f ∈ P[?X]"
by (auto simp: indets_extend_indets intro!: PolysI_alt imageI dest!: PolysD(2))
moreover have "None ∉ ?X" by simp
ultimately have "?f ∈ √ideal ?F" using assms(3) by (rule radical_idealI)
also have "?f ∈ √ideal ?F ⟷ f ∈ √ideal F"
proof
assume "f ∈ √ideal F"
then obtain m where "f ^ m ∈ ideal F" by (rule radicalE)
hence "extend_indets (f ^ m) ∈ extend_indets ` ideal F" by (rule imageI)
with extend_indets_ideal_subset have "?f ^ m ∈ ideal ?F" unfolding extend_indets_power ..
thus "?f ∈ √ideal ?F" by (rule radicalI)
next
assume "?f ∈ √ideal ?F"
then obtain m where "?f ^ m ∈ ideal ?F" by (rule radicalE)
moreover have "?f ^ m ∈ P[- {None}]"
by (rule Polys_closed_power) (auto intro!: PolysI_alt simp: indets_extend_indets)
ultimately have "extend_indets (f ^ m) ∈ extend_indets ` ideal F"
by (simp add: extend_indets_ideal extend_indets_power)
hence "f ^ m ∈ ideal F" by (simp only: inj_image_mem_iff[OF inj_extend_indets])
thus "f ∈ √ideal F" by (rule radicalI)
qed
finally show ?thesis .
qed
theorem Nullstellensatz:
assumes "finite X" and "F ⊆ P[X]"
and "(f::(_::{countable,linorder} ⇒⇩0 nat) ⇒⇩0 _::alg_closed_field) ∈ ℐ (𝒱 F)"
shows "f ∈ √ideal F"
using assms(1, 2)
proof (rule radical_idealI_extend_indets)
let ?f = "punit.monom_mult 1 (monomial 1 None) (extend_indets f)"
show "𝒱 (insert (1 - ?f) (extend_indets ` F)) = {}"
proof (intro subset_antisym subsetI)
fix a
assume "a ∈ 𝒱 (insert (1 - ?f) (extend_indets ` F))"
moreover have "1 - ?f ∈ insert (1 - ?f) (extend_indets ` F)" by simp
ultimately have "poly_eval a (1 - ?f) = 0" by (rule variety_ofD)
hence "poly_eval a (extend_indets f) ≠ 0"
by (auto simp: poly_eval_minus poly_eval_times simp flip: times_monomial_left)
hence "poly_eval (a ∘ Some) f ≠ 0" by (simp add: poly_eval_extend_indets)
have "a ∘ Some ∈ 𝒱 F"
proof (rule variety_ofI)
fix f'
assume "f' ∈ F"
hence "extend_indets f' ∈ insert (1 - ?f) (extend_indets ` F)" by simp
with ‹a ∈ _› have "poly_eval a (extend_indets f') = 0" by (rule variety_ofD)
thus "poly_eval (a ∘ Some) f' = 0" by (simp only: poly_eval_extend_indets)
qed
with assms(3) have "poly_eval (a ∘ Some) f = 0" by (rule ideal_ofD)
with ‹poly_eval (a ∘ Some) f ≠ 0› show "a ∈ {}" ..
qed simp
qed
theorem strong_Nullstellensatz:
assumes "finite X" and "F ⊆ P[X]"
shows "ℐ (𝒱 F) = √ideal (F::((_::{countable,linorder} ⇒⇩0 nat) ⇒⇩0 _::alg_closed_field) set)"
proof (intro subset_antisym subsetI)
fix f
assume "f ∈ ℐ (𝒱 F)"
with assms show "f ∈ √ideal F" by (rule Nullstellensatz)
qed (metis ideal_ofI variety_ofD variety_of_radical_ideal)
text ‹The following lemma can be used for actually ∗‹deciding› whether a polynomial is contained in
the radical of an ideal or not.›
lemma radical_ideal_iff:
assumes "finite X" and "F ⊆ P[X]" and "f ∈ P[X]" and "x ∉ X"
shows "(f::(_::{countable,linorder} ⇒⇩0 nat) ⇒⇩0 _::alg_closed_field) ∈ √ideal F ⟷
1 ∈ ideal (insert (1 - punit.monom_mult 1 (Poly_Mapping.single x 1) f) F)"
proof -
let ?f = "punit.monom_mult 1 (Poly_Mapping.single x 1) f"
show ?thesis
proof
assume "f ∈ √ideal F"
then obtain m where "f ^ m ∈ ideal F" by (rule radicalE)
from assms(1) have "finite (insert x X)" by simp
moreover have "insert (1 - ?f) F ⊆ P[insert x X]" unfolding insert_subset
proof (intro conjI Polys_closed_minus one_in_Polys Polys_closed_monom_mult PPs_closed_single)
have "P[X] ⊆ P[insert x X]" by (rule Polys_mono) blast
with assms(2, 3) show "f ∈ P[insert x X]" and "F ⊆ P[insert x X]" by blast+
qed simp
moreover have "𝒱 (insert (1 - ?f) F) = {}"
proof (intro subset_antisym subsetI)
fix a
assume "a ∈ 𝒱 (insert (1 - ?f) F)"
moreover have "1 - ?f ∈ insert (1 - ?f) F" by simp
ultimately have "poly_eval a (1 - ?f) = 0" by (rule variety_ofD)
hence "poly_eval a (f ^ m) ≠ 0"
by (auto simp: poly_eval_minus poly_eval_times poly_eval_power simp flip: times_monomial_left)
from ‹a ∈ _› have "a ∈ 𝒱 (ideal (insert (1 - ?f) F))" by (simp only: variety_of_ideal)
moreover from ‹f ^ m ∈ ideal F› ideal.span_mono have "f ^ m ∈ ideal (insert (1 - ?f) F)"
by (rule rev_subsetD) blast
ultimately have "poly_eval a (f ^ m) = 0" by (rule variety_ofD)
with ‹poly_eval a (f ^ m) ≠ 0› show "a ∈ {}" ..
qed simp
ultimately have "ideal (insert (1 - ?f) F) = UNIV" by (rule weak_Nullstellensatz)
thus "1 ∈ ideal (insert (1 - ?f) F)" by simp
next
assume "1 ∈ ideal (insert (1 - ?f) F)"
have "𝒱 (insert (1 - ?f) F) = {}"
proof (intro subset_antisym subsetI)
fix a
assume "a ∈ 𝒱 (insert (1 - ?f) F)"
hence "a ∈ 𝒱 (ideal (insert (1 - ?f) F))" by (simp only: variety_of_ideal)
hence "poly_eval a 1 = 0" using ‹1 ∈ _› by (rule variety_ofD)
thus "a ∈ {}" by simp
qed simp
with assms show "f ∈ √ideal F" by (rule radical_idealI)
qed
qed
end