Theory Nullstellensatz_Field
section ‹Field-Theoretic Version of Hilbert's Nullstellensatz›
theory Nullstellensatz_Field
imports Nullstellensatz "HOL-Types_To_Sets.Types_To_Sets"
begin
text ‹Building upon the geometric version of Hilbert's Nullstellensatz in
@{theory Nullstellensatz.Nullstellensatz}, we prove its field-theoretic version here. To that end we employ
the `types to sets' methodology.›
subsection ‹Getting Rid of Sort Constraints in Geometric Version›
text ‹We can use the `types to sets' approach to get rid of the @{class countable} and @{class linorder}
sort constraints on the type of indeterminates in the geometric version of the Nullstellensatz.
Once the `types to sets' methodology is integrated as a standard component into the main library of
Isabelle, the theorems in @{theory Nullstellensatz.Nullstellensatz} could be replaced by their counterparts
in this section.›
lemmas radical_idealI_internalized = radical_idealI[unoverload_type 'x]
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 ⇒⇩0 nat) ⇒⇩0 'a::alg_closed_field) ∈ √ideal F"
proof -
define Y where "Y = insert x X"
from assms(1) have fin_Y: "finite Y" by (simp add: Y_def)
have "X ⊆ Y" by (auto simp: Y_def)
hence "P[X] ⊆ P[Y]" by (rule Polys_mono)
with assms(2, 3) have F_sub: "F ⊆ P[Y]" and "f ∈ P[Y]" by auto
{
text ‹We define the type @{typ 'y} to be isomorphic to @{term Y}.›
assume "∃(Rep :: 'y ⇒ 'x) Abs. type_definition Rep Abs Y"
then obtain rep :: "'y ⇒ 'x" and abs :: "'x ⇒ 'y" where t: "type_definition rep abs Y"
by blast
then interpret y: type_definition rep abs Y .
from well_ordering obtain le_y'::"('y × 'y) set" where fld: "Field le_y' = UNIV"
and wo: "Well_order le_y'" by meson
define le_y where "le_y = (λa b::'y. (a, b) ∈ le_y')"
from ‹f ∈ P[Y]› have 0: "map_indets rep (map_indets abs f) = f" unfolding map_indets_map_indets
by (intro map_indets_id) (auto intro!: y.Abs_inverse dest: PolysD)
have 1: "map_indets (rep ∘ abs) ` F = F"
proof
from F_sub show "map_indets (rep ∘ abs) ` F ⊆ F"
by (smt PolysD(2) comp_apply image_subset_iff map_indets_id subsetD y.Abs_inverse)
next
from F_sub show "F ⊆ map_indets (rep ∘ abs) ` F"
by (smt PolysD(2) comp_apply image_eqI map_indets_id subsetD subsetI y.Abs_inverse)
qed
have 2: "inj rep" by (meson inj_onI y.Rep_inject)
hence 3: "inj (map_indets rep)" by (rule map_indets_injI)
from fin_Y have 4: "finite (abs ` Y)" by (rule finite_imageI)
from wo have le_y_refl: "le_y x x" for x
by (simp add: le_y_def well_order_on_def linear_order_on_def partial_order_on_def
preorder_on_def refl_on_def fld)
have le_y_total: "le_y x y ∨ le_y y x" for x y
proof (cases "x = y")
case True
thus ?thesis by (simp add: le_y_refl)
next
case False
with wo show ?thesis
by (simp add: le_y_def well_order_on_def linear_order_on_def total_on_def
Relation.total_on_def fld)
qed
from 4 finite_imp_inj_to_nat_seg y.Abs_image have "class.countable TYPE('y)"
by unfold_locales fastforce
moreover have "class.linorder le_y (strict le_y)"
apply standard
subgoal by (fact refl)
subgoal by (fact le_y_refl)
subgoal using wo
by (auto simp: le_y_def well_order_on_def linear_order_on_def partial_order_on_def
preorder_on_def fld dest: transD)
subgoal using wo
by (simp add: le_y_def well_order_on_def linear_order_on_def partial_order_on_def
preorder_on_def antisym_def fld)
subgoal by (fact le_y_total)
done
moreover from assms(1) have "finite (abs ` X)" by (rule finite_imageI)
moreover have "map_indets abs ` F ⊆ P[abs ` X]"
proof (rule subset_trans)
from assms(2) show "map_indets abs ` F ⊆ map_indets abs ` P[X]" by (rule image_mono)
qed (simp only: image_map_indets_Polys)
moreover have "map_indets abs f ∈ P[abs ` X]"
proof
from assms(3) show "map_indets abs f ∈ map_indets abs ` P[X]" by (rule imageI)
qed (simp only: image_map_indets_Polys)
moreover from assms(4) y.Abs_inject have "abs x ∉ abs ` X" unfolding Y_def by blast
moreover have "𝒱 (insert (1 - punit.monom_mult 1 (Poly_Mapping.single (abs x) (Suc 0))
(map_indets abs f)) (map_indets abs ` F)) = {}"
proof (intro set_eqI iffI)
fix a
assume "a ∈ 𝒱 (insert (1 - punit.monom_mult 1 (Poly_Mapping.single (abs x) (Suc 0))
(map_indets abs f)) (map_indets abs ` F))"
also have "… = (λb. b ∘ abs) -` 𝒱 (insert (1 - punit.monom_mult 1 (Poly_Mapping.single x 1) f) F)"
by (simp add: map_indets_minus map_indets_times map_indets_monomial
flip: variety_of_map_indets times_monomial_left)
finally show "a ∈ {}" by (simp only: assms(5) vimage_empty)
qed simp
ultimately have "map_indets abs f ∈ √ideal (map_indets abs ` F)"
by (rule radical_idealI_internalized[where 'x='y, untransferred, simplified])
hence "map_indets rep (map_indets abs f) ∈ map_indets rep ` √ideal (map_indets abs ` F)"
by (rule imageI)
also from 2 have "… = √(ideal F ∩ P[Y]) ∩ P[Y]"
by (simp add: image_map_indets_ideal image_map_indets_radical image_image map_indets_map_indets
1 y.Rep_range)
also have "… ⊆ √ideal F" using radical_mono by blast
finally have ?thesis by (simp only: 0)
}
note rl = this[cancel_type_definition]
have "Y ≠ {}" by (simp add: Y_def)
thus ?thesis by (rule rl)
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::_ ⇒⇩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::_ ⇒⇩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::(_ ⇒⇩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)
theorem weak_Nullstellensatz:
assumes "finite X" and "F ⊆ P[X]" and "𝒱 F = ({}::(_ ⇒ _::alg_closed_field) set)"
shows "ideal F = UNIV"
proof -
from assms(1, 2) have "ℐ (𝒱 F) = √ideal F" by (rule strong_Nullstellensatz)
thus ?thesis by (simp add: assms(3) flip: radical_ideal_eq_UNIV_iff)
qed
lemma radical_ideal_iff:
assumes "finite X" and "F ⊆ P[X]" and "f ∈ P[X]" and "x ∉ X"
shows "(f::_ ⇒⇩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
subsection ‹Field-Theoretic Version of the Nullstellensatz›
text ‹Due to the possibility of infinite indeterminate-types, we have to explicitly add the set of
indeterminates under consideration to the definition of maximal ideals.›
definition generates_max_ideal :: "'x set ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a::comm_ring_1) set ⇒ bool"
where "generates_max_ideal X F ⟷ (ideal F ≠ UNIV ∧
(∀F'. F' ⊆ P[X] ⟶ ideal F ⊂ ideal F' ⟶ ideal F' = UNIV))"
lemma generates_max_idealI:
assumes "ideal F ≠ UNIV" and "⋀F'. F' ⊆ P[X] ⟹ ideal F ⊂ ideal F' ⟹ ideal F' = UNIV"
shows "generates_max_ideal X F"
using assms by (simp add: generates_max_ideal_def)
lemma generates_max_idealI_alt:
assumes "ideal F ≠ UNIV" and "⋀p. p ∈ P[X] ⟹ p ∉ ideal F ⟹ 1 ∈ ideal (insert p F)"
shows "generates_max_ideal X F"
using assms(1)
proof (rule generates_max_idealI)
fix F'
assume "F' ⊆ P[X]" and sub: "ideal F ⊂ ideal F'"
from this(2) ideal.span_subset_spanI have "¬ F' ⊆ ideal F" by blast
then obtain p where "p ∈ F'" and "p ∉ ideal F" by blast
from this(1) ‹F' ⊆ P[X]› have "p ∈ P[X]" ..
hence "1 ∈ ideal (insert p F)" using ‹p ∉ _› by (rule assms(2))
also have "… ⊆ ideal (F' ∪ F)" by (rule ideal.span_mono) (simp add: ‹p ∈ F'›)
also have "… = ideal (ideal F' ∪ ideal F)" by (simp add: ideal.span_Un ideal.span_span)
also from sub have "ideal F' ∪ ideal F = ideal F'" by blast
finally show "ideal F' = UNIV" by (simp only: ideal_eq_UNIV_iff_contains_one ideal.span_span)
qed
lemma generates_max_idealD:
assumes "generates_max_ideal X F"
shows "ideal F ≠ UNIV" and "F' ⊆ P[X] ⟹ ideal F ⊂ ideal F' ⟹ ideal F' = UNIV"
using assms by (simp_all add: generates_max_ideal_def)
lemma generates_max_ideal_cases:
assumes "generates_max_ideal X F" and "F' ⊆ P[X]" and "ideal F ⊆ ideal F'"
obtains "ideal F = ideal F'" | "ideal F' = UNIV"
using assms by (auto simp: generates_max_ideal_def)
lemma max_ideal_UNIV_radical:
assumes "generates_max_ideal UNIV F"
shows "√ideal F = ideal F"
proof (rule ccontr)
assume "√ideal F ≠ ideal F"
with radical_superset have "ideal F ⊂ √ideal F" by blast
also have "… = ideal (√ideal F)" by simp
finally have "ideal F ⊂ ideal (√ideal F)" .
with assms _ have "ideal (√ideal F) = UNIV" by (rule generates_max_idealD) simp
hence "√ideal F = UNIV" by simp
hence "1 ∈ √ideal F" by simp
hence "1 ∈ ideal F" by (auto elim: radicalE)
hence "ideal F = UNIV" by (simp only: ideal_eq_UNIV_iff_contains_one)
moreover from assms have "ideal F ≠ UNIV" by (rule generates_max_idealD)
ultimately show False by simp
qed
lemma max_ideal_shape_aux:
"(λx. monomial 1 (Poly_Mapping.single x 1) - monomial (a x) 0) ` X ⊆ P[X]"
by (auto intro!: Polys_closed_minus Polys_closed_monomial PPs_closed_single zero_in_PPs)
lemma max_ideal_shapeI:
"generates_max_ideal X ((λx. monomial (1::'a::field) (Poly_Mapping.single x 1) - monomial (a x) 0) ` X)"
(is "generates_max_ideal X ?F")
proof (rule generates_max_idealI_alt)
show "ideal ?F ≠ UNIV"
proof
assume "ideal ?F = UNIV"
hence "𝒱 (ideal ?F) = 𝒱 UNIV" by (rule arg_cong)
hence "𝒱 ?F = {}" by simp
moreover have "a ∈ 𝒱 ?F" by (rule variety_ofI) (auto simp: poly_eval_minus poly_eval_monomial)
ultimately show False by simp
qed
next
fix p
assume "p ∈ P[X]" and "p ∉ ideal ?F"
have "p ∈ ideal (insert p ?F)" by (rule ideal.span_base) simp
let ?f = "λx. monomial (1::'a) (Poly_Mapping.single x 1) - monomial (a x) 0"
let ?g = "λx. monomial (1::'a) (Poly_Mapping.single x 1) + monomial (a x) 0"
define q where "q = poly_subst ?g p"
have "p = poly_subst ?f q" unfolding q_def poly_subst_poly_subst
by (rule sym, rule poly_subst_id)
(simp add: poly_subst_plus poly_subst_monomial subst_pp_single flip: times_monomial_left)
also have "… = (∑t∈keys q. punit.monom_mult (lookup q t) 0 (subst_pp ?f t))" by (fact poly_subst_def)
also have "… = punit.monom_mult (lookup q 0) 0 (subst_pp ?f 0) +
(∑t∈keys q - {0}. monomial (lookup q t) 0 * subst_pp ?f t)"
(is "_ = _ + ?r")
by (cases "0 ∈ keys q") (simp_all add: sum.remove in_keys_iff flip: times_monomial_left)
also have "… = monomial (lookup q 0) 0 + ?r" by (simp flip: times_monomial_left)
finally have eq: "p - ?r = monomial (lookup q 0) 0" by simp
have "?r ∈ ideal ?F"
proof (intro ideal.span_sum ideal.span_scale)
fix t
assume "t ∈ keys q - {0}"
hence "t ∈ keys q" and "keys t ≠ {}" by simp_all
from this(2) obtain x where "x ∈ keys t" by blast
hence "x ∈ indets q" using ‹t ∈ keys q› by (rule in_indetsI)
then obtain y where "y ∈ indets p" and "x ∈ indets (?g y)" unfolding q_def
by (rule in_indets_poly_substE)
from this(2) indets_plus_subset have "x ∈ indets (monomial (1::'a) (Poly_Mapping.single y 1)) ∪
indets (monomial (a y) 0)" ..
with ‹y ∈ indets p› have "x ∈ indets p" by (simp add: indets_monomial)
also from ‹p ∈ P[X]› have "… ⊆ X" by (rule PolysD)
finally have "x ∈ X" .
from ‹x ∈ keys t› have "lookup t x ≠ 0" by (simp add: in_keys_iff)
hence eq: "b ^ lookup t x = b ^ Suc (lookup t x - 1)" for b by simp
have "subst_pp ?f t = (∏y∈keys t. ?f y ^ lookup t y)" by (fact subst_pp_def)
also from ‹x ∈ keys t› have "… = ((∏y∈keys t - {x}. ?f y ^ lookup t y) * ?f x ^ (lookup t x - 1)) * ?f x"
by (simp add: prod.remove mult.commute eq)
also from ‹x ∈ X› have "… ∈ ideal ?F" by (intro ideal.span_scale ideal.span_base imageI)
finally show "subst_pp ?f t ∈ ideal ?F" .
qed
also have "… ⊆ ideal (insert p ?F)" by (rule ideal.span_mono) blast
finally have "?r ∈ ideal (insert p ?F)" .
with ‹p ∈ ideal _› have "p - ?r ∈ ideal (insert p ?F)" by (rule ideal.span_diff)
hence "monomial (lookup q 0) 0 ∈ ideal (insert p ?F)" by (simp only: eq)
hence "monomial (inverse (lookup q 0)) 0 * monomial (lookup q 0) 0 ∈ ideal (insert p ?F)"
by (rule ideal.span_scale)
hence "monomial (inverse (lookup q 0) * lookup q 0) 0 ∈ ideal (insert p ?F)"
by (simp add: times_monomial_monomial)
moreover have "lookup q 0 ≠ 0"
proof
assume "lookup q 0 = 0"
with eq ‹?r ∈ ideal ?F› have "p ∈ ideal ?F" by simp
with ‹p ∉ ideal ?F› show False ..
qed
ultimately show "1 ∈ ideal (insert p ?F)" by simp
qed
text ‹We first prove the following lemma assuming that the type of indeterminates is finite, and then
transfer the result to arbitrary types of indeterminates by using the `types to sets' methodology.
This approach facilitates the proof considerably.›
lemma max_ideal_shapeD_finite:
assumes "generates_max_ideal UNIV (F::(('x::finite ⇒⇩0 nat) ⇒⇩0 'a::alg_closed_field) set)"
obtains a where "ideal F = ideal (range (λx. monomial 1 (Poly_Mapping.single x 1) - monomial (a x) 0))"
proof -
have fin: "finite (UNIV::'x set)" by simp
have "(⋂a∈𝒱 F. ideal (range (λx. monomial 1 (Poly_Mapping.single x 1) - monomial (a x) 0))) = ℐ (𝒱 F)"
(is "?A = _")
proof (intro set_eqI iffI ideal_ofI INT_I)
fix p a
assume "p ∈ ?A" and "a ∈ 𝒱 F"
hence "p ∈ ideal (range (λx. monomial 1 (Poly_Mapping.single x 1) - monomial (a x) 0))"
(is "_ ∈ ideal ?B") ..
have "a ∈ 𝒱 ?B"
proof (rule variety_ofI)
fix f
assume "f ∈ ?B"
then obtain x where "f = monomial 1 (Poly_Mapping.single x 1) - monomial (a x) 0" ..
thus "poly_eval a f = 0" by (simp add: poly_eval_minus poly_eval_monomial)
qed
hence "a ∈ 𝒱 (ideal ?B)" by (simp only: variety_of_ideal)
thus "poly_eval a p = 0" using ‹p ∈ ideal _› by (rule variety_ofD)
next
fix p a
assume "p ∈ ℐ (𝒱 F)" and "a ∈ 𝒱 F"
hence eq: "poly_eval a p = 0" by (rule ideal_ofD)
have "p ∈ √ideal (range (λx. monomial 1 (monomial 1 x) - monomial (a x) 0))" (is "_ ∈ √ideal ?B")
using fin max_ideal_shape_aux
proof (rule Nullstellensatz)
show "p ∈ ℐ (𝒱 ?B)"
proof (rule ideal_ofI)
fix a0
assume "a0 ∈ 𝒱 ?B"
have "a0 = a"
proof
fix x
have "monomial 1 (monomial 1 x) - monomial (a x) 0 ∈ ?B" by (rule rangeI)
with ‹a0 ∈ _› have "poly_eval a0 (monomial 1 (monomial 1 x) - monomial (a x) 0) = 0"
by (rule variety_ofD)
thus "a0 x = a x" by (simp add: poly_eval_minus poly_eval_monomial)
qed
thus "poly_eval a0 p = 0" by (simp only: eq)
qed
qed
also have "… = ideal (range (λx. monomial 1 (monomial 1 x) - monomial (a x) 0))"
using max_ideal_shapeI by (rule max_ideal_UNIV_radical)
finally show "p ∈ ideal (range (λx. monomial 1 (monomial 1 x) - monomial (a x) 0))" .
qed
also from fin have "… = √ideal F" by (rule strong_Nullstellensatz) simp
also from assms have "… = ideal F" by (rule max_ideal_UNIV_radical)
finally have eq: "?A = ideal F" .
also from assms have "… ≠ UNIV" by (rule generates_max_idealD)
finally obtain a where "a ∈ 𝒱 F"
and "ideal (range (λx. monomial 1 (Poly_Mapping.single x (1::nat)) - monomial (a x) 0)) ≠ UNIV"
(is "?B ≠ _") by auto
from ‹a ∈ 𝒱 F› have "ideal F ⊆ ?B" by (auto simp flip: eq)
with assms max_ideal_shape_aux show ?thesis
proof (rule generates_max_ideal_cases)
assume "ideal F = ?B"
thus ?thesis ..
next
assume "?B = UNIV"
with ‹?B ≠ UNIV› show ?thesis ..
qed
qed
lemmas max_ideal_shapeD_internalized = max_ideal_shapeD_finite[unoverload_type 'x]
lemma max_ideal_shapeD:
assumes "finite X" and "F ⊆ P[X]"
and "generates_max_ideal X (F::(('x ⇒⇩0 nat) ⇒⇩0 'a::alg_closed_field) set)"
obtains a where "ideal F = ideal ((λx. monomial 1 (Poly_Mapping.single x 1) - monomial (a x) 0) ` X)"
proof (cases "X = {}")
case True
from assms(3) have "ideal F ≠ UNIV" by (rule generates_max_idealD)
hence "1 ∉ ideal F" by (simp add: ideal_eq_UNIV_iff_contains_one)
have "F ⊆ {0}"
proof
fix f
assume "f ∈ F"
with assms(2) have "f ∈ P[X]" ..
then obtain c where f: "f = monomial c 0" by (auto simp: True Polys_empty)
with ‹f ∈ F› have "monomial c 0 ∈ ideal F" by (simp only: ideal.span_base)
hence "monomial (inverse c) 0 * monomial c 0 ∈ ideal F" by (rule ideal.span_scale)
hence "monomial (inverse c * c) 0 ∈ ideal F" by (simp add: times_monomial_monomial)
with ‹1 ∉ ideal F› left_inverse have "c = 0" by fastforce
thus "f ∈ {0}" by (simp add: f)
qed
hence "ideal F = ideal ((λx. monomial 1 (Poly_Mapping.single x 1) - monomial (undefined x) 0) ` X)"
by (simp add: True)
thus ?thesis ..
next
case False
{
text ‹We define the type @{typ 'y} to be isomorphic to @{term X}.›
assume "∃(Rep :: 'y ⇒ 'x) Abs. type_definition Rep Abs X"
then obtain rep :: "'y ⇒ 'x" and abs :: "'x ⇒ 'y" where t: "type_definition rep abs X"
by blast
then interpret y: type_definition rep abs X .
have 1: "map_indets (rep ∘ abs) ` A = A" if "A ⊆ P[X]" for A::"(_ ⇒⇩0 'a) set"
proof
from that show "map_indets (rep ∘ abs) ` A ⊆ A"
by (smt PolysD(2) comp_apply image_subset_iff map_indets_id subsetD y.Abs_inverse)
next
from that show "A ⊆ map_indets (rep ∘ abs) ` A"
by (smt PolysD(2) comp_apply image_eqI map_indets_id subsetD subsetI y.Abs_inverse)
qed
have 2: "inj rep" by (meson inj_onI y.Rep_inject)
hence 3: "inj (map_indets rep)" by (rule map_indets_injI)
have "class.finite TYPE('y)"
proof
from assms(1) have "finite (abs ` X)" by (rule finite_imageI)
thus "finite (UNIV::'y set)" by (simp only: y.Abs_image)
qed
moreover have "generates_max_ideal UNIV (map_indets abs ` F)"
proof (intro generates_max_idealI notI)
assume "ideal (map_indets abs ` F) = UNIV"
hence "1 ∈ ideal (map_indets abs ` F)" by simp
hence "map_indets rep 1 ∈ map_indets rep ` ideal (map_indets abs ` F)" by (rule imageI)
also from map_indets_plus map_indets_times have "… ⊆ ideal (map_indets rep ` map_indets abs ` F)"
by (rule image_ideal_subset)
also from assms(2) have "map_indets rep ` map_indets abs ` F = F"
by (simp only: image_image map_indets_map_indets 1)
finally have "1 ∈ ideal F" by simp
moreover from assms(3) have "ideal F ≠ UNIV" by (rule generates_max_idealD)
ultimately show False by (simp add: ideal_eq_UNIV_iff_contains_one)
next
fix F'
assume "ideal (map_indets abs ` F) ⊂ ideal F'"
with inj_on_subset have "map_indets rep ` ideal (map_indets abs ` F) ⊂ map_indets rep ` ideal F'"
by (rule image_strict_mono) (fact 3, fact subset_UNIV)
hence sub: "ideal F ∩ P[X] ⊂ ideal (map_indets rep ` F') ∩ P[X]" using 2 assms(2)
by (simp add: image_map_indets_ideal image_image map_indets_map_indets 1 y.Rep_range)
have "ideal F ⊂ ideal (map_indets rep ` F')"
proof (intro psubsetI notI ideal.span_subset_spanI subsetI)
fix p
assume "p ∈ F"
with assms(2) ideal.span_base sub show "p ∈ ideal (map_indets rep ` F')" by blast
next
assume "ideal F = ideal (map_indets rep ` F')"
with sub show False by simp
qed
with assms(3) _ have "ideal (map_indets rep ` F') = UNIV"
proof (rule generates_max_idealD)
from subset_UNIV have "map_indets rep ` F' ⊆ range (map_indets rep)" by (rule image_mono)
also have "… = P[X]" by (simp only: range_map_indets y.Rep_range)
finally show "map_indets rep ` F' ⊆ P[X]" .
qed
hence "P[range rep] = ideal (map_indets rep ` F') ∩ P[range rep]" by simp
also from 2 have "… = map_indets rep ` ideal F'" by (simp only: image_map_indets_ideal)
finally have "map_indets rep ` ideal F' = range (map_indets rep)"
by (simp only: range_map_indets)
with 3 show "ideal F' = UNIV" by (metis inj_image_eq_iff)
qed
ultimately obtain a
where *: "ideal (map_indets abs ` F) =
ideal (range (λx. monomial 1 (Poly_Mapping.single x (Suc 0)) - monomial (a x) 0))"
(is "_ = ?A")
by (rule max_ideal_shapeD_internalized[where 'x='y, untransferred, simplified])
hence "map_indets rep ` ideal (map_indets abs ` F) = map_indets rep ` ?A" by simp
with 2 assms(2) have "ideal F ∩ P[X] =
ideal (range (λx. monomial 1 (Poly_Mapping.single (rep x) 1) - monomial (a x) 0)) ∩ P[X]"
(is "_ = ideal ?B ∩ _")
by (simp add: image_map_indets_ideal y.Rep_range image_image map_indets_map_indets
map_indets_minus map_indets_monomial 1)
also have "?B = (λx. monomial 1 (Poly_Mapping.single x 1) - monomial ((a ∘ abs) x) 0) ` X"
(is "_ = ?C")
proof
show "?B ⊆ ?C" by (smt comp_apply image_iff image_subset_iff y.Abs_image y.Abs_inverse)
next
from y.Rep_inverse y.Rep_range show "?C ⊆ ?B" by auto
qed
finally have eq: "ideal F ∩ P[X] = ideal ?C ∩ P[X]" .
have "ideal F = ideal ?C"
proof (intro subset_antisym ideal.span_subset_spanI subsetI)
fix p
assume "p ∈ F"
with assms(2) ideal.span_base have "p ∈ ideal F ∩ P[X]" by blast
thus "p ∈ ideal ?C" by (simp add: eq)
next
fix p
assume "p ∈ ?C"
then obtain x where "x ∈ X" and "p = monomial 1 (monomial 1 x) - monomial ((a ∘ abs) x) 0" ..
note this(2)
also from ‹x ∈ X› have "… ∈ P[X]"
by (intro Polys_closed_minus Polys_closed_monomial PPs_closed_single zero_in_PPs)
finally have "p ∈ P[X]" .
with ‹p ∈ ?C› have "p ∈ ideal ?C ∩ P[X]" by (simp add: ideal.span_base)
also have "… = ideal F ∩ P[X]" by (simp only: eq)
finally show "p ∈ ideal F" by simp
qed
hence ?thesis ..
}
note rl = this[cancel_type_definition]
from False show ?thesis by (rule rl)
qed
theorem Nullstellensatz_field:
assumes "finite X" and "F ⊆ P[X]" and "generates_max_ideal X (F::(_ ⇒⇩0 _::alg_closed_field) set)"
and "x ∈ X"
shows "{0} ⊂ ideal F ∩ P[{x}]"
unfolding subset_not_subset_eq
proof (intro conjI notI)
show "{0} ⊆ ideal F ∩ P[{x}]" by (auto intro: ideal.span_zero zero_in_Polys)
next
from assms(1, 2, 3) obtain a
where eq: "ideal F = ideal ((λx. monomial 1 (monomial 1 x) - monomial (a x) 0) ` X)"
by (rule max_ideal_shapeD)
let ?p = "λx. monomial 1 (monomial 1 x) - monomial (a x) 0"
from assms(4) have "?p x ∈ ?p ` X" by (rule imageI)
also have "… ⊆ ideal F" unfolding eq by (rule ideal.span_superset)
finally have "?p x ∈ ideal F" .
moreover have "?p x ∈ P[{x}]"
by (auto intro!: Polys_closed_minus Polys_closed_monomial PPs_closed_single zero_in_PPs)
ultimately have "?p x ∈ ideal F ∩ P[{x}]" ..
also assume "… ⊆ {0}"
finally show False
by (metis diff_eq_diff_eq diff_self monomial_0D monomial_inj one_neq_zero singletonD)
qed
end