(* 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 proof (intro abelian_subgroupI3 abelian_group.intro) show "additive_subgroup I R" by (simp add: is_additive_subgroup) show "abelian_monoid R" by (simp add: abelian_monoid_axioms) show "abelian_group_axioms R" using abelian_group_def is_abelian_group by blast qed 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 (add_monoid 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 by (auto simp: ideal.intro ideal_axioms.intro additive_subgroupI a_subgroup is_ring I_l_closed I_r_closed) 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) by (simp add: I_notcarr I_prime primeideal_axioms.intro) qed subsection ‹Special Ideals› lemma (in ring) zeroideal: "ideal {𝟬} R" by (intro idealI subgroup.intro) (simp_all add: is_ring) lemma (in ring) oneideal: "ideal (carrier R) R" by (rule idealI) (auto intro: is_ring add.subgroupI) lemma (in "domain") zeroprimeideal: "primeideal {𝟬} R" proof - have "carrier R ≠ {𝟬}" by (simp add: carrier_one_not_zero) then show ?thesis by (metis (no_types, lifting) domain_axioms domain_def integral primeidealI singleton_iff zeroideal) qed subsection ‹General Ideal Properies› lemma (in ideal) one_imp_carrier: assumes I_one_closed: "𝟭 ∈ I" shows "I = carrier R" proof show "carrier R ⊆ I" using I_r_closed assms by fastforce show "I ⊆ carrier R" by (rule a_subset) 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 have IJ: "I ∩ J ⊆ carrier R" by (force simp: a_subset) show ?thesis apply (intro idealI subgroup.intro) apply (simp_all add: IJ is_ring I_l_closed assms ideal.I_l_closed ideal.I_r_closed flip: a_inv_def) 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" proof - { fix x y J assume "∀I∈S. x ∈ I" "∀I∈S. y ∈ I" and JS: "J ∈ S" interpret ideal J R by (rule Sideals[OF JS]) have "x ⊕ y ∈ J" by (simp add: JS ‹∀I∈S. x ∈ I› ‹∀I∈S. y ∈ I›) } moreover have "𝟬 ∈ J" if "J ∈ S" for J by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1)) moreover { fix x J assume "∀I∈S. x ∈ I" and JS: "J ∈ S" interpret ideal J R by (rule Sideals[OF JS]) have "⊖ x ∈ J" by (simp add: JS ‹∀I∈S. x ∈ I›) } moreover { fix x y J assume "∀I∈S. x ∈ I" and ycarr: "y ∈ carrier R" and JS: "J ∈ S" interpret ideal J R by (rule Sideals[OF JS]) have "y ⊗ x ∈ J" "x ⊗ y ∈ J" using I_l_closed I_r_closed JS ‹∀I∈S. x ∈ I› ycarr by blast+ } moreover { fix x assume "∀I∈S. x ∈ I" obtain I0 where I0S: "I0 ∈ S" using notempty by blast interpret ideal I0 R by (rule Sideals[OF I0S]) have "x ∈ I0" by (simp add: I0S ‹∀I∈S. x ∈ I›) with a_subset have "x ∈ carrier R" by fast } ultimately show ?thesis by unfold_locales (auto simp: Inter_eq simp flip: a_inv_def) 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" proof (rule ideal.intro) show "additive_subgroup (I <+> J) R" by (intro ideal.axioms[OF idealI] ideal.axioms[OF idealJ] add_additive_subgroups) show "ring R" by (rule is_ring) show "ideal_axioms (I <+> J) R" 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 "∃h∈I. ∃k∈J. (i ⊕ j) ⊗ x = h ⊕ k" by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI) } moreover { 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 "∃h∈I. ∃k∈J. x ⊗ (i ⊕ j) = h ⊕ k" by (meson iI ideal.I_l_closed idealJ jJ local.idealI r_distr) } ultimately show "ideal_axioms (I <+> J) R" by (intro ideal_axioms.intro) (auto simp: set_add_defs) qed 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}" by (simp add: genideal_def) text ‹@{term genideal} generates the minimal ideal› lemma (in ring) genideal_minimal: assumes "ideal I R" "S ⊆ I" shows "Idl S ⊆ I" unfolding genideal_def by rule (elim InterD, simp add: assms) 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 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]) then show "Idl H ⊆ Idl I" by (meson HI Icarr genideal_self order_trans) 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}" proof - have "Idl {a} ⊆ Idl {b} ⟷ {a} ⊆ Idl {b}" by (simp add: Idl_subset_ideal acarr bcarr genideal_ideal) also have "… ⟷ a ∈ Idl {b}" by blast finally show ?thesis . qed lemma (in ring) genideal_zero: "Idl {𝟬} = {𝟬}" proof show "Idl {𝟬} ⊆ {𝟬}" by (simp add: genideal_minimal zeroideal) show "{𝟬} ⊆ Idl {𝟬}" by (simp add: genideal_self') qed lemma (in ring) genideal_one: "Idl {𝟭} = carrier R" proof - interpret ideal "Idl {𝟭}" "R" by (rule genideal_ideal) fast show "Idl {𝟭} = carrier R" using genideal_self' one_imp_carrier by blast 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}" lemma cginideal_def': "cgenideal R a = (λx. x ⊗⇘_{R⇙}a) ` carrier R" by (auto simp add: cgenideal_def) text ‹genhideal (?) really generates an ideal› lemma (in cring) cgenideal_ideal: assumes acarr: "a ∈ carrier R" shows "ideal (PIdl a) R" unfolding cgenideal_def proof (intro subgroup.intro idealI[OF is_ring], simp_all) show "{x ⊗ a |x. x ∈ carrier R} ⊆ carrier R" by (blast intro: acarr) show "⋀x y. ⟦∃u. x = u ⊗ a ∧ u ∈ carrier R; ∃x. y = x ⊗ a ∧ x ∈ carrier R⟧ ⟹ ∃v. x ⊕ y = v ⊗ a ∧ v ∈ carrier R" by (metis assms cring.cring_simprules(1) is_cring l_distr) show "∃x. 𝟬 = x ⊗ a ∧ x ∈ carrier R" by (metis assms l_null zero_closed) show "⋀x. ∃u. x = u ⊗ a ∧ u ∈ carrier R ⟹ ∃v. inv⇘_{add_monoid R⇙}x = v ⊗ a ∧ v ∈ carrier R" by (metis a_inv_def add.inv_closed assms l_minus) show "⋀b x. ⟦∃x. b = x ⊗ a ∧ x ∈ carrier R; x ∈ carrier R⟧ ⟹ ∃z. x ⊗ b = z ⊗ a ∧ z ∈ carrier R" by (metis assms m_assoc m_closed) show "⋀b x. ⟦∃x. b = x ⊗ a ∧ x ∈ carrier R; x ∈ carrier R⟧ ⟹ ∃z. b ⊗ x = z ⊗ a ∧ z ∈ carrier R" by (metis assms m_assoc m_comm m_closed) 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 using I_l_closed aJ by blast qed lemma (in cring) cgenideal_eq_genideal: assumes icarr: "i ∈ carrier R" shows "PIdl i = Idl {i}" proof show "PIdl i ⊆ Idl {i}" by (simp add: cgenideal_minimal genideal_ideal genideal_self' icarr) show "Idl {i} ⊆ PIdl i" by (simp add: cgenideal_ideal cgenideal_self genideal_minimal icarr) qed 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 "i ∈ carrier R" shows "principalideal (PIdl i) R" proof - have "∃i'∈carrier R. PIdl i = Idl {i'}" using cgenideal_eq_genideal assms by auto then show ?thesis by (simp add: cgenideal_ideal assms principalidealI) 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" proof show "Idl (I ∪ J) ⊆ I <+> J" proof (rule ring.genideal_minimal [OF is_ring]) show "ideal (I <+> J) R" by (rule add_ideals[OF idealI idealJ]) have "⋀x. x ∈ I ⟹ ∃xa∈I. ∃xb∈J. x = xa ⊕ xb" by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def local.idealI r_zero) moreover have "⋀x. x ∈ J ⟹ ∃xa∈I. ∃xb∈J. x = xa ⊕ xb" by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def l_zero local.idealI) ultimately show "I ∪ J ⊆ I <+> J" by (auto simp: set_add_defs) qed next show "I <+> J ⊆ Idl (I ∪ J)" by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def set_mp) qed subsection ‹Properties of Principal Ideals› text ‹The zero ideal is a principal ideal› corollary (in ring) zeropideal: "principalideal {𝟬} R" using genideal_zero principalidealI zeroideal by blast text ‹The unit ideal is a principal ideal› corollary (in ring) onepideal: "principalideal (carrier R) R" using genideal_one oneideal principalidealI by blast 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+ then have "I = PIdl i" by (simp add: cgenideal_eq_genideal) moreover have "i ∈ I" by (simp add: I1 genideal_self' icarr) moreover have "PIdl i = carrier R #> i" unfolding cgenideal_def r_coset_def by fast ultimately show "∃x∈I. I = carrier R #> x" by fast qed (* Next lemma contributed by Paulo EmÃlio de Vilhena. *) text ‹This next lemma would be trivial if placed in a theory that imports QuotRing, but it makes more sense to have it here (easier to find and coherent with the previous developments).› lemma (in cring) cgenideal_prod: assumes "a ∈ carrier R" "b ∈ carrier R" shows "(PIdl a) <#> (PIdl b) = PIdl (a ⊗ b)" proof - have "(carrier R #> a) <#> (carrier R #> b) = carrier R #> (a ⊗ b)" proof show "(carrier R #> a) <#> (carrier R #> b) ⊆ carrier R #> a ⊗ b" proof fix x assume "x ∈ (carrier R #> a) <#> (carrier R #> b)" then obtain r1 r2 where r1: "r1 ∈ carrier R" and r2: "r2 ∈ carrier R" and "x = (r1 ⊗ a) ⊗ (r2 ⊗ b)" unfolding set_mult_def r_coset_def by blast hence "x = (r1 ⊗ r2) ⊗ (a ⊗ b)" by (simp add: assms local.ring_axioms m_lcomm ring.ring_simprules(11)) thus "x ∈ carrier R #> a ⊗ b" unfolding r_coset_def using r1 r2 assms by blast qed next show "carrier R #> a ⊗ b ⊆ (carrier R #> a) <#> (carrier R #> b)" proof fix x assume "x ∈ carrier R #> a ⊗ b" then obtain r where r: "r ∈ carrier R" "x = r ⊗ (a ⊗ b)" unfolding r_coset_def by blast hence "x = (r ⊗ a) ⊗ (𝟭 ⊗ b)" using assms by (simp add: m_assoc) thus "x ∈ (carrier R #> a) <#> (carrier R #> b)" unfolding set_mult_def r_coset_def using assms r by blast qed qed thus ?thesis using cgenideal_eq_rcos[of a] cgenideal_eq_rcos[of b] cgenideal_eq_rcos[of "a ⊗ b"] by simp 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" by (simp add: I_prime InR is_cring is_ideal primeidealI) 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" proof (intro domain.intro is_cring domain_axioms.intro) show "𝟭 ≠ 𝟬" using genideal_one genideal_zero pi primeideal.I_notcarr by force show "a = 𝟬 ∨ b = 𝟬" if ab: "a ⊗ b = 𝟬" and carr: "a ∈ carrier R" "b ∈ carrier R" for a b proof - interpret primeideal "{𝟬}" "R" by (rule pi) show "a = 𝟬 ∨ b = 𝟬" using I_prime ab carr by blast qed qed corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {𝟬} R" using domain.zeroprimeideal zeroprimeideal_domainI by blast 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 proof (rule idealI, simp_all) show "ring R" by (simp add: local.ring_axioms) show "subgroup {x ∈ carrier R. a ⊗ x ∈ I} (add_monoid R)" by (rule subgroup.intro) (auto simp: r_distr acarr r_minus simp flip: a_inv_def) show "⋀b x. ⟦b ∈ carrier R ∧ a ⊗ b ∈ I; x ∈ carrier R⟧ ⟹ a ⊗ (x ⊗ b) ∈ I" using acarr helper_I_closed m_comm by auto show "⋀b x. ⟦b ∈ carrier R ∧ a ⊗ b ∈ I; x ∈ carrier R⟧ ⟹ a ⊗ (b ⊗ x) ∈ I" by (simp add: acarr helper_I_closed) 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 proof (rule ccontr) assume neg: "¬ primeideal I R" 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" using primeidealCE [OF is_cring] by (metis I_notcarr) 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" using I_l_closed J_def a_Hcarr acarr by blast from abI and acarr bcarr have "b ∈ J" unfolding J_def by fast with bnI have JnI: "J ≠ I" by fast have "𝟭 ∉ J" unfolding J_def by (simp add: acarr anI) then have Jncarr: "J ≠ carrier R" by fast interpret ideal J R by (rule idealJ) have "J = I ∨ J = carrier R" by (simp add: I_maximal IsubJ a_subset is_ideal) with JnI and Jncarr show False by simp qed qed subsection ‹Derived Theorems› text ‹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" proof (intro cring_fieldI equalityI) show "Units R ⊆ carrier R - {𝟬}" by (metis Diff_empty Units_closed Units_r_inv_ex carrnzero l_null one_zeroD subsetI subset_Diff_insert) show "carrier R - {𝟬} ⊆ Units R" proof fix x assume xcarr': "x ∈ carrier R - {𝟬}" then have xcarr: "x ∈ carrier R" and xnZ: "x ≠ 𝟬" by auto from xcarr have xIdl: "ideal (PIdl x) R" by (intro cgenideal_ideal) fast have "PIdl x ≠ {𝟬}" using xcarr xnZ cgenideal_self by blast 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 have "∃y ∈ carrier R. y ⊗ x = 𝟭 ∧ x ⊗ y = 𝟭" using m_comm xcarr ycarr ylinv by auto with xcarr show "x ∈ Units R" unfolding Units_def by fast qed qed lemma (in field) all_ideals: "{I. ideal I R} = {{𝟬}, carrier R}" proof (intro equalityI subsetI) 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+ have aUnit: "a ∈ Units R" by (simp add: aI anZ 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" using oneI one_imp_carrier by auto 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 ⊆ {𝟬}" using False by auto have "𝟬 ∈ I" by simp with a have "I = {𝟬}" by fast then show "I ∈ {{𝟬}, carrier R}" by fast qed qed (auto simp: 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" proof (intro maximalidealI zeroideal) 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" proof (intro trivialideals_fieldI maximalideal.I_notcarr[OF zeromax]) have "J = carrier R" if Jn0: "J ≠ {𝟬}" and idealJ: "ideal J R" for J proof - interpret ideal J R by (rule idealJ) have "{𝟬} ⊆ J" by force from zeromax idealJ this a_subset have "J = {𝟬} ∨ J = carrier R" by (rule maximalideal.I_maximal) with Jn0 show "J = carrier R" by simp qed then show "{I. ideal I R} = {{𝟬}, carrier R}" by (auto simp: zeroideal oneideal) qed lemma (in cring) zeromaximalideal_eq_field: "maximalideal {𝟬} R = field R" using field.zeromaximalideal zeromaximalideal_fieldI by blast end