(* 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\<index> _" [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 {\<zero>} 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 {\<zero>} 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 = {\<zero>}" then have "\<one> = \<zero>" 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: "\<one> ∈ 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 ⊗ \<one> ∈ 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 "\<zero> ∈ 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 "\<ominus> 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) {* Ideals generated by a subset of @{term "carrier R"} *} text {* @{term genideal} generates an ideal *} lemma (in ring) genideal_ideal: assumes Scarr: "S ⊆ carrier R" shows "ideal (Idl S) R" unfolding genideal_def proof (rule i_Intersect, fast, simp) from oneideal and Scarr show "∃I. ideal I R ∧ S ≤ I" by fast qed lemma (in ring) genideal_self: assumes "S ⊆ carrier R" shows "S ⊆ Idl S" unfolding genideal_def by fast lemma (in ring) genideal_self': assumes carr: "i ∈ carrier R" shows "i ∈ Idl {i}" proof - from carr have "{i} ⊆ Idl {i}" by (fast intro!: genideal_self) then show "i ∈ Idl {i}" by fast qed text {* @{term genideal} generates the minimal ideal *} lemma (in ring) genideal_minimal: assumes a: "ideal I R" and b: "S ⊆ I" shows "Idl S ⊆ I" unfolding genideal_def by rule (elim InterD, simp add: a b) text {* Generated ideals and subsets *} lemma (in ring) Idl_subset_ideal: assumes Iideal: "ideal I R" and Hcarr: "H ⊆ carrier R" shows "(Idl H ⊆ I) = (H ⊆ I)" proof assume a: "Idl H ⊆ I" from Hcarr have "H ⊆ Idl H" by (rule genideal_self) with a show "H ⊆ I" by simp next fix x assume "H ⊆ I" with Iideal have "I ∈ {I. ideal I R ∧ H ⊆ I}" by fast then show "Idl H ⊆ I" unfolding genideal_def by fast qed lemma (in ring) subset_Idl_subset: assumes Icarr: "I ⊆ carrier R" and HI: "H ⊆ I" shows "Idl H ⊆ Idl I" proof - from HI and genideal_self[OF Icarr] have HIdlI: "H ⊆ Idl I" by fast from Icarr have Iideal: "ideal (Idl I) R" by (rule genideal_ideal) from HI and Icarr have "H ⊆ carrier R" by fast with Iideal have "(H ⊆ Idl I) = (Idl H ⊆ Idl I)" by (rule Idl_subset_ideal[symmetric]) with HIdlI show "Idl H ⊆ Idl I" by simp qed lemma (in ring) Idl_subset_ideal': assumes acarr: "a ∈ carrier R" and bcarr: "b ∈ carrier R" shows "(Idl {a} ⊆ Idl {b}) = (a ∈ Idl {b})" apply (subst Idl_subset_ideal[OF genideal_ideal[of "{b}"], of "{a}"]) apply (fast intro: bcarr, fast intro: acarr) apply fast done lemma (in ring) genideal_zero: "Idl {\<zero>} = {\<zero>}" apply rule apply (rule genideal_minimal[OF zeroideal], simp) apply (simp add: genideal_self') done lemma (in ring) genideal_one: "Idl {\<one>} = carrier R" proof - interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal) fast show "Idl {\<one>} = carrier R" apply (rule, rule a_subset) apply (simp add: one_imp_carrier genideal_self') done qed text {* Generation of Principal Ideals in Commutative Rings *} definition cgenideal :: "_ => 'a => 'a set" ("PIdl\<index> _" [80] 79) where "cgenideal R a = {x ⊗⇘_{R⇙}a | x. x ∈ carrier R}" text {* genhideal (?) really generates an ideal *} lemma (in cring) cgenideal_ideal: assumes acarr: "a ∈ carrier R" shows "ideal (PIdl a) R" apply (unfold cgenideal_def) apply (rule idealI[OF is_ring]) apply (rule subgroup.intro) apply simp_all apply (blast intro: acarr) apply clarsimp defer 1 defer 1 apply (fold a_inv_def, clarsimp) defer 1 apply clarsimp defer 1 apply clarsimp defer 1 proof - fix x y assume xcarr: "x ∈ carrier R" and ycarr: "y ∈ carrier R" note carr = acarr xcarr ycarr from carr have "x ⊗ a ⊕ y ⊗ a = (x ⊕ y) ⊗ a" by (simp add: l_distr) with carr show "∃z. x ⊗ a ⊕ y ⊗ a = z ⊗ a ∧ z ∈ carrier R" by fast next from l_null[OF acarr, symmetric] and zero_closed show "∃x. \<zero> = x ⊗ a ∧ x ∈ carrier R" by fast next fix x assume xcarr: "x ∈ carrier R" note carr = acarr xcarr from carr have "\<ominus> (x ⊗ a) = (\<ominus> x) ⊗ a" by (simp add: l_minus) with carr show "∃z. \<ominus> (x ⊗ a) = z ⊗ a ∧ z ∈ carrier R" by fast next fix x y assume xcarr: "x ∈ carrier R" and ycarr: "y ∈ carrier R" note carr = acarr xcarr ycarr from carr have "y ⊗ a ⊗ x = (y ⊗ x) ⊗ a" by (simp add: m_assoc) (simp add: m_comm) with carr show "∃z. y ⊗ a ⊗ x = z ⊗ a ∧ z ∈ carrier R" by fast next fix x y assume xcarr: "x ∈ carrier R" and ycarr: "y ∈ carrier R" note carr = acarr xcarr ycarr from carr have "x ⊗ (y ⊗ a) = (x ⊗ y) ⊗ a" by (simp add: m_assoc) with carr show "∃z. x ⊗ (y ⊗ a) = z ⊗ a ∧ z ∈ carrier R" by fast qed lemma (in ring) cgenideal_self: assumes icarr: "i ∈ carrier R" shows "i ∈ PIdl i" unfolding cgenideal_def proof simp from icarr have "i = \<one> ⊗ i" by simp with icarr show "∃x. i = x ⊗ i ∧ x ∈ carrier R" by fast qed text {* @{const "cgenideal"} is minimal *} lemma (in ring) cgenideal_minimal: assumes "ideal J R" assumes aJ: "a ∈ J" shows "PIdl a ⊆ J" proof - interpret ideal J R by fact show ?thesis unfolding cgenideal_def apply rule apply clarify using aJ apply (erule I_l_closed) done qed lemma (in cring) cgenideal_eq_genideal: assumes icarr: "i ∈ carrier R" shows "PIdl i = Idl {i}" apply rule apply (intro cgenideal_minimal) apply (rule genideal_ideal, fast intro: icarr) apply (rule genideal_self', fast intro: icarr) apply (intro genideal_minimal) apply (rule cgenideal_ideal [OF icarr]) apply (simp, rule cgenideal_self [OF icarr]) done lemma (in cring) cgenideal_eq_rcos: "PIdl i = carrier R #> i" unfolding cgenideal_def r_coset_def by fast lemma (in cring) cgenideal_is_principalideal: assumes icarr: "i ∈ carrier R" shows "principalideal (PIdl i) R" apply (rule principalidealI) apply (rule cgenideal_ideal [OF icarr]) proof - from icarr have "PIdl i = Idl {i}" by (rule cgenideal_eq_genideal) with icarr show "∃i'∈carrier R. PIdl i = Idl {i'}" by fast qed subsection {* Union of Ideals *} lemma (in ring) union_genideal: assumes idealI: "ideal I R" and idealJ: "ideal J R" shows "Idl (I ∪ J) = I <+> J" apply rule apply (rule ring.genideal_minimal) apply (rule is_ring) apply (rule add_ideals[OF idealI idealJ]) apply (rule) apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1 apply (rule) apply (simp add: set_add_defs genideal_def) apply clarsimp defer 1 proof - fix x assume xI: "x ∈ I" have ZJ: "\<zero> ∈ J" by (intro additive_subgroup.zero_closed) (rule ideal.axioms[OF idealJ]) from ideal.Icarr[OF idealI xI] have "x = x ⊕ \<zero>" by algebra with xI and ZJ show "∃h∈I. ∃k∈J. x = h ⊕ k" by fast next fix x assume xJ: "x ∈ J" have ZI: "\<zero> ∈ I" by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealI]) from ideal.Icarr[OF idealJ xJ] have "x = \<zero> ⊕ x" by algebra with ZI and xJ show "∃h∈I. ∃k∈J. x = h ⊕ k" by fast next fix i j K assume iI: "i ∈ I" and jJ: "j ∈ J" and idealK: "ideal K R" and IK: "I ⊆ K" and JK: "J ⊆ K" from iI and IK have iK: "i ∈ K" by fast from jJ and JK have jK: "j ∈ K" by fast from iK and jK show "i ⊕ j ∈ K" by (intro additive_subgroup.a_closed) (rule ideal.axioms[OF idealK]) qed subsection {* Properties of Principal Ideals *} text {* @{text "\<zero>"} generates the zero ideal *} lemma (in ring) zero_genideal: "Idl {\<zero>} = {\<zero>}" apply rule apply (simp add: genideal_minimal zeroideal) apply (fast intro!: genideal_self) done text {* @{text "\<one>"} generates the unit ideal *} lemma (in ring) one_genideal: "Idl {\<one>} = carrier R" proof - have "\<one> ∈ Idl {\<one>}" by (simp add: genideal_self') then show "Idl {\<one>} = carrier R" by (intro ideal.one_imp_carrier) (fast intro: genideal_ideal) qed text {* The zero ideal is a principal ideal *} corollary (in ring) zeropideal: "principalideal {\<zero>} R" apply (rule principalidealI) apply (rule zeroideal) apply (blast intro!: zero_genideal[symmetric]) done text {* The unit ideal is a principal ideal *} corollary (in ring) onepideal: "principalideal (carrier R) R" apply (rule principalidealI) apply (rule oneideal) apply (blast intro!: one_genideal[symmetric]) done text {* Every principal ideal is a right coset of the carrier *} lemma (in principalideal) rcos_generate: assumes "cring R" shows "∃x∈I. I = carrier R #> x" proof - interpret cring R by fact from generate obtain i where icarr: "i ∈ carrier R" and I1: "I = Idl {i}" by fast+ from icarr and genideal_self[of "{i}"] have "i ∈ Idl {i}" by fast then have iI: "i ∈ I" by (simp add: I1) from I1 icarr have I2: "I = PIdl i" by (simp add: cgenideal_eq_genideal) have "PIdl i = carrier R #> i" unfolding cgenideal_def r_coset_def by fast with I2 have "I = carrier R #> i" by simp with iI show "∃x∈I. I = carrier R #> x" by fast qed subsection {* Prime Ideals *} lemma (in ideal) primeidealCD: assumes "cring R" assumes notprime: "¬ primeideal I R" shows "carrier R = I ∨ (∃a b. a ∈ carrier R ∧ b ∈ carrier R ∧ a ⊗ b ∈ I ∧ a ∉ I ∧ b ∉ I)" proof (rule ccontr, clarsimp) interpret cring R by fact assume InR: "carrier R ≠ I" and "∀a. a ∈ carrier R --> (∀b. a ⊗ b ∈ I --> b ∈ carrier R --> a ∈ I ∨ b ∈ I)" then have I_prime: "!! a b. [|a ∈ carrier R; b ∈ carrier R; a ⊗ b ∈ I|] ==> a ∈ I ∨ b ∈ I" by simp have "primeideal I R" apply (rule primeideal.intro [OF is_ideal is_cring]) apply (rule primeideal_axioms.intro) apply (rule InR) apply (erule (2) I_prime) done with notprime show False by simp qed lemma (in ideal) primeidealCE: assumes "cring R" assumes notprime: "¬ primeideal I R" obtains "carrier R = I" | "∃a b. a ∈ carrier R ∧ b ∈ carrier R ∧ a ⊗ b ∈ I ∧ a ∉ I ∧ b ∉ I" proof - interpret R: cring R by fact assume "carrier R = I ==> thesis" and "∃a b. a ∈ carrier R ∧ b ∈ carrier R ∧ a ⊗ b ∈ I ∧ a ∉ I ∧ b ∉ I ==> thesis" then show thesis using primeidealCD [OF R.is_cring notprime] by blast qed text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *} lemma (in cring) zeroprimeideal_domainI: assumes pi: "primeideal {\<zero>} R" shows "domain R" apply (rule domain.intro, rule is_cring) apply (rule domain_axioms.intro) proof (rule ccontr, simp) interpret primeideal "{\<zero>}" "R" by (rule pi) assume "\<one> = \<zero>" then have "carrier R = {\<zero>}" by (rule one_zeroD) from this[symmetric] and I_notcarr show False by simp next interpret primeideal "{\<zero>}" "R" by (rule pi) fix a b assume ab: "a ⊗ b = \<zero>" and carr: "a ∈ carrier R" "b ∈ carrier R" from ab have abI: "a ⊗ b ∈ {\<zero>}" by fast with carr have "a ∈ {\<zero>} ∨ b ∈ {\<zero>}" by (rule I_prime) then show "a = \<zero> ∨ b = \<zero>" by simp qed corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\<zero>} R" apply rule apply (erule domain.zeroprimeideal) apply (erule zeroprimeideal_domainI) done subsection {* Maximal Ideals *} lemma (in ideal) helper_I_closed: assumes carr: "a ∈ carrier R" "x ∈ carrier R" "y ∈ carrier R" and axI: "a ⊗ x ∈ I" shows "a ⊗ (x ⊗ y) ∈ I" proof - from axI and carr have "(a ⊗ x) ⊗ y ∈ I" by (simp add: I_r_closed) also from carr have "(a ⊗ x) ⊗ y = a ⊗ (x ⊗ y)" by (simp add: m_assoc) finally show "a ⊗ (x ⊗ y) ∈ I" . qed lemma (in ideal) helper_max_prime: assumes "cring R" assumes acarr: "a ∈ carrier R" shows "ideal {x∈carrier R. a ⊗ x ∈ I} R" proof - interpret cring R by fact show ?thesis apply (rule idealI) apply (rule cring.axioms[OF is_cring]) apply (rule subgroup.intro) apply (simp, fast) apply clarsimp apply (simp add: r_distr acarr) apply (simp add: acarr) apply (simp add: a_inv_def[symmetric], clarify) defer 1 apply clarsimp defer 1 apply (fast intro!: helper_I_closed acarr) proof - fix x assume xcarr: "x ∈ carrier R" and ax: "a ⊗ x ∈ I" from ax and acarr xcarr have "\<ominus>(a ⊗ x) ∈ I" by simp also from acarr xcarr have "\<ominus>(a ⊗ x) = a ⊗ (\<ominus>x)" by algebra finally show "a ⊗ (\<ominus>x) ∈ I" . from acarr have "a ⊗ \<zero> = \<zero>" by simp next fix x y assume xcarr: "x ∈ carrier R" and ycarr: "y ∈ carrier R" and ayI: "a ⊗ y ∈ I" from ayI and acarr xcarr ycarr have "a ⊗ (y ⊗ x) ∈ I" by (simp add: helper_I_closed) moreover from xcarr ycarr have "y ⊗ x = x ⊗ y" by (simp add: m_comm) ultimately show "a ⊗ (x ⊗ y) ∈ I" by simp qed qed text {* In a cring every maximal ideal is prime *} lemma (in cring) maximalideal_is_prime: assumes "maximalideal I R" shows "primeideal I R" proof - interpret maximalideal I R by fact show ?thesis apply (rule ccontr) apply (rule primeidealCE) apply (rule is_cring) apply assumption apply (simp add: I_notcarr) proof - assume "∃a b. a ∈ carrier R ∧ b ∈ carrier R ∧ a ⊗ b ∈ I ∧ a ∉ I ∧ b ∉ I" then obtain a b where acarr: "a ∈ carrier R" and bcarr: "b ∈ carrier R" and abI: "a ⊗ b ∈ I" and anI: "a ∉ I" and bnI: "b ∉ I" by fast def J ≡ "{x∈carrier R. a ⊗ x ∈ I}" from is_cring and acarr have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime) have IsubJ: "I ⊆ J" proof fix x assume xI: "x ∈ I" with acarr have "a ⊗ x ∈ I" by (intro I_l_closed) with xI[THEN a_Hcarr] show "x ∈ J" unfolding J_def by fast qed from abI and acarr bcarr have "b ∈ J" unfolding J_def by fast with bnI have JnI: "J ≠ I" by fast from acarr have "a = a ⊗ \<one>" by algebra with anI have "a ⊗ \<one> ∉ I" by simp with one_closed have "\<one> ∉ J" unfolding J_def by fast then have Jncarr: "J ≠ carrier R" by fast interpret ideal J R by (rule idealJ) have "J = I ∨ J = carrier R" apply (intro I_maximal) apply (rule idealJ) apply (rule IsubJ) apply (rule a_subset) done with JnI and Jncarr show False by simp qed qed subsection {* Derived Theorems *} --"A non-zero cring that has only the two trivial ideals is a field" lemma (in cring) trivialideals_fieldI: assumes carrnzero: "carrier R ≠ {\<zero>}" and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}" shows "field R" apply (rule cring_fieldI) apply (rule, rule, rule) apply (erule Units_closed) defer 1 apply rule defer 1 proof (rule ccontr, simp) assume zUnit: "\<zero> ∈ Units R" then have a: "\<zero> ⊗ inv \<zero> = \<one>" by (rule Units_r_inv) from zUnit have "\<zero> ⊗ inv \<zero> = \<zero>" by (intro l_null) (rule Units_inv_closed) with a[symmetric] have "\<one> = \<zero>" by simp then have "carrier R = {\<zero>}" by (rule one_zeroD) with carrnzero show False by simp next fix x assume xcarr': "x ∈ carrier R - {\<zero>}" then have xcarr: "x ∈ carrier R" by fast from xcarr' have xnZ: "x ≠ \<zero>" by fast from xcarr have xIdl: "ideal (PIdl x) R" by (intro cgenideal_ideal) fast from xcarr have "x ∈ PIdl x" by (intro cgenideal_self) fast with xnZ have "PIdl x ≠ {\<zero>}" by fast with haveideals have "PIdl x = carrier R" by (blast intro!: xIdl) then have "\<one> ∈ PIdl x" by simp then have "∃y. \<one> = y ⊗ x ∧ y ∈ carrier R" unfolding cgenideal_def by blast then obtain y where ycarr: " y ∈ carrier R" and ylinv: "\<one> = y ⊗ x" by fast+ from ylinv and xcarr ycarr have yrinv: "\<one> = x ⊗ y" by (simp add: m_comm) from ycarr and ylinv[symmetric] and yrinv[symmetric] have "∃y ∈ carrier R. y ⊗ x = \<one> ∧ x ⊗ y = \<one>" by fast with xcarr show "x ∈ Units R" unfolding Units_def by fast qed lemma (in field) all_ideals: "{I. ideal I R} = {{\<zero>}, carrier R}" apply (rule, rule) proof - fix I assume a: "I ∈ {I. ideal I R}" then interpret ideal I R by simp show "I ∈ {{\<zero>}, carrier R}" proof (cases "∃a. a ∈ I - {\<zero>}") case True then obtain a where aI: "a ∈ I" and anZ: "a ≠ \<zero>" by fast+ from aI[THEN a_Hcarr] anZ have aUnit: "a ∈ Units R" by (simp add: field_Units) then have a: "a ⊗ inv a = \<one>" by (rule Units_r_inv) from aI and aUnit have "a ⊗ inv a ∈ I" by (simp add: I_r_closed del: Units_r_inv) then have oneI: "\<one> ∈ I" by (simp add: a[symmetric]) have "carrier R ⊆ I" proof fix x assume xcarr: "x ∈ carrier R" with oneI have "\<one> ⊗ x ∈ I" by (rule I_r_closed) with xcarr show "x ∈ I" by simp qed with a_subset have "I = carrier R" by fast then show "I ∈ {{\<zero>}, carrier R}" by fast next case False then have IZ: "!!a. a ∈ I ==> a = \<zero>" by simp have a: "I ⊆ {\<zero>}" proof fix x assume "x ∈ I" then have "x = \<zero>" by (rule IZ) then show "x ∈ {\<zero>}" by fast qed have "\<zero> ∈ I" by simp then have "{\<zero>} ⊆ I" by fast with a have "I = {\<zero>}" by fast then show "I ∈ {{\<zero>}, carrier R}" by fast qed qed (simp add: zeroideal oneideal) --"Jacobson Theorem 2.2" lemma (in cring) trivialideals_eq_field: assumes carrnzero: "carrier R ≠ {\<zero>}" shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R" by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals) text {* Like zeroprimeideal for domains *} lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R" apply (rule maximalidealI) apply (rule zeroideal) proof- from one_not_zero have "\<one> ∉ {\<zero>}" by simp with one_closed show "carrier R ≠ {\<zero>}" by fast next fix J assume Jideal: "ideal J R" then have "J ∈ {I. ideal I R}" by fast with all_ideals show "J = {\<zero>} ∨ J = carrier R" by simp qed lemma (in cring) zeromaximalideal_fieldI: assumes zeromax: "maximalideal {\<zero>} R" shows "field R" apply (rule trivialideals_fieldI, rule maximalideal.I_notcarr[OF zeromax]) apply rule apply clarsimp defer 1 apply (simp add: zeroideal oneideal) proof - fix J assume Jn0: "J ≠ {\<zero>}" and idealJ: "ideal J R" interpret ideal J R by (rule idealJ) have "{\<zero>} ⊆ J" by (rule ccontr) simp from zeromax and idealJ and this and a_subset have "J = {\<zero>} ∨ J = carrier R" by (rule maximalideal.I_maximal) with Jn0 show "J = carrier R" by simp qed lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\<zero>} R = field R" apply rule apply (erule zeromaximalideal_fieldI) apply (erule field.zeromaximalideal) done end