Theory Weak_Hilbert_Basis
section ‹The weak Hilbert Basis theorem›
theory Weak_Hilbert_Basis
imports
"HOL-Algebra.Polynomials"
"HOL-Algebra.Indexed_Polynomials"
"Polynomials_Ring_Misc"
"Padic_Field.Cring_Multivariable_Poly"
"HOL-Algebra.Module"
"Ring_Misc"
begin
text ‹In this section, we show what we called "weak" Hilbert basis theorem, meaning Hilbert basis
theorem for univariate polynomials
The theorem is done for all three (Polynomials, UP, IP with card = 1)
models of polynomials that exists in HOL-Algebra›
subsection ‹Weak Hilbert Basis›
lemma (in noetherian_domain) weak_Hilbert_basis:‹noetherian_ring ((carrier R)[X])›
proof(rule ring.trivial_ideal_chain_imp_noetherian)
show ‹ring ((carrier R) [X])›
using carrier_is_subring univ_poly_is_ring by blast
next
interpret kxr: cring "(carrier R)[X]"
using carrier_is_subring univ_poly_is_cring by blast
fix C
assume F:‹C ≠ {}› ‹subset.chain {I. ideal I ((carrier R) [X])} C›
have f1:‹I∈C ⟹ ideal I (carrier R[X])› for I
using F unfolding subset.chain_def by(auto)
have f2:‹a∈carrier((carrier R)[X])∧ aa∈carrier((carrier R)[X])
⟹ coeff (a⊕⇘(carrier R)[X]⇙ aa) k = coeff a k⊕ coeff aa k ›
for a aa k
unfolding univ_poly_add
apply(subst poly_add_coeff)
using polynomial_in_carrier[of ‹carrier R› a] polynomial_in_carrier[of ‹carrier R› aa]
polynomial_def carrier_is_subring
by (simp add: univ_poly_carrier)+
have f4a:‹subring (carrier R) R›
using carrier_is_subring by auto
have degree_of_inv:
‹p∈carrier((carrier R)[X]) ⟹ degree (inv⇘add_monoid ((carrier R)[X])⇙ p) = degree p› for p
by (metis a_inv_def local.ring_axioms ring.carrier_is_subring univ_poly_a_inv_degree)
from f1 have ‹I∈C ⟹ a ∈ I ⟹ coeff a (degree a)∈ (carrier R)› for a I
using lead_coeff_in_carrier by blast
have emp_in_i:‹ideal I ((carrier R)[X]) ⟹ [] ∈ I› for I
by (simp add: additive_subgroup_def ideal_def subgroup_def univ_poly_zero)
have g0:‹I⊆I' ⟹ lead_coeff_set I k ⊆ lead_coeff_set I' k›
for I I' k
unfolding lead_coeff_set_def deg_poly_set by(auto)
have g1:‹ ideal I ((carrier R)[X]) ⟹ {(X⊗⇘(carrier R)[X]⇙l) | l. l∈I} ⊆ I› for I
using f4a ideal.I_l_closed var_closed(1) by fastforce
then have g2:
‹ideal I ((carrier R)[X]) ⟹ lead_coeff_set {(X⊗⇘(carrier R)[X]⇙l) | l. l∈I} k ⊆ lead_coeff_set I k›
for I k
using g0 g1 by auto
have f7b:‹ideal I ((carrier R)[X]) ⟹ lead_coeff_set I k ⊆ lead_coeff_set I (k+1)› for I k
unfolding lead_coeff_set_def deg_poly_set
proof(safe)
fix x a
assume y1:‹ideal I (poly_ring R)› ‹a ∈ I› ‹k = degree a›
then show
‹∃aa. local.coeff a (degree a) = local.coeff aa (degree aa) ∧ aa ∈ {aa ∈ I. degree aa = degree a + 1} ∪ {[]}›
apply(cases ‹a=[]›)
apply(rule exI[where x=‹[]›])
apply blast
apply(rule exI[where x=‹a⊗⇘(carrier R)[X]⇙X›])
apply(safe)
unfolding ideal_def univ_poly_mult
using poly_mult_var[of "(carrier R)" a for a]
apply (metis One_nat_def additive_subgroup.a_Hcarr
append_is_Nil_conv f4a hd_append2 lead_coeff_simp univ_poly_mult)
apply (simp add: f4a ideal_axioms_def univ_poly_mult var_closed(1))
using poly_mult_var[of ‹(carrier R)› a for a]
by (metis Suc_eq_plus1 Suc_pred' diff_Suc_Suc f4a ideal.Icarr length_append_singleton
length_greater_0_conv minus_nat.diff_0 univ_poly_mult y1(1))
next
assume y1:‹ideal I (poly_ring R)›
then show
‹∃a. local.coeff [] (degree []) = local.coeff a (degree a) ∧ a ∈ {a ∈ I. degree a = k + 1} ∪ {[]}›
by force
qed
then have f7:‹y∈C ⟹ lead_coeff_set y k ⊆ lead_coeff_set y (k+1)› for k y
using f1 by blast
then have f8:‹k≤k' ⟹ y∈C ⟹ lead_coeff_set y k ⊆ lead_coeff_set y k'› for k k' y
apply(induct k')
using le_Suc_eq by(auto)
have n:‹noetherian_ring R›
by (simp add: noetherian_ring_axioms)
have c:‹x∈C ⟹ subset.chain {I. ideal I R} {lead_coeff_set x k | k. k∈UNIV}› for x
apply(subst subset_chain_def)
apply(safe)
apply (simp add: f1 ideal_lead_coeff_set)
by (meson f8 nle_le subsetD)
have c':‹ subset.chain {I. ideal I R} {lead_coeff_set x k | x. x∈C}› for k
proof(rule Zorn.subset.chainI)
show ‹{lead_coeff_set x k |x. x ∈ C} ⊆ {I. ideal I R}›
using f1 ideal_lead_coeff_set by blast
next
fix xa y
assume 1:‹xa ∈ {lead_coeff_set x k |x. x ∈ C}› ‹ y ∈ {lead_coeff_set x k |x. x ∈ C}›
obtain z z' where g10:‹xa = lead_coeff_set z k ∧ y =lead_coeff_set z' k ∧ z∈C ∧ z' ∈C ›
using "1"(1) "1"(2) by blast
then have ‹z⊆z' ∨ z' ⊆ z›
using F unfolding subset.chain_def by(auto)
then show ‹(⊂)⇧=⇧= xa y ∨ (⊂)⇧=⇧= y xa›
using g0 g10 by blast+
qed
then have U0:‹∀x∈C. (⋃{lead_coeff_set x k | k. k∈UNIV}) ∈ {lead_coeff_set x k | k. k∈UNIV}›
proof(safe)
fix x
assume a1: "x ∈ C"
have "∀A. ¬ subset.chain {A. ideal A R} A ∨ ⋃ A ∈ A ∨ A = {}"
using ideal_chain_is_trivial by blast
then show ‹∃k. ⋃ {lead_coeff_set x k |k. k ∈ UNIV} = lead_coeff_set x k ∧ k ∈ UNIV›
using a1 c by auto
qed
have t9:‹x∈C ⟹ ideal (lead_coeff_set x k) R› for k x
using f1 ideal_lead_coeff_set by blast
then have degree_of_inv:‹{lead_coeff_set x k | x. x∈C} ≠ {}› for x::‹'a set› and k
using F(1) by blast
then have U1:‹∀k. (⋃{lead_coeff_set x k |x. x ∈ C}) ∈ {lead_coeff_set x k | x. x∈C}›
using ideal_lead_coeff_set f7b n c'
using ideal_chain_is_trivial[OF degree_of_inv c'] by(auto)
have kl0:‹x∈C ∧ y∈C⟹x=y ⟷ (∀k. deg_poly_set x k = deg_poly_set y k)› for x y
proof(safe)
fix xa :: "'a list"
assume a1: "y ∈ C"
assume a2: "∀k. deg_poly_set x k = deg_poly_set y k"
assume "xa ∈ x"
then have "∃n. xa ∈ deg_poly_set x n"
using deg_poly_set noetherian_domain_axioms by fastforce
then show "xa ∈ y"
using a2 a1
by (metis (no_types, lifting) UnE emp_in_i f1 local.ring_axioms
mem_Collect_eq ring.deg_poly_set singleton_iff)
next
fix xa :: "'a list"
assume a1: "x ∈ C"
assume a2: "∀k. deg_poly_set x k = deg_poly_set y k"
assume "xa ∈ y"
then have "∃n. xa ∈ deg_poly_set y n"
using deg_poly_set noetherian_domain_axioms by fastforce
then show "xa ∈ x"
using a2 a1
by (metis (no_types, lifting) UnE emp_in_i f1 local.ring_axioms
mem_Collect_eq ring.deg_poly_set singleton_iff)
qed
have kl:‹x'∈C ∧ y∈C ∧ x'⊆ y⟹(∀k≤n. lead_coeff_set x' k = lead_coeff_set y k)
⟷ (∀k≤n. deg_poly_set x' k = deg_poly_set y k)›
for x' y n
apply(rule iffI)
subgoal
proof(induct n)
case z:0
from lead_coeff_set_0 have d2:‹{a. [a] ∈ x'} = {a. [a] ∈ y}›
using z(2)[rule_format, of 0] unfolding lead_coeff_set_def
using z.prems(1) f1 unfolding ideal_def
by (simp add:f1 ideal_def polynomial_def univ_poly_carrier additive_subgroup.a_Hcarr)
(metis (mono_tags, lifting) additive_subgroup.a_Hcarr insert_iff
list.sel(1) list.simps(3) mem_Collect_eq polynomial_def univ_poly_carrier)
show ?case
apply(insert z)
apply(simp)
apply(subst (asm) (1 2) lead_coeff_set_0)
apply(subst (1 2) deg_poly_set_0)
using d2 by(auto)
next
case (Suc n)
have t0:‹∀k≤n. deg_poly_set x' k = deg_poly_set y k›
using Suc.hyps Suc.prems(1) Suc.prems(2) le_Suc_eq by blast
have t':‹ideal x' ((carrier R)[X])›
using Suc.prems(1) f1 by blast
have t:‹deg_poly_set x' (Suc n) = deg_poly_set y (Suc n) ⟹ ?case›
using Suc.hyps Suc.prems(1) Suc.prems(2) le_Suc_eq by presburger
have ‹ ∀k. ∃S. lead_coeff_set x' k = genideal R (S k) ∧ finite (S k)›
by (meson ideal_lead_coeff_set finetely_gen t')
then have ‹∃S. ∀k. lead_coeff_set x' k = genideal R (S k) ∧ finite (S k)›
by moura
then obtain S where t1:‹∀k. lead_coeff_set x' k = genideal R (S k) ∧ finite (S k)›
by (blast)
then have ‹∀k≤Suc n. lead_coeff_set y (k) = genideal R (S k)›
using Suc.prems(2) le_Suc_eq by presburger
show ?case
proof(rule t)
show ‹deg_poly_set x' (Suc n) = deg_poly_set y (Suc n)›
unfolding deg_poly_set
proof(safe)
fix x
assume 2:‹x ∉ {}› ‹x ≠ []› ‹x ∈ x'› ‹degree x = Suc n›
then show ‹x ∈ y›
using Suc.prems(1) by blast
next
fix x
assume 2:‹x ∉ {}› ‹x ≠ []› ‹x ∈ y› ‹degree x = Suc n›
{assume 1:‹x ≠ []› ‹x ∈ y› ‹length x - Suc 0 = Suc n› ‹x ∉ x'›
have ‹lead_coeff_set x' (Suc n) = lead_coeff_set y (Suc n)›
using Suc.prems(2) by auto
then have tp:‹coeff x (degree x) ∈ lead_coeff_set x' (Suc n)›
by (metis (mono_tags, lifting) "1"(2) "1"(3) One_nat_def
Un_iff deg_poly_set lead_coeff_set_def mem_Collect_eq)
then have ‹∃x2. x2≠x ∧ x2 ∈ x' ∧ coeff x2 (degree x2) = coeff x (degree x)∧ degree x2 = Suc n›
unfolding lead_coeff_set_def by(simp) (metis (mono_tags, lifting) "1"(1) "1"(2) "1"(4)
One_nat_def Suc.prems(1) Un_iff coeff.simps(1) deg_poly_set f1 ideal.Icarr lead_coeff_simp
mem_Collect_eq partial_object.select_convs(1) polynomial_def singletonD univ_poly_def)
then obtain x2 where g1:‹coeff x2 (degree x2) ∈ lead_coeff_set x' (Suc n) ∧ x2 ≠ x ∧degree x2
= Suc n∧ x2∈ x'∧ coeff x2 (degree x2) = coeff x (degree x)›
using tp by force
then have g2:‹x2 ∈ y›
using Suc.prems(1) by blast
then have g3:‹x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2 ∈ y›
using t'
by (meson "1"(2) Suc.prems(1) additive_subgroup.a_closed additive_subgroup_def
f1 group.subgroupE(3) ideal_def kxr.add.group_l_invI kxr.add.l_inv_ex)
then have g4:‹x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2 ∉ x'›
using t' g1 "1"(2) "1"(4) f1 Suc.prems(1)
kxr.add.m_assoc kxr.add.r_inv_ex kxr.add.subgroupE(4) kxr.minus_unique kxr.r_zero
unfolding additive_subgroup_def ideal_def
by (smt (verit, best) f1 ideal.Icarr kxr.add.comm_inv_char)
have ‹degree x = Suc n ∧ degree x2 = Suc n›
using 1 g1 by auto
also have ‹coeff (inv⇘add_monoid ((carrier R)[X])⇙ x2) (degree x2) = inv⇘add_monoid R⇙ (coeff x (degree x))›
by (smt (verit, best) a_inv_def diff_0_eq_0 f4a g1 ideal.Icarr kxr.add.inv_closed
kxr.l_neg length_add list.size(3) max.idem nat.discI t' univ_poly_a_inv_degree univ_poly_zero)
then have ‹coeff ((x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2)) (Suc n) = 𝟬 ›
by (smt (verit, best) "1"(2) Suc.prems(1) ‹degree x = Suc n ∧ degree x2 = Suc n›
a_inv_def add.Units_eq add.Units_r_inv lead_coeff_in_carrier f1 f2 g1 ideal.Icarr kxr.add.inv_closed)
then have *:‹∀k≥Suc n. coeff ((x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2)) (k) = 𝟬 ›
by (smt (verit, best) "1"(2) Suc.prems(1) a_inv_def calculation coeff_degree f1 f2 f4a g2
ideal.Icarr kxr.add.inv_closed l_zero le_eq_less_or_eq univ_poly_a_inv_degree zero_closed)
then have **:‹degree (x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2) ≤ Suc n›
unfolding univ_poly_add
by (metis (no_types, lifting) a_inv_def calculation f4a g1 ideal.Icarr
max.idem poly_add_degree t' univ_poly_a_inv_degree univ_poly_add)
then have b0:‹coeff ((x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2)) (Suc n) = 𝟬 ›
using * by auto
have b1:‹x∈(carrier ((carrier R)[X])) ⟹ degree x ≤ Suc n ∧ coeff x (Suc n) = 𝟬 ⟹ degree x ≤ n › for x
by (metis diff_0_eq_0 diff_Suc_1 le_SucE lead_coeff_simp list.size(3) polynomial_def univ_poly_carrier)
then have ‹degree (x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2) ≤ n›
using b0 b1 **
by (meson Suc.prems(1) f1 g3 ideal.Icarr)
then obtain k where n:‹k≤n ∧ k = degree (x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2)›
by blast
then have‹x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2 ∈ deg_poly_set y k ∧ x ⊕⇘(carrier R)[X]⇙ inv⇘add_monoid ((carrier R)[X])⇙ x2 ∉ deg_poly_set x' k›
unfolding deg_poly_set using g1 g2 g3 monoid.cases monoid.simps(1) monoid.simps(2)
partial_object.select_convs(1) emp_in_i g4 t' by fastforce
then have False using n t0 by blast
}note this_is_proof=this
then show ‹x∈x'›
using this_is_proof "2"(2) "2"(3) "2"(4) One_nat_def by argo
qed
qed
qed
using lead_coeff_set_def by presburger
have chain_is:‹x'∈C ∧ y∈C ⟹x' ⊆ y ∨ y ⊆ x' › for x' y
using F unfolding subset.chain_def by(auto)
from kl have imppp:‹x'∈C ∧ y∈C ∧ x'⊆ y
⟹(∀k. lead_coeff_set x' k = lead_coeff_set y k) ⟷ (∀k. deg_poly_set x' k = deg_poly_set y k)›
for x' y
by (meson dual_order.refl)
then have impp:‹x'∈C ∧ y∈C⟹(∀k. lead_coeff_set x' k = lead_coeff_set y k)
⟷ (∀k. deg_poly_set x' k = deg_poly_set y k)›
for x' y
by (metis chain_is)
then have sup1:‹x'∈C ∧ y∈C ⟹ (x' = y) ⟷(∀k. lead_coeff_set x' k = lead_coeff_set y k)› for x' y
using kl0 by presburger
then have ‹∃Ux. ∀k. Ux k = ⋃{lead_coeff_set x k |x. x ∈ C} ›
by auto
then obtain Ux where U_x:‹∀k. Ux k = ⋃{lead_coeff_set x k |x. x ∈ C}› by blast
then have ‹∃Uk. ∀x∈C. ( Uk x = ⋃{lead_coeff_set x k |k. k∈UNIV})› using U0 by auto
then obtain Uk where U_k:‹∀x∈C. (Uk x = ⋃{lead_coeff_set x k |k. k∈UNIV})› using U0 by(auto)
have ‹(⋃{lead_coeff_set x k |x k. x ∈ C ∧ k∈UNIV}) = (⋃x∈C. (⋃k. lead_coeff_set x k))›
by auto
have ‹(⋃x∈C. (⋃k. lead_coeff_set x k)) ∈ {lead_coeff_set x k|x k. x∈C} ›
proof -
have n0:‹x∈C ∧ y∈C ∧ x⊆y ⟹ (⋃k. lead_coeff_set x k) ⊆ (⋃k. lead_coeff_set y k)› for x y
by (simp add: SUP_mono' g0)
obtain s1 where n1:‹(∀x∈C. (⋃k. lead_coeff_set x k) = lead_coeff_set x (s1 x))›
using U0
by(simp)(metis full_SetCompr_eq)
then have n4:‹(⋃x∈C. (⋃k. lead_coeff_set x k)) = (⋃x∈C. lead_coeff_set x (s1 x))›
by auto
have ‹x∈C ∧ y∈C ⟹ x⊆y ∨ y⊆x› for x y
using F unfolding subset.chain_def by(auto)
then have n1:‹x∈C ∧ y∈C ⟹ lead_coeff_set x (s1 x) ⊆ lead_coeff_set y (s1 y) ∨
lead_coeff_set y (s1 y) ⊆ lead_coeff_set x (s1 x)›
for x y
apply(cases ‹x⊆y›)
apply(rule disjI1)
subgoal using n0 n1 by auto[1]
by (metis n0 n1)
have n2:‹subset.chain {I. ideal I R} {lead_coeff_set x (s1 x) |x. x∈C}›
apply(rule subset.chainI)
using ‹⋀x k. x ∈ C ⟹ ideal (lead_coeff_set x k) R› apply force
using n1 by auto
have n3:‹{lead_coeff_set x (s1 x) |x. x∈C} ≠ {}›
using F(1) by blast
have ‹(⋃x∈C. lead_coeff_set x (s1 x)) = (⋃ {lead_coeff_set x (s1 x) |x. x∈C})›
by auto
then have ‹(⋃x∈C. lead_coeff_set x (s1 x)) ∈ {lead_coeff_set x (s1 x) |x. x∈C}›
using ideal_chain_is_trivial[OF n3 n2]
by(auto)
then show ‹(⋃x∈C. ⋃ (range (lead_coeff_set x))) ∈ {lead_coeff_set x k |x k. x ∈ C} ›
using n4 by auto
qed
then obtain x l where n5:‹(⋃ {lead_coeff_set x k |x k. x∈C}) = lead_coeff_set x l ∧ x∈C›
using ‹⋃ {lead_coeff_set x k |x k. x ∈ C ∧ k ∈ UNIV} = (⋃x∈C. ⋃ (range (lead_coeff_set x)))›
by auto
then have ‹∀y∈C. x⊆y ⟶ (∀ n≥l. (lead_coeff_set y n = lead_coeff_set x l))›
apply(safe)
subgoal using UnionI by blast
by (meson f8 g0 in_mono)
have ‹∀k. ∃y'. ⋃{lead_coeff_set x k |x. x ∈ C} = lead_coeff_set (y' k) k ∧ y' k ∈ C›
using U1 by fastforce
then have ‹∃y'. ∀k. ⋃{lead_coeff_set x k |x. x ∈ C} = lead_coeff_set (y' k) k ∧ y' k ∈ C›
by moura
then obtain y' where n10:‹⋃{lead_coeff_set x k |x. x ∈ C} = lead_coeff_set (y' k) k ∧ y' k ∈ C›
for k
by blast
have n8:‹({y' k|k. k≤l}∪{x}) ⊆ C›
using ‹⋀k. ⋃ {lead_coeff_set x k |x. x ∈ C} = lead_coeff_set (y' k) k ∧ y' k ∈ C› n5 by auto
then have fin:‹finite ({y' k|k. k≤l}∪{x})›
by(auto)
have n9:‹subset.chain C ({y' k|k. k≤l}∪{x})›
apply(rule subset.chainI)
using n8 apply force
using F(2) n8 unfolding subset.chain_def
by (meson subset_eq)
then obtain M where n11:‹M∈C ∧ (⋃({y' k|k. k≤l}∪{x}) = M)›
unfolding subset_chain_def
by (metis (no_types, lifting) Un_empty Union_in_chain n9 fin insert_not_empty subsetD)
then have ‹∀y∈C. M⊆y ⟶ (∀ n≤l. (lead_coeff_set y n = lead_coeff_set (y' n) n))›
using n10 g0 apply(safe)
using Sup_le_iff mem_Collect_eq by blast+
then have nn:‹∀y∈C. ∀n≤l. M⊆y ⟶ (lead_coeff_set (y) n = lead_coeff_set M n)›
using ‹M ∈ C ∧ ⋃ ({y' k |k. k ≤ l} ∪ {x}) = M› by auto
then have ‹∀y∈C. ∀n≥l. M⊆y ⟶ (lead_coeff_set (y) n = lead_coeff_set M n)›
using ‹M ∈ C ∧ ⋃ ({y' k |k. k ≤ l} ∪ {x}) = M›
using ‹∀y∈C. x ⊆ y ⟶ (∀n≥l. lead_coeff_set y n = lead_coeff_set x l)› by auto
then have n_1:‹∀y∈C. M ⊆ y ⟶ M = y›
by (metis n11 sup1 nn linorder_le_cases)
have ‹⋃C = M›
proof(rule ccontr)
assume h_1:‹⋃C ≠ M›
then have f_0:‹∃x∈⋃C. x∉M›
by (meson UnionI ‹M ∈ C ∧ ⋃ ({y' k |k. k ≤ l} ∪ {x}) = M› subset_antisym subset_iff)
then obtain x where f_1:‹x∈⋃C ∧ x∉M› by blast
then have f_3:‹∃M'∈C. x∈M'›
by blast
then obtain M' where f_2:‹x∈M'› by blast
then have ‹M⊆M' ∧ M≠M'›
using F unfolding subset_chain_def
by (metis f_1 f_3 n11 n_1 subsetD)
then show False
using n_1 n11 f_1 f_3 F(2) unfolding subset_chain_def
by (metis subsetD)
qed
then show ‹⋃ C ∈ C›
by (simp add: n11)
qed
subsection ‹Some properties of noetherian rings›
text ‹Assuming I is an ideal of A and A is noetherian, then ‹A/I› is noetherian.›
lemma noetherian_ring_imp_quot_noetherian_ring:
assumes h1:‹noetherian_ring A› and h2:‹ideal I A›
shows‹noetherian_ring (A Quot I)›
proof -
interpret cr:ring A
using h1 unfolding noetherian_ring_def by(auto)
interpret crI: ring "(A Quot I)"
by (simp add: h2 ideal.quotient_is_ring)
interpret rhr:ring_hom_ring A "(A Quot I)" "((+>⇘A⇙) I)"
using h2 ideal.rcos_ring_hom_ring by blast
have rhr_p:‹ring_hom_ring A (A Quot I) ((+>⇘A⇙) I)›
using h2 ideal.rcos_ring_hom_ring by blast
from h1 show ?thesis
proof(intro ring.trivial_ideal_chain_imp_noetherian)
assume 1:‹noetherian_ring A›
show ‹ring (A Quot I)›
by (simp add: crI.ring_axioms)
next
fix C
assume 1:‹noetherian_ring A› ‹C ≠ {}› ‹subset.chain {Ia. ideal Ia (A Quot I)} C›
let ?f=‹the_inv_into ({J. ideal J A ∧ I ⊆ J}) (λx. (+>⇘A⇙) I ` x)›
have inv_imp:‹∀J∈{J. ideal J A ∧ I ⊆ J}. ?f ((+>⇘A⇙) I ` J) = J›
using the_inv_into_onto[of ‹λx. (+>⇘A⇙) I`x› ‹{J. ideal J A ∧ I ⊆ J}›]
apply(subst set_eq_iff)
by (metis (no_types, lifting) Collect_cong bij_betw_def cr.ring_axioms h2
ring.quot_ideal_correspondence the_inv_into_f_f)+
have rule_inv:‹x ∈ the_inv_into {J. ideal J A ∧ I ⊆ J} ((`) ((+>⇘A⇙) I)) J
⟹ideal J (A Quot I) ⟹ ideal J' (A Quot I) ⟹ J ⊆ J'
⟹ x ∈ the_inv_into {J. ideal J A ∧ I ⊆ J} ((`) ((+>⇘A⇙) I)) J'›
for x J J'
by (smt (verit, best) Collect_cong additive_subgroup.a_subset bij_betw_imp_surj_on
cr.canonical_proj_vimage_mem_iff f_the_inv_into_f_bij_betw h2 ideal_def image_eqI
image_eqI inj_onI mem_Collect_eq mem_Collect_eq ring.ideal_incl_iff
ring.quot_ideal_correspondence subsetD the_inv_into_onto)
have inv:‹bij_betw ?f {J. ideal J (A Quot I)} {J. ideal J A ∧ I ⊆ J}
∧ (∀J J'. {J,J'} ⊆ {J. ideal J (A Quot I)} ∧ J ⊆ J' ⟶ ?f J ⊆ ?f J')›
using ring.quot_ideal_correspondence[of A I] the_inv_into_onto[of ‹λx. (+>⇘A⇙) I`x›
‹{J. ideal J A ∧ I ⊆ J}›]
unfolding bij_betw_def
using cr.ring_axioms h2 the_inv_into_onto inj_on_the_inv_into f_the_inv_into_f
inj_on_the_inv_into[of ‹λx. (+>⇘A⇙) I`x› ‹{J. ideal J A ∧ I ⊆ J}›]
additive_subgroup.a_subset cr.canonical_proj_vimage_mem_iff
f_the_inv_into_f[of ‹(λx. (+>⇘A⇙) I ` x)› ‹{J. ideal J A ∧ I ⊆ J}›]
ideal_def image_eqI mem_Collect_eq ring.ideal_incl_iff subsetD
by(auto simp: rule_inv)
then have ‹∀c∈C. ideal (?f c) A›
using 1(3) inv unfolding subset.chain_def
using bij_betwE by fast
have inv_imp2:‹∀J∈{J. ideal J (A Quot I)}. ((+>⇘A⇙) I ` ?f J) = J›
by (smt (verit, del_insts) Collect_cong bij_betw_def cr.ring_axioms
h2 imageE inv_imp ring.quot_ideal_correspondence)
have ‹∀c c'. c ∈C ∧ c' ∈C ∧ c⊆c' ⟶ ?f c ⊆ ?f c'›
using inv using 1(3) unfolding subset_chain_def
by (meson empty_subsetI insert_subset subsetD)
then have sub1:‹subset.chain {Ia. ideal Ia (A)} (?f`C)›
using 1(3) unfolding subset_chain_def image_def
using ‹∀c∈C. ideal (?f c) A› apply(safe)
apply (simp add: image_def)
by (meson in_mono)
have sub2 :‹(?f`C) ≠ {}›
using "1"(2) by blast
then have k0:‹(⋃(?f`C)) ∈ (?f`C)›
by (metis (no_types) h1 noetherian_ring.ideal_chain_is_trivial sub1 sub2)
then have ‹(+>⇘A⇙) I ` (⋃(?f`C)) = (⋃C)›
apply(safe)
apply (smt (verit, del_insts) "1"(3) UnionI image_eqI inv_imp2 subset.chain_def subsetD)
by (smt (verit, best) "1"(3) SUP_upper in_mono inv_imp2 subset_chain_def subset_image_iff)
then show ‹⋃ C ∈ C›
by (smt (verit) "1"(3) k0 image_iff inv_imp2 subset.chain_def subsetD)
qed
qed
text ‹If A is noetherian and ‹A ≃ B› then B is noetherian.›
lemma noetherian_isom_imp_noetherian:
assumes h1:‹noetherian_ring A ∧ ring B ∧ A ≃ B›
shows ‹noetherian_ring B›
proof(rule ring.trivial_ideal_chain_imp_noetherian)
show ‹ring B› using h1 by(simp)
next
fix C
assume h2:‹C≠{}› and h3:‹subset.chain {I. ideal I B} C›
obtain g where bij_g:‹bij_betw g (carrier A) (carrier B) ∧ g∈ring_hom A B›
using h1 is_ring_iso_def ring_iso_def by fastforce
obtain h where bij_h:‹bij_betw h (carrier B) (carrier A) ∧ h∈ring_hom B A ∧ h = the_inv_into (carrier A) g›
using h1 is_ring_iso_def ring_iso_def
by (smt (verit, ccfv_SIG) bij_betwE bij_betw_def bij_betw_the_inv_into bij_g f_the_inv_into_f
noetherian_ring.axioms(1) ring.ring_simprules(1) ring.ring_simprules(5) ring.ring_simprules(6)
ring_hom_add ring_hom_memI ring_hom_mult ring_hom_one the_inv_into_f_f)
from bij_g have f0:‹ideal I A ⟹ ideal (g ` I) B› for I
using h1 img_ideal_is_ideal noetherian_ring_def ring_iso_def by fastforce
from bij_h have f2:‹ideal I B ⟹ ideal (h ` I) A› for I
using h1 img_ideal_is_ideal noetherian_ring_def ring_iso_def by fastforce
then obtain g' where jj1:‹g' = the_inv_into (carrier A) (g)›
by blast
then have f1:‹∀a∈carrier A. ∀b∈carrier B. g (g' b) = b ∧ g' (g a) = a›
by (meson bij_betw_def bij_g f_the_inv_into_f_bij_betw the_inv_into_f_f)
then have ‹∃f'. bij_betw f' {I. ideal I A} {I. ideal I B}›
apply(intro exI[where x=‹(`) g›])
apply(rule bij_betw_byWitness[where f'=‹(`) h›])
unfolding image_def apply(safe)
using jj1 bij_h h1 ideal.Icarr ring.ring_simprules(6) apply fastforce
using jj1 additive_subgroup.a_subset bij_h h1 ideal.axioms(1) ring.ring_simprules(6) apply fastforce
apply (metis bij_betwE bij_h ideal.Icarr jj1)
using bij_g bij_h f_the_inv_into_f_bij_betw ideal.Icarr apply fastforce
apply(fold image_def)
using f0 apply presburger
using f2 by presburger
then have f5:‹∀J∈{I. ideal I A}. h ` g ` J = J ∧ (∀J∈{I. ideal I B}. g ` h ` J = J)›
unfolding image_def apply(safe)
apply (metis bij_betw_def bij_g bij_h ideal.Icarr the_inv_into_f_f)
apply (smt (verit, best) bij_betwE bij_g bij_h f1 ideal.Icarr jj1 mem_Collect_eq)
apply (metis bij_g bij_h f_the_inv_into_f_bij_betw ideal.Icarr)
by (metis (mono_tags, lifting) bij_g bij_h f_the_inv_into_f_bij_betw ideal.Icarr mem_Collect_eq)
then have ‹∀c∈C. ideal (h ` c) A›
unfolding subset.chain_def
by (metis f2 h3 mem_Collect_eq subset_chain_def subset_eq)
then have inv_imp2:‹∀J∈{J. ideal J (B)}. (g ` h ` J) = J›
by (metis f5 f2 mem_Collect_eq)
then have sub1:‹subset.chain {Ia. ideal Ia (A)} ((λx. h ` x) `C)›
unfolding subset_chain_def image_def apply(safe)
apply (metis ‹∀c∈C. ideal (h ` c) A› image_def)
by (metis (no_types, lifting) h3 subsetD subset_chain_def)
have sub2 :‹((λx. h ` x)`C) ≠ {}›
using h2 by blast
then have f10:‹(⋃((λx. h ` x)`C)) ∈ ((λx. h ` x)`C)›
by (meson h1 noetherian_ring.ideal_chain_is_trivial sub1)
then have f9:‹g ` (⋃((λx. h ` x)`C)) = (⋃C)›
apply(safe)
apply (metis UnionI additive_subgroup.a_Hcarr bij_h f1 h1 h3 ideal.axioms(1) jj1
mem_Collect_eq noetherian_ring_def ring.ring_simprules(6) subset.chain_def subsetD)
by (smt (verit, del_insts) UN_iff h3 image_def inv_imp2 mem_Collect_eq subsetD subset_chain_def)
show ‹⋃C ∈ C›
by (smt (verit, best) f10 f9 h3 image_iff in_mono inv_imp2 subset.chain_def)
qed
lemma (in domain) subring:‹subring (carrier R) R›
using carrier_is_subring by auto
subsection ‹Some properties of the polynomial rings regarding ideals and quotients›
lemma (in domain) gen_is_cgen:‹(genideal ((carrier R)[X]) {X}) = cgenideal ((carrier R)[X]) X›
by (simp add: cring.cgenideal_eq_genideal domain.univ_poly_is_cring domain_axioms subring var_closed(1))
lemma (in domain) principal_X:‹principalideal (genideal ((carrier R)[X]) {X}) ((carrier R)[X])›
apply(subst gen_is_cgen)
by (simp add: cring.cgenideal_is_principalideal domain.univ_poly_is_cring domain_axioms subring var_closed(1))
named_theorems poly
lemma (in ring) PIdl_X[poly]:
‹(cgenideal ((carrier R)[X]) X) = {a⊗⇘(carrier R) [X]⇙X |a. a∈carrier((carrier R)[X])}›
unfolding cgenideal_def by(auto)
lemma (in domain) Idl_X[poly]:
‹(genideal ((carrier R)[X]) {X})= {a⊗⇘(carrier R) [X]⇙X |a. a∈carrier((carrier R)[X])}›
using PIdl_X gen_is_cgen by argo
lemma (in domain) Idl_X_is_X[poly]:
‹p∈(genideal ((carrier R)[X]) {X}) ⟹ ∃a∈carrier((carrier R)[X]). p = a⊗⇘(carrier R) [X]⇙X ›
using gen_is_cgen Idl_X by auto
lemma (in ring) degree_of_nonempty_p[poly]:‹a∈carrier((carrier R)[X]) ∧ a≠[] ⟹ coeff a (degree a) ≠ 𝟬›
by (metis lead_coeff_simp polynomial_def univ_poly_carrier)
lemma (in domain)coeff_0_of_mult_X[poly]:‹a∈carrier((carrier R)[X]) ⟹ coeff (a⊗⇘(carrier R) [X]⇙X) 0 = 𝟬›
apply(cases ‹a=[]›)
apply (simp add: domain.poly_mult_var domain_axioms subring univ_poly_zero_closed)
apply(induct a)
using coeff.simps(1) poly_mult.simps(1)
apply (simp add: univ_poly_mult)
by (simp add: append_coeff poly_mult_var subring)
lemma (in domain)zero_coeff_of_Idl_X[poly]:‹p∈genideal ((carrier R)[X]) {X} ⟹ coeff p 0 = 𝟬›
using Idl_X coeff_0_of_mult_X by auto
lemma (in domain) mult_X_append_0[poly]:‹p∈carrier((carrier R)[X]) ⟹ p≠[] ⟹ poly_mult p X = p@[𝟬]›
using poly_mult_var[of ‹(carrier R)› p]
by(auto simp add: poly_mult_var'(2) polynomial_incl subring univ_poly_carrier univ_poly_mult)
lemma (in ring) polynomial_incl':‹p∈carrier((carrier R)[X]) ⟹ set p ⊆(carrier R)› for p
unfolding univ_poly_def
using polynomial_incl by auto
lemma (in ring) hd_in_carrier:‹p≠ [] ⟹ p∈carrier((carrier R)[X]) ⟹ hd p ∈(carrier R)› for p
using polynomial_incl' unfolding univ_poly_def
using list.set_sel(1) by blast
lemma (in ring) inv_in_carrier:
‹p≠[] ⟹ p∈carrier((carrier R)[X]) ⟹ (inv⇘add_monoid R⇙ (hd p)) ∈(carrier R)› for p
using hd_in_carrier by simp
lemma (in ring) inv_ld_coeff:
‹p≠[] ⟹ p∈carrier((carrier R)[X]) ⟹ (inv⇘add_monoid R⇙ (hd p)#replicate (degree p) 𝟬)∈carrier((carrier R)[X])›
for p
using inv_in_carrier by (metis a_inv_def add.inv_eq_1_iff hd_in_carrier list.sel(1) local.monom_def
monom_in_carrier polynomial_def univ_poly_carrier)
lemma (in ring) take_in_RX:‹p∈carrier((carrier R)[X]) ⟹ n≤length p ⟹ (set (take n p)) ⊆(carrier R)› for p n
using set_take_subset[of n p] polynomial_incl' by blast
lemma (in ring) normalize_take_is_poly:
‹p∈carrier((carrier R)[X]) ⟹ n≤length p ⟹ normalize (take n p) ∈ carrier((carrier R)[X])› for n p
using take_in_RX by (meson normalize_gives_polynomial univ_poly_carrier)
lemma (in ring) normalize_take_is_take:‹p∈carrier((carrier R)[X]) ∧n≤length p ⟹ normalize (take n p) = take n p›
by (metis bot_nat_0.not_eq_extremum degree_of_nonempty_p hd_take lead_coeff_simp
normalize.elims normalize.simps(1) take_eq_Nil)
lemma (in ring) take_in_carrier:‹p∈carrier((carrier R)[X]) ⟹ n≤length p ⟹ (take n p) ∈ carrier((carrier R)[X])›
using normalize_take_is_poly normalize_take_is_take by force
lemma (in domain) take_misc_poly:‹p∈carrier((carrier R)[X]) ⟹ p≠[] ⟹ coeff p 0 = 𝟬 ⟹ ((take (degree p) p))⊗⇘(carrier R) [X]⇙X = p› for p
apply(unfold univ_poly_mult)
apply(cases ‹p=[]›)
subgoal by(simp)
apply(subst mult_X_append_0)
apply (simp add: normalize_take_is_poly univ_poly_carrier)
using normalize_take_is_poly normalize_take_is_take apply force
using degree_of_nonempty_p normalize_take_is_take apply force
by (metis One_nat_def Suc_pred coeff_nth diff_Suc_eq_diff_pred diff_less le_refl
length_greater_0_conv less_one take_Suc_conv_app_nth take_all)
lemma (in ring) length_geq_2:‹normalize p≠[] ∧ ¬(∃a. normalize p=[a]) ⟹ length p ≥ 2› for p::‹'a list›
apply(induct p)
using not_less_eq_eq
by (auto split:if_splits)
lemma (in ring) norm_take_not_mt:‹length (normalize p) ≥ 2 ⟹ normalize (take (degree p) p) ≠ []› for p::‹'a list›
using length_geq_2
apply(induct p rule:normalize.induct)
apply simp
using One_nat_def Suc_eq_plus1 Suc_le_lessD list.sel(3) list.size(3)
list.size(4) nat_less_le normalize.elims numeral_2_eq_2 take_Cons' take_eq_Nil
by (smt (z3) length_tl list.sel(1) normalize.simps(2))
lemma (in ring) normalize_take_invariant:‹p∈carrier((carrier R)[X]) ⟹ p≠[] ⟹ (normalize (take (degree p) p))@[coeff p 0] = p›
for p
apply(subst normalize_take_is_take)
apply simp
by (metis One_nat_def Suc_pred coeff_nth diff_Suc_eq_diff_pred diff_less le_refl
length_greater_0_conv less_one take_Suc_conv_app_nth take_all)
lemma (in domain) lower_coeff_add:‹p≠[] ⟹ p∈carrier((carrier R)[X])∧ b ∈ (carrier R)
⟹ coeff (((normalize p) @[𝟬])⊕⇘(carrier R) [X]⇙ [b]) = coeff ((normalize p) @[b])› for p b
unfolding univ_poly_add
apply(subst poly_add_coeff)
apply (metis local.ring_axioms mult_X_append_0 normalize_polynomial ring.poly_mult_in_carrier
ring.polynomial_in_carrier subring univ_poly_carrier var_closed(2))
by(auto simp add:fun_eq_iff append_coeff polynomial_incl' normalize_polynomial univ_poly_carrier)
lemma (in ring) cons_in_RX:‹a@p∈carrier((carrier R)[X]) ⟹ normalize p∈carrier((carrier R)[X])›
proof -
assume h1:‹a@p∈carrier((carrier R)[X])›
then have ‹set (a@p) ⊆ (carrier R)›
using polynomial_incl' by presburger
then have ‹set p ⊆ (carrier R)›
by simp
then show ?thesis
using normalize_gives_polynomial univ_poly_carrier by blast
qed
lemma (in ring) p_in_norm:‹p∈carrier((carrier R)[X]) ⟹ normalize p = p›
by (simp add: normalize_polynomial univ_poly_carrier)
lemma (in domain) lower_coeff_add':‹p≠[] ⟹ p∈carrier((carrier R)[X])∧ b ∈ (carrier R) ⟹ (((normalize p) @[𝟬])⊕⇘(carrier R) [X]⇙ [b]) = ((normalize p) @[b])› for p b
proof -
interpret kcr:cring "(carrier R)[X]"
using carrier_is_subring univ_poly_is_cring by auto
assume h1:‹p≠[]› ‹p∈carrier((carrier R)[X])∧ b ∈ (carrier R)›
have f0:‹b≠𝟬 ⟹ polynomial (carrier R) p ∧ polynomial (carrier R) [b]›
by (metis h1(2) insert_subset polynomial_incl' list.sel(1) list.simps(15) polynomial_def univ_poly_carrier)
with h1 show ?thesis
apply(cases ‹b=𝟬›)
apply (metis append_self_conv2 domain.mult_X_append_0 domain_axioms kcr.r_zero kcr.zero_closed
polynomial_incl' p_in_norm poly_add_append_zero poly_mult_var'(2) univ_poly_add univ_poly_zero)
unfolding univ_poly_add apply(subst coeff_iff_polynomial_cond[of ‹(carrier R)›])
apply (metis polynomial_incl' mult_X_append_0 normalize_polynomial poly_add_closed poly_mult_is_polynomial subring var_closed(1))
apply (metis (mono_tags, lifting) Un_insert_right append_Nil2 hd_append2 insert_subset
list.simps(15) normalize_polynomial polynomial_def set_append)
by (metis lower_coeff_add univ_poly_add)
qed
lemma (in domain) poly_invariant:‹p∈carrier((carrier R)[X]) ⟹ p≠[] ⟹ ((normalize (take (degree p) p))⊗⇘(carrier R) [X]⇙X ) ⊕⇘(carrier R) [X]⇙ [coeff p 0] = p›
for p
proof -
interpret kcr:cring "(carrier R)[X]"
using carrier_is_subring univ_poly_is_cring by auto
assume h1:‹p ∈ carrier (poly_ring R)› ‹ p ≠ [] ›
with h1 show ?thesis
using take_misc_poly apply(cases ‹p=[]›) apply(simp)
apply(cases ‹∃a. p=[a]›)
apply (metis One_nat_def diff_is_0_eq' kcr.l_zero le_refl lead_coeff_simp length_Cons
list.sel(1) list.size(3) normalize.simps(1) poly_mult.simps(1) take0 univ_poly_mult univ_poly_zero)
unfolding univ_poly_mult
apply(subst mult_X_append_0)
using diff_le_self normalize_take_is_poly apply presburger
using length_geq_2[of p] norm_take_not_mt[of p]
apply (metis coeff_iff_length_cond degree_of_nonempty_p lead_coeff_simp normalize_coeff normalize_length_eq)
by (metis (no_types, lifting) append.right_neutral append_self_conv2 coeff_in_carrier
diff_le_self polynomial_incl' normalize_take_invariant lower_coeff_add' normalize_take_is_poly local.normalize_idem)
qed
lemma (in domain) gen_ideal_X_iff:‹p∈(genideal ((carrier R)[X]) {X}) ⟷ (p∈carrier ((carrier R)[X]) ∧ coeff p 0 = 𝟬)› for p::‹'a list›
using poly take_misc_poly apply(safe)
using domain.univ_poly_is_ring domain_axioms monoid.m_closed ring_def subring var_closed(1)
apply (metis (no_types, lifting))
apply (meson domain.univ_poly_is_ring domain_axioms monoid.m_closed ring_def subring var_closed(1))
by (smt (verit, ccfv_threshold) mem_Collect_eq nat_le_linear poly_mult.simps(1) take_all
take_in_carrier univ_poly_mult)
lemma (in domain) gen_ideal_X_iff':‹(genideal ((carrier R)[X]) {X}) = {p∈carrier ((carrier R)[X]). coeff p 0 = 𝟬}› for p::‹'a list›
using gen_ideal_X_iff by auto
lemma (in domain) quot_X_is_R:‹carrier (((carrier R)[X]) Quot (genideal ((carrier R)[X]) {X}))
= {{x∈carrier((carrier R)[X]). coeff x 0 = a} |a. a∈(carrier R)}›
proof(subst set_eq_subset, safe)
interpret kcr:cring "(carrier R)[X]"
using carrier_is_subring univ_poly_is_cring by auto
fix x
assume h1:‹x ∈ carrier ((carrier R) [X] Quot (genideal ((carrier R)[X]) {X}))›
have l0:‹as≠[] ⟹ take (length as) (a#as) = a#take (degree as) as› for a::'a and as
by (simp add: take_Cons')
have rule_U:‹xaa ∈ (⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa})
= (∃x∈Idl⇘poly_ring R⇙ {X}. xaa = x ⊕⇘poly_ring R⇙ xa)›
for xaa xa
by auto
from h1 have ‹∃xa∈carrier (poly_ring R). x = (⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa})›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def r_coset_def by simp
with h1 show ‹∃a. x = {x ∈ carrier (poly_ring R). local.coeff x 0 = a} ∧ a ∈ carrier R›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def r_coset_def
proof(safe, fold FactRing_def A_RCOSETS_def RCOSETS_def r_coset_def )
fix xa
assume h1:‹(⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa})
∈ carrier (poly_ring R Quot Idl⇘poly_ring R⇙ {X})›
‹xa ∈ carrier (poly_ring R)›
‹x = (⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa})›
‹x ∈ carrier (poly_ring R Quot Idl⇘poly_ring R⇙ {X})›
‹∃xa∈carrier (poly_ring R). x = (⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa})›
show ‹∃a. (⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa}) =
{x ∈ carrier (poly_ring R). local.coeff x 0 = a} ∧
a ∈ carrier R›
proof(rule exI[where x=‹coeff xa 0›], safe)
fix x' xaa
assume h2:‹xaa ∈ Idl⇘poly_ring R⇙ {X}›
with h1 show ‹xaa ⊕⇘poly_ring R⇙ xa ∈ carrier (poly_ring R)›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def r_coset_def
using Idl_X subring var_closed(1) by auto[1]
show ‹local.coeff (xaa ⊕⇘poly_ring R⇙ xa) 0 = local.coeff xa 0›
apply(insert h1 h2)
unfolding FactRing_def A_RCOSETS_def RCOSETS_def r_coset_def
using Idl_X subring var_closed(1) apply(safe)
apply(frule coeff_0_of_mult_X)
apply(frule zero_coeff_of_Idl_X)
apply(subst coeffs_of_add_poly)
using gen_ideal_X_iff apply blast
apply blast
by (simp add: polynomial_incl univ_poly_carrier)
next
fix y
assume h2:‹y ∈ carrier (poly_ring R)›
‹local.coeff y 0 = local.coeff xa 0›
with h1 show ‹y ∈ (⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa})›
apply(subst rule_U)
apply(rule bexI[where x=‹y⊕⇘(carrier R) [X]⇙(inv⇘add_monoid ((carrier R)[X])⇙ xa)›])
apply (metis a_inv_def kcr.add.inv_solve_right' kcr.minus_closed kcr.minus_eq)
by (metis a_inv_def coeff.simps(1) coeffs_of_add_poly gen_ideal_X_iff kcr.add.inv_closed
kcr.add.inv_solve_right kcr.add.m_closed kcr.add.m_lcomm
kcr.r_zero kcr.zero_closed univ_poly_zero)
next
from h1 show ‹local.coeff xa 0 ∈ carrier R›
by (simp add: polynomial_incl univ_poly_carrier)
qed
qed
next
interpret kcr:cring "(carrier R)[X]"
using carrier_is_subring univ_poly_is_cring by auto
fix a
assume h1:‹a ∈ (carrier R)›
have p_h1:‹a≠𝟬 ⟹ [a] ∈ carrier ((carrier R)[X])›
by (metis Diff_iff const_is_polynomial empty_iff h1 insert_iff univ_poly_carrier)
have rule_s:‹{x ∈ carrier (poly_ring R). local.coeff x 0 = a} ∈ carrier (poly_ring R Quot Idl⇘poly_ring R⇙ {X}) =
(∃x∈carrier (poly_ring R).
{x ∈ carrier (poly_ring R). local.coeff x 0 = a} =
(⋃xa∈Idl⇘poly_ring R⇙ {X}. {xa ⊕⇘poly_ring R⇙ x}) )›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def r_coset_def by(auto)
show ‹{x ∈ carrier (poly_ring R). local.coeff x 0 = a}
∈ carrier (poly_ring R Quot Idl⇘poly_ring R⇙ {X})›
apply(subst rule_s)
apply(cases ‹a=𝟬›)
apply(rule bexI[where x=‹[]›])
apply(subst Idl_X) apply(safe)[1]
apply (metis (no_types, lifting) PIdl_X UN_iff gen_ideal_X_iff gen_is_cgen
insert_iff kcr.r_zero univ_poly_zero)
using subring var_closed(1) apply force
apply (metis coeff_0_of_mult_X kcr.m_closed kcr.r_zero subring univ_poly_zero var_closed(1))
apply blast
apply(rule bexI[where x=‹[a]›])
apply(subst Idl_X)
apply(safe)
apply(simp)
apply (metis poly_invariant coeff.simps(1) diff_le_self normalize_take_is_poly)
using h1 subring var_closed(1) p_h1 apply(auto)[1]
apply (metis coeffs_of_add_poly diff_Suc_1 domain.coeff_0_of_mult_X domain.poly_mult_var
domain_axioms kcr.l_zero kcr.m_closed kcr.zero_closed lead_coeff_simp length_Cons
list.distinct(1) list.sel(1) list.size(3) p_h1 subring univ_poly_zero var_closed(1))
using p_h1 by auto
qed
lemma (in domain) uniq_a_quot:
‹c∈ carrier (((carrier R)[X]) Quot (genideal ((carrier R)[X]) {X})) ⟹ ∃!a∈(carrier R). ∀y∈c. coeff y 0 = a›
proof(subst (asm) quot_X_is_R, safe)
fix a
assume h1:‹a ∈ carrier R› ‹c = {x ∈ carrier (poly_ring R). local.coeff x 0 = a}›
then show ‹∃aa. aa ∈ carrier R ∧
(∀y∈{x ∈ carrier (poly_ring R). local.coeff x 0 = a}. local.coeff y 0 = aa)›
apply(intro exI[where x=a])
by fastforce
next
fix a aa y
assume h1:‹a ∈ carrier R› ‹c = {x ∈ carrier (poly_ring R). local.coeff x 0 = a}› ‹aa ∈ carrier R›
‹∀y∈{x ∈ carrier (poly_ring R). local.coeff x 0 = a}. local.coeff y 0 = aa› ‹y ∈ carrier R›
‹∀ya∈{x ∈ carrier (poly_ring R). local.coeff x 0 = a}. local.coeff ya 0 = y›
have ‹{x |x. x ∈ carrier ((carrier R) [X]) ∧ local.coeff x 0 = a} ≠ {}›
apply(subst ex_in_conv[symmetric]) apply(cases ‹a=𝟬›)
apply(rule exI[where x=‹[]›])
apply(fastforce)
apply(rule exI[where x=‹[a]›])
using h1(1) apply(safe)
apply(rule exI[where x=‹[a]›])apply(simp)
by (metis empty_subsetI insert_subset list.sel(1)
list.simps(15) polynomialI set_empty univ_poly_carrier)
then show ‹aa = y›
using h1(4) h1(6) all_not_in_conv[of ‹{x |x. x ∈ carrier (poly_ring R) ∧ local.coeff x 0 = a}›]
by (metis (no_types, lifting))
qed
lemma (in ring) append_in_carrier:‹a∈carrier((carrier R)[X]) ∧ b∈carrier((carrier R)[X]) ⟹ a@b ∈ carrier((carrier R)[X])›
apply(induct b arbitrary:a)
by (metis append_self_conv2 hd_append2 le_sup_iff mem_Collect_eq
partial_object.select_convs(1) polynomial_def set_append univ_poly_def)+
lemma (in domain) The_a_is_a:‹a∈(carrier R) ⟹
(THE aa. ∀y∈{x |x. x ∈ carrier ((carrier R) [X]) ∧ local.coeff x 0 = a}. local.coeff y 0 = aa) = a›
proof -
assume h1:‹a∈(carrier R)›
have ‹∃c ∈ carrier (((carrier R)[X]) Quot (genideal ((carrier R)[X]) {X})).
c = {x |x. x ∈ carrier ((carrier R) [X]) ∧ local.coeff x 0 = a}›
apply(subst quot_X_is_R)
using h1 by auto
then obtain c where f0:‹c = {x |x. x ∈ carrier ((carrier R) [X]) ∧ local.coeff x 0 = a}
∧ c ∈ carrier (((carrier R)[X]) Quot (genideal ((carrier R)[X]) {X}))›
by blast
then have ‹(THE aa. ∀y∈c. local.coeff y 0 = aa) = a›
by (smt (verit, best) coeff.simps(1) h1 mem_Collect_eq theI uniq_a_quot univ_poly_zero_closed zero_closed)
then show ?thesis
by (simp add:f0)
qed
lemma (in ring) poly_mult_in_carrier2:
"⟦ set p1 ⊆ carrier R; set p2 ⊆ carrier R ⟧ ⟹ poly_mult p1 p2 ∈ carrier ((carrier R)[X])"
using poly_mult_is_polynomial polynomial_in_carrier carrier_is_subring
by (simp add: univ_poly_carrier)
lemma (in ring) normalize_equiv:‹polynomial (carrier R) (normalize p) ⟷ (coeff (normalize p)) ∈ carrier (UP R)›
proof(safe)
interpret UP_r: UP_ring R "UP R"
by (simp add: UP_ring_def local.ring_axioms)+
assume ‹polynomial (carrier R) (normalize p)›
then show ‹coeff (normalize p) ∈ carrier (UP R)›
by (meson carrier_is_subring coeff_degree poly_coeff_in_carrier UP_r.UP_car_memI)
next
interpret UP_r: UP_ring R "UP R"
by (simp add: UP_ring_def local.ring_axioms)+
assume ‹coeff (normalize p) ∈ carrier (UP R)›
then show ‹polynomial (carrier R) (normalize p)›
unfolding polynomial_def UP_r.P_def UP_def apply(safe)
using coeff_img_restrict[of ‹(normalize p)›] imageE[of _ ‹coeff (normalize p)› ]
mem_upD[of ‹coeff (normalize p)›] partial_object.select_convs(1)
apply (metis (no_types, lifting))
by (meson ring_axioms polynomial_def ring.normalize_gives_polynomial subsetI)
qed
lemma (in ring) p_in_RX_imp_in_P:‹p∈carrier ((carrier R)[X]) ⟹ coeff p ∈ up R›
by (meson bound.intro coeff_in_carrier coeff_length
linorder_not_less mem_upI nat_le_linear polynomial_incl')
lemma (in ring) X_has_correp:‹coeff X = (λi. if i = 1 then 𝟭 else 𝟬)›
unfolding var_def by(auto)
lemma (in ring) mult_is_mult:
‹{x,y}⊆carrier ((carrier R)[X]) ⟹ coeff (x⊗⇘(carrier R)[X]⇙y) = coeff x ⊗⇘UP R⇙ coeff y›
proof -
interpret UP_r: UP_ring R "UP R"
by (simp add: UP_ring_def local.ring_axioms)+
assume a1: "{x,y}⊆carrier ((carrier R)[X])"
then have a2: "y ∈ carrier (poly_ring R)" "x ∈ carrier (poly_ring R)"
by auto
then have f3: "coeff y ∈ carrier (UP R)"
by (metis p_in_norm normalize_equiv univ_poly_carrier)
have "coeff x ∈ carrier (UP R)"
using a2 by (metis p_in_norm normalize_equiv univ_poly_carrier)
then show ?thesis
unfolding univ_poly_mult
apply(subst poly_mult_coeff)
apply (simp add: polynomial_incl' a2)+
unfolding UP_r.P_def UP_def
using UP_r.p_in_RX_imp_in_P UP_r.UP_ring_axioms a2(1)
by (simp add: local.ring_axioms ring.p_in_RX_imp_in_P)
qed
lemma (in ring) add_is_add:‹x ∈ carrier (poly_ring R) ⟹
y ∈ carrier (poly_ring R)
⟹ coeff (x ⊕⇘poly_ring R⇙ y) = coeff x ⊕⇘UP R⇙ coeff y›
proof -
interpret UP_r: UP_ring R "UP R"
by (simp add: UP_ring_def local.ring_axioms)+
assume a1: "x ∈ carrier (poly_ring R)"
assume a2: "y ∈ carrier (poly_ring R)"
then have f3: "coeff y ∈ carrier (UP R)"
by (metis p_in_norm normalize_equiv univ_poly_carrier)
have "coeff x ∈ carrier (UP R)"
using a1 by (metis p_in_norm normalize_equiv univ_poly_carrier)
then show ?thesis
using f3 a2 a1 UP_r.cfs_add[of ‹coeff x› ‹coeff y›] coeffs_of_add_poly[of x y] by presburger
qed
subsection ‹The isomorphisms between the different models of polynomials›
lemma (in ring) coeff_iso_RX_P:‹coeff ∈ ring_iso (poly_ring R) (UP R)›
proof -
interpret UP_r: UP_ring R "UP R"
by (simp add: UP_ring_def local.ring_axioms)+
{
fix x
assume h1:‹x ∈ carrier (UP R)›
then obtain n::nat where ‹bound 𝟬 n x› using UP_r.P_def unfolding UP_def by auto
then have ‹x≠(λ_. 𝟬) ⟹ ∃n'. ∀m>n'. x m = 𝟬 ∧ x n' ≠ 𝟬›
by (metis UP_ring.coeff_simp UP_r.UP_ring_axioms UP_r.deg_gtE UP_r.deg_nzero_nzero h1 UP_r.lcoeff_nonzero not_gr_zero)
then obtain n'::nat where f5:‹x≠(λ_. 𝟬) ⟹ ∀m>n'. x m = 𝟬 ∧ x n' ≠ 𝟬› by blast
define l::"'a list" where l_is:‹l ≡ rev (map x [0..<Suc n'])›
then have ‹x≠(λ_. 𝟬) ⟹ normalize l = l›
using f5 by(auto)
from l_is have ‹l≠[]›
by simp
then have f6:‹k≤length l - 1 ⟹ coeff l k = l!(length l - 1 - k)› for k
apply(induct l rule:coeff.induct)
using coeff_nth diff_diff_left le_neq_implies_less plus_1_eq_Suc by auto
have gen_ideal_X_iff:‹k≤length g - 1 ⟹ g!k = (rev g) ! (length g -1 - k)› for g::"'a list" and k::nat
apply(induct g)
apply force
by (metis One_nat_def diff_Suc_Suc length_Cons length_rev less_Suc_eq_le minus_nat.diff_0 rev_nth rev_rev_ident)
then have ‹length l - 1 = n'› using l_is by(auto)
then have f9:‹∀n≤n'. x n = coeff l n›
using l_is f6
by (metis add_0 diff_Suc_Suc diff_diff_cancel diff_less_Suc diff_zero l_is length_map length_upt nth_map_upt rev_nth)
then have ‹∀n>n'. coeff l n = 𝟬›
using coeff_degree ‹Polynomials.degree l = n'› by blast
then have f8:‹∀n>n'. x n = coeff l n›
using f5 by(auto)
have f10:‹∀n. x n = coeff l n›
using f8 f9
by (meson linorder_not_less)
then have ‹∃xa∈carrier (poly_ring R). x = coeff xa›
apply(cases ‹x=(λ_. 𝟬)›)
apply(rule bexI[where x=‹[]›])
apply simp
apply (simp add: univ_poly_zero_closed)
apply(rule bexI[where x=l])
apply blast
by (metis ‹x ≠ (λ_. 𝟬) ⟹ normalize l = l› ext h1 mem_Collect_eq
normalize_equiv partial_object.select_convs(1) univ_poly_def)}note subg=this
show ?thesis
unfolding is_ring_iso_def ring_iso_def
apply(safe)
subgoal unfolding ring_hom_def apply(safe)
apply(simp add: local.ring_axioms UP_def ring.p_in_RX_imp_in_P univ_poly_def)
apply (simp add: mult_is_mult)
apply (simp add: add_is_add)
using UP_r.P_def unfolding univ_poly_def UP_def by(simp add:fun_eq_iff)
unfolding bij_betw_def inj_on_def apply(safe)
apply (simp add: coeff_iff_polynomial_cond univ_poly_carrier)
apply (metis normalize_polynomial mem_Collect_eq normalize_equiv partial_object.select_convs(1)
univ_poly_def)
apply(simp add:image_def)
by(simp add:subg)
qed
lemma (in ring) RX_iso_P:‹(carrier R)[X] ≃ (UP R)›
unfolding is_ring_iso_def
using coeff_iso_RX_P by force
lemma (in domain) R_isom_RX_X:‹R ≃ (((carrier R)[X]) Quot (genideal ((carrier R)[X]) {X}))›
proof(unfold is_ring_iso_def, subst ex_in_conv[symmetric])
show ‹∃x. x ∈ ring_iso R ((carrier R) [X] Quot Idl⇘(carrier R) [X]⇙ {X})›
proof(rule exI[where x=‹λx. {y. y∈carrier((carrier R)[X]) ∧ coeff y 0 = x}›], rule ring_iso_memI)
fix x
assume h1:‹x∈(carrier R)›
then show ‹{y ∈ carrier ((carrier R) [X]). local.coeff y 0 = x} ∈ carrier ((carrier R) [X] Quot Idl⇘(carrier R) [X]⇙ {X})›
using quot_X_is_R by auto
next
interpret kcr:cring "(carrier R)[X]"
using carrier_is_subring univ_poly_is_cring by auto
fix x y
assume h1:‹x∈(carrier R)› and h2:‹y∈(carrier R)›
interpret RcR: cring R
by (simp add: is_cring)
interpret QcR: cring ‹(carrier R) [X] Quot Idl⇘(carrier R) [X]⇙ {X}›
by (simp add: ideal.quotient_is_cring kcr.genideal_ideal kcr.is_cring subring var_closed(1))
have left:‹x∈(carrier R) ∧ y∈(carrier R) ⟹ x = 𝟬 ⟹
{ya ∈ carrier ((carrier R) [X]). local.coeff ya 0 = x ⊗ y} =
{y ∈ carrier ((carrier R) [X]). local.coeff y 0 = x}
⊗⇘(carrier R) [X] Quot Idl⇘(carrier R) [X]⇙ {X}⇙ {ya ∈ carrier ((carrier R) [X]). local.coeff ya 0 = y}›
if h3:‹x∈(carrier R) ∧ y∈(carrier R)› for x y
unfolding FactRing_def A_RCOSETS_def RCOSETS_def rcoset_mult_def r_coset_def a_r_coset_def
apply(simp, safe, simp)
apply (metis Diff_iff One_nat_def coeff.simps(1) const_is_polynomial diff_self_eq_0 empty_iff
gen_ideal_X_iff insert_iff kcr.l_null kcr.r_zero lead_coeff_simp length_Cons list.distinct(1) list.sel(1)
list.size(3) univ_poly_carrier univ_poly_zero univ_poly_zero_closed )
using gen_ideal_X_iff apply blast
unfolding univ_poly_mult univ_poly_add
apply(frule zero_coeff_of_Idl_X)
apply(subst (asm) Idl_X)
using h3
by (metis (no_types, lifting) PIdl_X coeffs_of_add_poly gen_ideal_X_iff gen_is_cgen ideal.I_l_closed
kcr.cgenideal_ideal kcr.m_comm l_zero subring univ_poly_add univ_poly_mult var_closed(1))
have right :‹y = 𝟬 ⟹ {ya ∈ carrier ((carrier R) [X]). local.coeff ya 0 = x ⊗ y} =
{y ∈ carrier ((carrier R) [X]). local.coeff y 0 = x} ⊗⇘(carrier R) [X] Quot Idl⇘(carrier R) [X]⇙ {X}⇙
{ya ∈ carrier ((carrier R) [X]). local.coeff ya 0 = y}›
apply(subst m_comm[OF h1 h2])
apply(subst QcR.m_comm)
using h1 quot_X_is_R left h1 by auto
have poly_mult_a_b:‹a∈(carrier R) ∧ b∈(carrier R) ∧ a≠𝟬 ∧ b≠𝟬 ⟹ poly_mult ([a]) ([b]) = [a⊗b]› for a b
using integral_iff by force
have poly_mult_0:‹a∈carrier((carrier R)[X]) ∧ b∈carrier((carrier R)[X]) ⟹ coeff (poly_mult a b) 0 = coeff a 0 ⊗ coeff b 0›
for a b
apply(subst poly_mult_coeff)
by (simp add: polynomial_incl')+
have j0:‹xa ∈ carrier (poly_ring R) ⟹ local.coeff xa 0 = x ⊗ y ⟹ x ≠ 𝟬 ⟹ y ≠ 𝟬
⟹ ∃xb. xb ∈ carrier (poly_ring R) ∧ local.coeff xb 0 = x ∧ (∃x. x ∈ carrier (poly_ring R) ∧
local.coeff x 0 = y ∧ (∃xc∈Idl⇘poly_ring R⇙ {X}. xa = xc ⊕⇘poly_ring R⇙ xb ⊗⇘poly_ring R⇙ x))›
for xa
apply(rule exI[where x=‹[x]›])
apply(safe)
subgoal by (metis Diff_iff const_is_polynomial empty_iff h1 insert_iff univ_poly_carrier)
subgoal by simp
apply(rule exI[where x=‹[y]›])
apply(safe)
subgoal by (metis Diff_iff const_is_polynomial empty_iff h2 insert_iff univ_poly_carrier)
subgoal by simp
apply(rule bexI[where x=‹normalize (take (degree xa) xa @[𝟬])›])
unfolding univ_poly_add univ_poly_mult
apply(subst poly_mult_a_b)
subgoal using h1 h2 by(simp)
subgoal by (metis (no_types, lifting) diff_le_self
domain.coeff_0_of_mult_X domain.m_lcancel domain.poly_mult_var domain_axioms h1 h2
poly_invariant take_in_RX normalize_take_is_take poly_mult_var'(2) r_null subring univ_poly_add
univ_poly_mult zero_closed)
apply(subst Idl_X)
by (metis (no_types, lifting) PIdl_X coeff_0_of_mult_X diff_le_self gen_ideal_X_iff gen_is_cgen
kcr.m_closed take_in_RX poly_mult_var'(2) subring take_in_carrier univ_poly_mult var_closed(1))
show fst:‹{ya ∈ carrier ((carrier R) [X]). local.coeff ya 0 = x ⊗ y} =
{y ∈ carrier ((carrier R) [X]). local.coeff y 0 = x} ⊗⇘(carrier R) [X] Quot Idl⇘(carrier R) [X]⇙ {X}⇙
{ya ∈ carrier ((carrier R) [X]). local.coeff ya 0 = y}›
proof(safe)
fix xa
assume h1:‹xa ∈ carrier (poly_ring R)› ‹local.coeff xa 0 = x ⊗ y›
then show ‹xa ∈ {y ∈ carrier (poly_ring R). local.coeff y 0 = x} ⊗⇘poly_ring R Quot Idl⇘poly_ring R⇙ {X}⇙
{ya ∈ carrier (poly_ring R). local.coeff ya 0 = y}›
apply(cases ‹x=𝟬 ∨ y=𝟬›)
using h2 left right apply blast
unfolding FactRing_def A_RCOSETS_def RCOSETS_def rcoset_mult_def r_coset_def a_r_coset_def
using j0 by(auto) [1]
next
fix xa
assume h1':‹xa ∈ {y ∈ carrier (poly_ring R). local.coeff y 0 = x} ⊗⇘poly_ring R Quot Idl⇘poly_ring R⇙ {X}⇙
{ya ∈ carrier (poly_ring R). local.coeff ya 0 = y}›
then show ‹xa ∈ carrier (poly_ring R)›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def rcoset_mult_def r_coset_def a_r_coset_def
by simp (metis gen_ideal_X_iff kcr.add.m_closed kcr.m_closed univ_poly_add univ_poly_mult)
from h1' show ‹local.coeff xa 0 = x ⊗ y›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def rcoset_mult_def r_coset_def a_r_coset_def
apply(simp, safe)
apply(frule zero_coeff_of_Idl_X)
apply (simp add: polynomial_incl' domain_axioms gen_ideal_X_iff)
using polynomial_incl' poly_mult_in_carrier
by (metis coeffs_of_add_poly h1 h2 kcr.m_closed l_distr l_null l_zero poly_mult_0 univ_poly_mult zero_closed)
qed
have poly_add_a_b:‹a∈(carrier R) ∧ b∈(carrier R) ∧ a≠𝟬 ∧ b≠𝟬 ⟹ poly_add ([a]) ([b]) = normalize [a⊕b]› for a b
by(auto)
have is_inv_0:‹local.normalize [inv⇘add_monoid R⇙ y ⊕ y] = []›
by (simp add: h2)
have poly_add_comm: ‹{x,y,z}⊆carrier ((carrier R)[X]) ⟹poly_add (poly_add y z) x = poly_add y (poly_add z x) › for x y z
by (metis insert_subset kcr.add.m_assoc univ_poly_add)
show ‹{ya ∈ carrier ((carrier R) [X]). local.coeff ya 0 = x ⊕ y} =
{y ∈ carrier ((carrier R) [X]). local.coeff y 0 = x} ⊕⇘(carrier R) [X] Quot Idl⇘(carrier R) [X]⇙ {X}⇙
{ya ∈ carrier ((carrier R) [X]). local.coeff ya 0 = y}›
proof(safe)
fix xa
assume h1':‹xa ∈ carrier (poly_ring R)›‹local.coeff xa 0 = x ⊕ y ›
then show ‹xa ∈ {y ∈ carrier (poly_ring R). local.coeff y 0 = x} ⊕⇘poly_ring R Quot Idl⇘poly_ring R⇙ {X}⇙
{ya ∈ carrier (poly_ring R). local.coeff ya 0 = y}›
apply(cases ‹x=𝟬 ∨ y=𝟬›)
unfolding FactRing_def A_RCOSETS_def RCOSETS_def rcoset_mult_def r_coset_def a_r_coset_def
set_add_def set_mult_def apply(simp, safe)[1]
apply (metis coeff.simps(1) h2 kcr.l_zero l_zero univ_poly_zero univ_poly_zero_closed)
apply (metis coeff.simps(1) h1 kcr.r_zero r_zero univ_poly_zero univ_poly_zero_closed)
unfolding FactRing_def A_RCOSETS_def RCOSETS_def rcoset_mult_def r_coset_def a_r_coset_def
set_add_def set_mult_def apply(simp)
apply(rule exI[where x=‹xa ⊕⇘(carrier R) [X]⇙ [inv⇘add_monoid R⇙ y]›])
apply(safe)
apply (metis a_inv_def add.Units_eq add.Units_inv_closed add.inv_eq_1_iff h2 insert_subset
kcr.add.m_closed list.sel(1) list.simps(15) polynomial_def polynomial_incl univ_poly_carrier)
apply (metis (no_types, lifting) a_assoc add.Units_eq add.Units_inv_closed add.Units_r_inv
coeffs_of_add_poly diff_Suc_1 h1 h2 insert_subset polynomial_incl' lead_coeff_simp length_Cons list.distinct(1) list.sel(1) list.simps(15) list.size(3) mem_Collect_eq partial_object.select_convs(1) polynomial_def r_zero univ_poly_def)
apply(rule exI[where x=‹[y]›])
apply(safe) apply(simp add:h2 univ_poly_def polynomial_def)
apply(simp)
apply(cases xa)
unfolding univ_poly_add
using add.Units_eq add.inv_eq_one_eq add.Units_inv_closed add.Units_l_inv h2 r_zero apply(auto)[1]
apply(subst poly_add_comm)
apply (metis Diff_iff One_nat_def append.right_neutral const_is_polynomial diff_self_eq_0
empty_iff empty_subsetI h2 insert_iff insert_subset inv_ld_coeff length_Cons list.distinct(1) list.sel(1)
list.size(3) normalize.simps(1) normalize_trick univ_poly_carrier)
apply(subst poly_add_a_b)
apply(simp add:h2 add.inv_eq_one_eq)
apply(subst is_inv_0)
by (metis polynomial_incl' p_in_norm poly_add_zero'(1))
next
fix xa
assume h1':‹xa ∈ {y ∈ carrier (poly_ring R). local.coeff y 0 = x} ⊕⇘poly_ring R Quot Idl⇘poly_ring R⇙ {X}⇙
{ya ∈ carrier (poly_ring R). local.coeff ya 0 = y} ›
then show ‹xa ∈ carrier (poly_ring R)›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def rcoset_mult_def r_coset_def a_r_coset_def
set_add_def set_mult_def by(auto)
from h1' show ‹local.coeff xa 0 = x ⊕ y›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def rcoset_mult_def r_coset_def a_r_coset_def
set_add_def set_mult_def using polynomial_incl' poly_add_coeff coeffs_of_add_poly by auto
qed
next
interpret kcr:cring "(carrier R)[X]"
using carrier_is_subring univ_poly_is_cring by auto
show ‹{y ∈ carrier ((carrier R) [X]). local.coeff y 0 = 𝟭} = 𝟭⇘(carrier R) [X] Quot Idl⇘(carrier R) [X]⇙ {X}⇙›
unfolding FactRing_def a_r_coset_def r_coset_def
using gen_ideal_X_iff apply(simp, safe, simp)
apply (metis (no_types, lifting) diff_le_self domain.coeff_0_of_mult_X
domain.poly_mult_var domain_axioms gen_ideal_X_iff kcr.m_closed poly_invariant normalize_take_is_poly monoid.simps(2) subring univ_poly_def
var_closed(1) zero_not_one)
apply force
by (metis One_nat_def coeff.simps(1) coeffs_of_add_poly diff_self_eq_0 kcr.l_zero kcr.one_closed
lead_coeff_simp length_Cons list.distinct(1) list.sel(1) list.size(3) univ_poly_one univ_poly_zero
univ_poly_zero_closed)
next
interpret kcr:cring "(carrier R)[X]"
using carrier_is_subring univ_poly_is_cring by auto
have rule_1:‹{y ∈ carrier (poly_ring R). local.coeff y 0 = xa} ∈ carrier (poly_ring R Quot Idl⇘poly_ring R⇙ {X}) =
(∃x∈carrier (poly_ring R). {y ∈ carrier (poly_ring R). local.coeff y 0 = xa} = (⋃xa∈Idl⇘poly_ring R⇙ {X}. {xa ⊕⇘poly_ring R⇙ x}))› for xa
unfolding FactRing_def A_RCOSETS_def RCOSETS_def r_coset_def by(auto)
have rule_2:‹(⋀x. x ∈ carrier (poly_ring R Quot Idl⇘poly_ring R⇙ {X}) ⟹
x ∈ (λx. {y ∈ carrier (poly_ring R). local.coeff y 0 = x}) ` carrier R)
⟹ (⋀xa. xa ∈ carrier (poly_ring R) ⟹
(⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa}) ∈ (λx. {y ∈ carrier (poly_ring R). local.coeff y 0 = x}) ` carrier R)›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def r_coset_def
using UN_singleton by auto
have rule_2':‹ (⋀xa. xa ∈ carrier (poly_ring R) ⟹
(⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa}) ∈ (λx. {y ∈ carrier (poly_ring R). local.coeff y 0 = x}) ` carrier R)
⟹ (⋀x. x ∈ carrier (poly_ring R Quot Idl⇘poly_ring R⇙ {X}) ⟹
x ∈ (λx. {y ∈ carrier (poly_ring R). local.coeff y 0 = x}) ` carrier R)›
unfolding FactRing_def A_RCOSETS_def RCOSETS_def r_coset_def
using UN_singleton by auto
show ‹bij_betw (λx. {y ∈ carrier ((carrier R) [X]). local.coeff y 0 = x}) (carrier R) (carrier ((carrier R) [X] Quot Idl⇘(carrier R) [X]⇙ {X}))›
unfolding bij_betw_def
apply(safe)
apply(rule inj_onI)
subgoal proof -
fix x :: 'a and y :: 'a
assume a1: "x ∈ (carrier R)"
assume a2: "y ∈ (carrier R)"
assume "{y ∈ carrier ((carrier R) [X]). local.coeff y 0 = x} = {ya ∈ carrier ((carrier R) [X]). local.coeff ya 0 = y}"
then have "y = (THE a. ∀as. as ∈ {as ∈ carrier ((carrier R) [X]). local.coeff as 0 = x} ⟶ local.coeff as 0 = a)"
using a2 The_a_is_a by force
then show "x = y"
using a1 The_a_is_a by auto
qed
proof(subst rule_1)
fix x xa
have rule_1:‹x' ∈ (⋃xa∈{p ∈ carrier (poly_ring R). local.coeff p 0 = 𝟬}. {xa ⊕⇘poly_ring R⇙ [local.coeff x' 0]}) =
(∃xa. xa ∈ carrier (poly_ring R) ∧ local.coeff xa 0 = 𝟬 ∧ x' = xa ⊕⇘poly_ring R⇙ [local.coeff x' 0])› for x'
by simp
assume h1':‹xa ∈ carrier R›
then show ‹∃x∈carrier (poly_ring R).
{y ∈ carrier (poly_ring R). local.coeff y 0 = xa} = (⋃xa∈Idl⇘poly_ring R⇙ {X}. {xa ⊕⇘poly_ring R⇙ x})›
apply(cases ‹xa=𝟬›)
apply(rule bexI[where x=‹[]›])
using gen_ideal_X_iff kcr.r_zero univ_poly_zero apply(safe)[1]
apply (simp add: univ_poly_zero)+
apply (simp add: univ_poly_zero_closed)
apply(rule bexI[where x=‹[xa]›])
apply(subst gen_ideal_X_iff')
apply(safe)
apply(subst rule_1)
apply (metis coeff.simps(1) coeff_0_of_mult_X diff_le_self kcr.m_closed
normalize_take_is_poly poly_invariant subring var_closed(1))
apply (metis bot_least insert_subset list.simps(15) poly_add_is_polynomial polynomial_incl'
set_empty2 subring univ_poly_add univ_poly_carrier)
apply (metis diff_Suc_1 insert_subset kcr.zero_closed l_zero lead_coeff_simp length_Cons
list.distinct(1) list.sel(1) list.simps(15) list.size(3) poly_add_coeff polynomial_incl' univ_poly_add univ_poly_zero)
by (metis Diff_iff const_is_polynomial emptyE insertE univ_poly_carrier)
next
show ‹⋀x. x ∈ carrier (poly_ring R Quot Idl⇘poly_ring R⇙ {X})
⟹ x ∈ (λx. {y ∈ carrier (poly_ring R). local.coeff y 0 = x}) ` carrier R›
proof(rule rule_2')
fix x xa
assume h1:‹x ∈ carrier (poly_ring R Quot Idl⇘poly_ring R⇙ {X})› ‹xa ∈ carrier (poly_ring R)›
then show ‹(⋃x∈Idl⇘poly_ring R⇙ {X}. {x ⊕⇘poly_ring R⇙ xa})
∈ (λx. {y ∈ carrier (poly_ring R). local.coeff y 0 = x}) ` carrier R›
apply(simp only:image_def, safe)
apply(rule bexI[where x=‹coeff xa 0›])
apply(safe)
by(auto simp:gen_ideal_X_iff coeffs_of_add_poly domain_axioms polynomial_incl')
(metis coeff.simps(1) coeffs_of_add_poly gen_ideal_X_iff insertI1 kcr.add.inv_closed
kcr.add.inv_solve_right kcr.add.m_comm kcr.l_neg kcr.minus_closed kcr.minus_eq univ_poly_zero)+
qed
qed
qed
qed
lemma (in domain) RX_imp_RX_over_X:
‹noetherian_ring (carrier R[X]) ⟹ noetherian_ring (carrier R[X] Quot genideal (carrier R[X]) {X})›
by (meson domain.var_closed(1) domain_axioms empty_subsetI insert_subset noetherian_ring_def
noetherian_ring_imp_quot_noetherian_ring ring.genideal_ideal subring)
lemma (in domain) noetherian_RX_imp_noetherian_R:
‹noetherian_ring ((carrier R)[X]) ⟹ noetherian_ring R›
proof -
assume h1:‹noetherian_ring ((carrier R)[X])›
have ‹noetherian_ring (((carrier R)[X]) Quot (genideal ((carrier R)[X]) {X}))›
using RX_imp_RX_over_X h1 by auto
moreover have ‹(((carrier R)[X]) Quot (genideal ((carrier R)[X]) {X})) ≃ R›
using R_isom_RX_X local.ring_axioms ring_iso_sym by blast
ultimately show ?thesis
using local.ring_axioms noetherian_isom_imp_noetherian by blast
qed
lemma principal_imp_noetherian:‹principal_domain R ⟹ noetherian_ring R›
proof -
assume h1:‹principal_domain R›
then show ?thesis
apply(intro ring.noetherian_ringI)
using cring.axioms(1) domain_def principal_domain.axioms(1) apply blast
by (metis cring.cgenideal_eq_genideal domain_def empty_subsetI finite.emptyI finite.insertI
insert_subset principal_domain.axioms(1) principal_domain.exists_gen)
qed
lemma (in ring) coeff_iff_poly_carrier:‹x ∈ carrier (poly_ring R) ⟹
y ∈ carrier (poly_ring R) ⟹ (x=y) ⟷ coeff x = coeff y›
by (auto simp add: coeff_iff_polynomial_cond univ_poly_carrier)
lemma zero_is_zero:‹B = B⦇zero := 𝟬⇘B⇙⦈›
unfolding ring_def monoid_def ring_axioms_def abelian_group_def abelian_group_axioms_def
abelian_monoid_def comm_monoid_def by(auto)
lemma ring_iso_imp_iso:‹A≃B ⟹ A≅B›
unfolding is_ring_iso_def is_iso_def ring_iso_def iso_def
ring_hom_def hom_def by(auto)
lemma (in ring) iso_imp_exist_0:‹R≃B ⟹ ∃x. ring (B⦇zero:=x⦈)›
proof -
assume h1:‹R≃B›
have ‹ring R›
by (simp add: local.ring_axioms)
with h1 obtain h where f0:‹h ∈ ring_hom R B ∧ bij_betw h (carrier R) (carrier B)›
unfolding is_ring_iso_def ring_iso_def by auto
then have f1:"ring (B ⦇ carrier := h ` (carrier R), zero := h 𝟬⇘R⇙ ⦈)"
using ring_hom_imp_img_ring[of ] h1 unfolding ring_iso_def
using ring.ring_hom_imp_img_ring by blast
moreover have f2:"h ` (carrier R) = carrier B"
using h1 unfolding ring_iso_def bij_betw_def
by (simp add: f0 bij_betw_imp_surj_on)
then show ?thesis using f1 f2 by(auto)
qed
lemma (in domain) noetherian_R_imp_noetherian_UP_R:
assumes h1:‹noetherian_ring R›
shows ‹noetherian_ring (UP R)›
proof -
interpret UPring: UP_ring R "UP R"
by (simp add: UP_ring_def local.ring_axioms)+
have ‹noetherian_ring ((carrier R)[X])›
using noetherian_domain.weak_Hilbert_basis h1
using domain_axioms noetherian_domain.intro by auto
with h1 show ?thesis
unfolding noetherian_domain_def
using ‹noetherian_ring (poly_ring R)› noetherian_isom_imp_noetherian h1 UPring.UP_ring RX_iso_P
by blast
qed
lemma (in domain) noetheriandom_R_imp_noetheriandom_UP_R:
assumes h1:‹noetherian_domain R›
shows ‹noetherian_domain (UP R)›
proof -
interpret UP_dom: UP_domain R "UP R"
by (simp add: UP_domain.intro domain_axioms)+
have ‹noetherian_ring ((carrier R)[X])›
using noetherian_domain.weak_Hilbert_basis h1
by(auto)
with h1 show ?thesis
unfolding noetherian_domain_def
using UP_dom.domain_axioms noetherian_R_imp_noetherian_UP_R by blast
qed
lemma (in cring) Pring_one_index_isom_P:‹(Pring R {N}) ≃ UP R›
proof -
interpret UPcring: UP_cring R "UP R"
by (simp add: UP_cring_def is_cring)+
have ‹IP_to_UP N ∈ ring_hom (Pring R {N}) (UP R)›
by (simp add: UPcring.IP_to_UP_ring_hom ring_hom_ring.homh)
then show ?thesis unfolding is_ring_iso_def ring_iso_def
apply(subst ex_in_conv[symmetric])
apply(rule exI[where x=‹IP_to_UP N›])
unfolding bij_betw_def apply(safe)
apply (simp add: UPcring.IP_to_UP_ring_hom_inj)
apply (simp add: IP_to_UP_closed is_cring)
by (metis UPcring.IP_to_UP_inv UPcring.UP_to_IP_closed image_eqI)
qed
lemma (in cring) P_isom_Pring_one_index: ‹UP R ≃ (Pring R {N})›
proof -
interpret UPcring: UP_cring R "UP R"
by (simp add: UP_cring_def is_cring)+
interpret crR:cring "Pring R {N}"
by (simp add: Pring_is_cring is_cring)
show ?thesis
using cring.Pring_one_index_isom_P crR.ring_axioms ring_iso_sym is_cring by fastforce
qed
lemma (in domain) P_iso_RX:‹ UP R ≃ ((carrier R)[X])›
proof -
interpret d: domain "(carrier R)[X]"
by (simp add: subring univ_poly_is_domain)
have ‹(carrier R)[X] ≃ UP R›
using RX_iso_P UP_ring_def local.ring_axioms by blast
then show ?thesis
using d.ring_axioms ring_iso_sym by blast
qed
lemma (in domain) IP_noeth_imp_R_noeth:‹noetherian_ring (Pring R {a}) ⟹ noetherian_ring R›
proof -
assume h1:‹noetherian_ring (Pring R {a})›
have ‹(Pring R {a}) ≃ ((carrier R)[X])›
by (meson Pring_one_index_isom_P domain.P_iso_RX domain_axioms ring_iso_trans)
then have ‹noetherian_ring ((carrier R)[X])›
using domain.univ_poly_is_ring domain_axioms h1 noetherian_isom_imp_noetherian subring by blast
then show ?thesis
using noetherian_RX_imp_noetherian_R by fastforce
qed
lemma (in domain) R_iso_UPR_quot_X:‹R ≃ (UP R) Quot (cgenideal (UP R) (λi. if i=1 then 𝟭 else 𝟬))›
proof -
interpret UP_r: UP_ring R "UP R"
by (simp add: UP_ring_def local.ring_axioms)+
have f0:‹coeff ∈ ring_iso (poly_ring R) (UP R)›
using coeff_iso_RX_P by blast
have ‹X ∈ carrier (poly_ring R)› ‹(λi. if i = 1 then 𝟭 else 𝟬) ∈ carrier (UP R)›
‹cring (poly_ring R)› ‹cring (UP R)›
apply (simp add: subring var_closed(1))
apply(force simp:UP_def up_def)
apply (simp add: subring univ_poly_is_cring)
by (simp add: UP_cring.UP_cring UP_cring.intro is_cring)
then have ‹(carrier R[X]) Quot (cgenideal (poly_ring R) X) ≃(UP R) Quot (cgenideal (UP R) (λi. if i=1 then 𝟭 else 𝟬))›
using Quot_iso_cgen[of X ‹poly_ring R› ‹(λi. if i=1 then 𝟭 else 𝟬)› ‹(UP R)› coeff] X_has_correp
f0 by fastforce
then show ?thesis
using domain.R_isom_RX_X domain_axioms gen_is_cgen ring_iso_trans by force
qed
end