(* 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 = ⋂{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) 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› paragraph ‹Intersection of two ideals› text ‹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 (⋂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) ‹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 {𝟬} = {𝟬}" apply rule apply (rule genideal_minimal[OF zeroideal], simp) apply (simp add: genideal_self') done lemma (in ring) genideal_one: "Idl {𝟭} = carrier R" proof - interpret ideal "Idl {𝟭}" "R" by (rule genideal_ideal) fast show "Idl {𝟭} = 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ı _" [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. 𝟬 = x ⊗ a ∧ x ∈ carrier R" by fast next fix x assume xcarr: "x ∈ carrier R" note carr = acarr xcarr from carr have "⊖ (x ⊗ a) = (⊖ x) ⊗ a" by (simp add: l_minus) with carr show "∃z. ⊖ (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 = 𝟭 ⊗ 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: "𝟬 ∈ J" by (intro additive_subgroup.zero_closed) (rule ideal.axioms[OF idealJ]) from ideal.Icarr[OF idealI xI] have "x = x ⊕ 𝟬" 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: "𝟬 ∈ I" by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealI]) from ideal.Icarr[OF idealJ xJ] have "x = 𝟬 ⊕ 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 ‹‹𝟬› generates the zero ideal› lemma (in ring) zero_genideal: "Idl {𝟬} = {𝟬}" apply rule apply (simp add: genideal_minimal zeroideal) apply (fast intro!: genideal_self) done text ‹‹𝟭› generates the unit ideal› lemma (in ring) one_genideal: "Idl {𝟭} = carrier R" proof - have "𝟭 ∈ Idl {𝟭}" by (simp add: genideal_self') then show "Idl {𝟭} = 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 {𝟬} 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 ‹{𝟬}› is a prime ideal of a commutative ring, the ring is a domain› lemma (in cring) zeroprimeideal_domainI: assumes pi: "primeideal {𝟬} R" shows "domain R" apply (rule domain.intro, rule is_cring) apply (rule domain_axioms.intro) proof (rule ccontr, simp) interpret primeideal "{𝟬}" "R" by (rule pi) assume "𝟭 = 𝟬" then have "carrier R = {𝟬}" by (rule one_zeroD) from this[symmetric] and I_notcarr show False by simp next interpret primeideal "{𝟬}" "R" by (rule pi) fix a b assume ab: "a ⊗ b = 𝟬" and carr: "a ∈ carrier R" "b ∈ carrier R" from ab have abI: "a ⊗ b ∈ {𝟬}" by fast with carr have "a ∈ {𝟬} ∨ b ∈ {𝟬}" by (rule I_prime) then show "a = 𝟬 ∨ b = 𝟬" by simp qed corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {𝟬} 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 "⊖(a ⊗ x) ∈ I" by simp also from acarr xcarr have "⊖(a ⊗ x) = a ⊗ (⊖x)" by algebra finally show "a ⊗ (⊖x) ∈ I" . from acarr have "a ⊗ 𝟬 = 𝟬" 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_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 define J where "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 ⊗ 𝟭" by algebra with anI have "a ⊗ 𝟭 ∉ I" by simp with one_closed have "𝟭 ∉ 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 ≠ {𝟬}" and haveideals: "{I. ideal I R} = {{𝟬}, 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: "𝟬 ∈ Units R" then have a: "𝟬 ⊗ inv 𝟬 = 𝟭" by (rule Units_r_inv) from zUnit have "𝟬 ⊗ inv 𝟬 = 𝟬" by (intro l_null) (rule Units_inv_closed) with a[symmetric] have "𝟭 = 𝟬" by simp then have "carrier R = {𝟬}" by (rule one_zeroD) with carrnzero show False by simp next fix x assume xcarr': "x ∈ carrier R - {𝟬}" then have xcarr: "x ∈ carrier R" by fast from xcarr' have xnZ: "x ≠ 𝟬" 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 ≠ {𝟬}" by fast with haveideals have "PIdl x = carrier R" by (blast intro!: xIdl) then have "𝟭 ∈ PIdl x" by simp then have "∃y. 𝟭 = y ⊗ x ∧ y ∈ carrier R" unfolding cgenideal_def by blast then obtain y where ycarr: " y ∈ carrier R" and ylinv: "𝟭 = y ⊗ x" by fast+ from ylinv and xcarr ycarr have yrinv: "𝟭 = x ⊗ y" by (simp add: m_comm) from ycarr and ylinv[symmetric] and yrinv[symmetric] have "∃y ∈ carrier R. y ⊗ x = 𝟭 ∧ x ⊗ y = 𝟭" by fast with xcarr show "x ∈ Units R" unfolding Units_def by fast qed lemma (in field) all_ideals: "{I. ideal I R} = {{𝟬}, carrier R}" apply (rule, rule) proof - fix I assume a: "I ∈ {I. ideal I R}" then interpret ideal I R by simp show "I ∈ {{𝟬}, carrier R}" proof (cases "∃a. a ∈ I - {𝟬}") case True then obtain a where aI: "a ∈ I" and anZ: "a ≠ 𝟬" by fast+ from aI[THEN a_Hcarr] anZ have aUnit: "a ∈ Units R" by (simp add: field_Units) then have a: "a ⊗ inv a = 𝟭" 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: "𝟭 ∈ I" by (simp add: a[symmetric]) have "carrier R ⊆ I" proof fix x assume xcarr: "x ∈ carrier R" with oneI have "𝟭 ⊗ 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 ∈ {{𝟬}, carrier R}" by fast next case False then have IZ: "⋀a. a ∈ I ⟹ a = 𝟬" by simp have a: "I ⊆ {𝟬}" proof fix x assume "x ∈ I" then have "x = 𝟬" by (rule IZ) then show "x ∈ {𝟬}" by fast qed have "𝟬 ∈ I" by simp then have "{𝟬} ⊆ I" by fast with a have "I = {𝟬}" by fast then show "I ∈ {{𝟬}, carrier R}" by fast qed qed (simp add: zeroideal oneideal) ―"Jacobson Theorem 2.2" lemma (in cring) trivialideals_eq_field: assumes carrnzero: "carrier R ≠ {𝟬}" shows "({I. ideal I R} = {{𝟬}, carrier R}) = field R" by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals) text ‹Like zeroprimeideal for domains› lemma (in field) zeromaximalideal: "maximalideal {𝟬} R" apply (rule maximalidealI) apply (rule zeroideal) proof- from one_not_zero have "𝟭 ∉ {𝟬}" by simp with one_closed show "carrier R ≠ {𝟬}" by fast next fix J assume Jideal: "ideal J R" then have "J ∈ {I. ideal I R}" by fast with all_ideals show "J = {𝟬} ∨ J = carrier R" by simp qed lemma (in cring) zeromaximalideal_fieldI: assumes zeromax: "maximalideal {𝟬} 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 ≠ {𝟬}" and idealJ: "ideal J R" interpret ideal J R by (rule idealJ) have "{𝟬} ⊆ J" by (rule ccontr) simp from zeromax and idealJ and this and a_subset have "J = {𝟬} ∨ J = carrier R" by (rule maximalideal.I_maximal) with Jn0 show "J = carrier R" by simp qed lemma (in cring) zeromaximalideal_eq_field: "maximalideal {𝟬} R = field R" apply rule apply (erule zeromaximalideal_fieldI) apply (erule field.zeromaximalideal) done end