(* Title: HOL/Algebra/Ideal.thy
Author: Stephan Hohe, TU Muenchen
*)
theory Ideal
imports Ring AbelCoset
begin
section \Ideals\
subsection \Definitions\
subsubsection \General definition\
locale ideal = additive_subgroup I R + ring R for I and R (structure) +
assumes I_l_closed: "\a \ I; x \ carrier R\ \ x \ a \ I"
and I_r_closed: "\a \ I; x \ carrier R\ \ a \ x \ I"
sublocale ideal \ abelian_subgroup I R
apply (intro abelian_subgroupI3 abelian_group.intro)
apply (rule ideal.axioms, rule ideal_axioms)
apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
done
lemma (in ideal) is_ideal: "ideal I R"
by (rule ideal_axioms)
lemma idealI:
fixes R (structure)
assumes "ring R"
assumes a_subgroup: "subgroup I \carrier = carrier R, mult = add R, one = zero R\"
and I_l_closed: "\a x. \a \ I; x \ carrier R\ \ x \ a \ I"
and I_r_closed: "\a x. \a \ I; x \ carrier R\ \ a \ x \ I"
shows "ideal I R"
proof -
interpret ring R by fact
show ?thesis apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
apply (rule a_subgroup)
apply (rule is_ring)
apply (erule (1) I_l_closed)
apply (erule (1) I_r_closed)
done
qed
subsubsection (in ring) \Ideals Generated by a Subset of @{term "carrier R"}\
definition genideal :: "_ \ 'a set \ 'a set" ("Idl\ _" [80] 79)
where "genideal R S = Inter {I. ideal I R \ S \ I}"
subsubsection \Principal Ideals\
locale principalideal = ideal +
assumes generate: "\i \ carrier R. I = Idl {i}"
lemma (in principalideal) is_principalideal: "principalideal I R"
by (rule principalideal_axioms)
lemma principalidealI:
fixes R (structure)
assumes "ideal I R"
and generate: "\i \ carrier R. I = Idl {i}"
shows "principalideal I R"
proof -
interpret ideal I R by fact
show ?thesis
by (intro principalideal.intro principalideal_axioms.intro)
(rule is_ideal, rule generate)
qed
subsubsection \Maximal Ideals\
locale maximalideal = ideal +
assumes I_notcarr: "carrier R \ I"
and I_maximal: "\ideal J R; I \ J; J \ carrier R\ \ J = I \ J = carrier R"
lemma (in maximalideal) is_maximalideal: "maximalideal I R"
by (rule maximalideal_axioms)
lemma maximalidealI:
fixes R
assumes "ideal I R"
and I_notcarr: "carrier R \ I"
and I_maximal: "\J. \ideal J R; I \ J; J \ carrier R\ \ J = I \ J = carrier R"
shows "maximalideal I R"
proof -
interpret ideal I R by fact
show ?thesis
by (intro maximalideal.intro maximalideal_axioms.intro)
(rule is_ideal, rule I_notcarr, rule I_maximal)
qed
subsubsection \Prime Ideals\
locale primeideal = ideal + cring +
assumes I_notcarr: "carrier R \ I"
and I_prime: "\a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I"
lemma (in primeideal) is_primeideal: "primeideal I R"
by (rule primeideal_axioms)
lemma primeidealI:
fixes R (structure)
assumes "ideal I R"
and "cring R"
and I_notcarr: "carrier R \ I"
and I_prime: "\a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I"
shows "primeideal I R"
proof -
interpret ideal I R by fact
interpret cring R by fact
show ?thesis
by (intro primeideal.intro primeideal_axioms.intro)
(rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
qed
lemma primeidealI2:
fixes R (structure)
assumes "additive_subgroup I R"
and "cring R"
and I_l_closed: "\a x. \a \ I; x \ carrier R\ \ x \ a \ I"
and I_r_closed: "\a x. \a \ I; x \ carrier R\ \ a \ x \ I"
and I_notcarr: "carrier R \ I"
and I_prime: "\a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I"
shows "primeideal I R"
proof -
interpret additive_subgroup I R by fact
interpret cring R by fact
show ?thesis apply (intro_locales)
apply (intro ideal_axioms.intro)
apply (erule (1) I_l_closed)
apply (erule (1) I_r_closed)
apply (intro primeideal_axioms.intro)
apply (rule I_notcarr)
apply (erule (2) I_prime)
done
qed
subsection \Special Ideals\
lemma (in ring) zeroideal: "ideal {\} R"
apply (intro idealI subgroup.intro)
apply (rule is_ring)
apply simp+
apply (fold a_inv_def, simp)
apply simp+
done
lemma (in ring) oneideal: "ideal (carrier R) R"
by (rule idealI) (auto intro: is_ring add.subgroupI)
lemma (in "domain") zeroprimeideal: "primeideal {\} R"
apply (intro primeidealI)
apply (rule zeroideal)
apply (rule domain.axioms, rule domain_axioms)
defer 1
apply (simp add: integral)
proof (rule ccontr, simp)
assume "carrier R = {\}"
then have "\ = \" by (rule one_zeroI)
with one_not_zero show False by simp
qed
subsection \General Ideal Properies\
lemma (in ideal) one_imp_carrier:
assumes I_one_closed: "\ \ I"
shows "I = carrier R"
apply (rule)
apply (rule)
apply (rule a_Hcarr, simp)
proof
fix x
assume xcarr: "x \ carrier R"
with I_one_closed have "x \ \ \ I" by (intro I_l_closed)
with xcarr show "x \ I" by simp
qed
lemma (in ideal) Icarr:
assumes iI: "i \ I"
shows "i \ carrier R"
using iI by (rule a_Hcarr)
subsection \Intersection of Ideals\
text \\paragraph{Intersection of two ideals} The intersection of any
two ideals is again an ideal in @{term R}\
lemma (in ring) i_intersect:
assumes "ideal I R"
assumes "ideal J R"
shows "ideal (I \ J) R"
proof -
interpret ideal I R by fact
interpret ideal J R by fact
show ?thesis
apply (intro idealI subgroup.intro)
apply (rule is_ring)
apply (force simp add: a_subset)
apply (simp add: a_inv_def[symmetric])
apply simp
apply (simp add: a_inv_def[symmetric])
apply (clarsimp, rule)
apply (fast intro: ideal.I_l_closed ideal.intro assms)+
apply (clarsimp, rule)
apply (fast intro: ideal.I_r_closed ideal.intro assms)+
done
qed
text \The intersection of any Number of Ideals is again
an Ideal in @{term R}\
lemma (in ring) i_Intersect:
assumes Sideals: "\I. I \ S \ ideal I R"
and notempty: "S \ {}"
shows "ideal (Inter S) R"
apply (unfold_locales)
apply (simp_all add: Inter_eq)
apply rule unfolding mem_Collect_eq defer 1
apply rule defer 1
apply rule defer 1
apply (fold a_inv_def, rule) defer 1
apply rule defer 1
apply rule defer 1
proof -
fix x y
assume "\I\S. x \ I"
then have xI: "\I. I \ S \ x \ I" by simp
assume "\I\S. y \ I"
then have yI: "\I. I \ S \ y \ I" by simp
fix J
assume JS: "J \ S"
interpret ideal J R by (rule Sideals[OF JS])
from xI[OF JS] and yI[OF JS] show "x \ y \ J" by (rule a_closed)
next
fix J
assume JS: "J \ S"
interpret ideal J R by (rule Sideals[OF JS])
show "\ \ J" by simp
next
fix x
assume "\I\S. x \ I"
then have xI: "\I. I \ S \ x \ I" by simp
fix J
assume JS: "J \ S"
interpret ideal J R by (rule Sideals[OF JS])
from xI[OF JS] show "\ x \ J" by (rule a_inv_closed)
next
fix x y
assume "\I\S. x \ I"
then have xI: "\I. I \ S \ x \ I" by simp
assume ycarr: "y \ carrier R"
fix J
assume JS: "J \ S"
interpret ideal J R by (rule Sideals[OF JS])
from xI[OF JS] and ycarr show "y \ x \ J" by (rule I_l_closed)
next
fix x y
assume "\I\S. x \ I"
then have xI: "\I. I \ S \ x \ I" by simp
assume ycarr: "y \ carrier R"
fix J
assume JS: "J \ S"
interpret ideal J R by (rule Sideals[OF JS])
from xI[OF JS] and ycarr show "x \ y \ J" by (rule I_r_closed)
next
fix x
assume "\I\S. x \ I"
then have xI: "\I. I \ S \ x \ I" by simp
from notempty have "\I0. I0 \ S" by blast
then obtain I0 where I0S: "I0 \ S" by auto
interpret ideal I0 R by (rule Sideals[OF I0S])
from xI[OF I0S] have "x \ I0" .
with a_subset show "x \ carrier R" by fast
next
qed
subsection \Addition of Ideals\
lemma (in ring) add_ideals:
assumes idealI: "ideal I R"
and idealJ: "ideal J R"
shows "ideal (I <+> J) R"
apply (rule ideal.intro)
apply (rule add_additive_subgroups)
apply (intro ideal.axioms[OF idealI])
apply (intro ideal.axioms[OF idealJ])
apply (rule is_ring)
apply (rule ideal_axioms.intro)
apply (simp add: set_add_defs, clarsimp) defer 1
apply (simp add: set_add_defs, clarsimp) defer 1
proof -
fix x i j
assume xcarr: "x \ carrier R"
and iI: "i \ I"
and jJ: "j \ J"
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
have c: "(i \ j) \ x = (i \ x) \ (j \ x)"
by algebra
from xcarr and iI have a: "i \ x \ I"
by (simp add: ideal.I_r_closed[OF idealI])
from xcarr and jJ have b: "j \ x \ J"
by (simp add: ideal.I_r_closed[OF idealJ])
from a b c show "\ha\I. \ka\J. (i \ j) \ x = ha \ ka"
by fast
next
fix x i j
assume xcarr: "x \ carrier R"
and iI: "i \ I"
and jJ: "j \ J"
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
have c: "x \ (i \ j) = (x \ i) \ (x \ j)" by algebra
from xcarr and iI have a: "x \ i \ I"
by (simp add: ideal.I_l_closed[OF idealI])
from xcarr and jJ have b: "x \ j \ J"
by (simp add: ideal.I_l_closed[OF idealJ])
from a b c show "\ha\I. \ka\J. x \ (i \ j) = ha \ ka"
by fast
qed
subsection (in ring) \