# Theory Ideal

```(*  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 "abelian_monoid R"
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 ring_axioms 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

(* NEW ====== *)
lemma (in ideal) rcos_const_imp_mem:
assumes "i ∈ carrier R" and "I +> i = I" shows "i ∈ I"
(* ========== *)

(* NEW ====== *)
lemma (in ring) a_rcos_zero:
assumes "ideal I R" "i ∈ I" shows "I +> i = I"
using abelian_subgroupI3[OF ideal.axioms(1) is_abelian_group]
(* ========== *)

(* NEW ====== *)
lemma (in ring) ideal_is_normal:
assumes "ideal I R" shows "I ⊲ (add_monoid R)"
using abelian_subgroup.a_normal[OF abelian_subgroupI3[OF ideal.axioms(1)]]
abelian_group_axioms assms
by auto
(* ========== *)

(* NEW ====== *)
lemma (in ideal) a_rcos_sum:
assumes "a ∈ carrier R" and "b ∈ carrier R" shows "(I +> a) <+> (I +> b) = I +> (a ⊕ b)"
using normal.rcos_sum[OF ideal_is_normal[OF ideal_axioms]] assms
(* ========== *)

(* NEW ====== *)
assumes "I ⊆ carrier R" "J ⊆ carrier R" shows "I <+> J = J <+> I"
proof -
{ fix I J assume "I ⊆ carrier R" "J ⊆ carrier R" hence "I <+> J ⊆ J <+> I"
using a_comm unfolding set_add_def' by (auto, blast) }
thus ?thesis
using assms by auto
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)
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: ring_axioms)

lemma (in ring) oneideal: "ideal (carrier R) R"
by (rule idealI) (auto intro: ring_axioms add.subgroupI)

lemma (in "domain") zeroprimeideal: "primeideal {𝟬} R"
proof -
have "carrier R ≠ {𝟬}"
then show ?thesis
by (metis (no_types, lifting) domain_axioms domain_def integral primeidealI singleton_iff zeroideal)
qed

subsection ‹General Ideal Properties›

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)

lemma (in ring) quotient_eq_iff_same_a_r_cos:
assumes "ideal I R" and "a ∈ carrier R" and "b ∈ carrier R"
shows "a ⊖ b ∈ I ⟷ I +> a = I +> b"
proof
assume "I +> a = I +> b"
then obtain i where "i ∈ I" and "𝟬 ⊕ a = i ⊕ b"
unfolding a_r_coset_def' by blast
hence "a ⊖ b = i"
using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero)
with ‹i ∈ I› show "a ⊖ b ∈ I"
by simp
next
assume "a ⊖ b ∈ I"
then obtain i where "i ∈ I" and "a = i ⊕ b"
using ideal.Icarr[OF assms(1)] assms(2-3)
hence "I +> a = (I +> i) +> b"
using ideal.Icarr[OF assms(1)] assms(3)
with ‹i ∈ I› show "I +> a = I +> b"
using a_rcos_zero[OF assms(1)] by simp
qed

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 ring_axioms 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
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

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"
show "ring R"
by (rule ring_axioms)
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}"

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 {𝟬} ⊆ {𝟬}"
show "{𝟬} ⊆ Idl {𝟬}"
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}"

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 ring_axioms], 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 ring_axioms])
show "ideal (I <+> J) R"
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"
qed
next
show "I <+> J ⊆ Idl (I ∪ J)"
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"
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

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: ✐‹contributor ‹Paulo Emílio de Vilhena››
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"
also from carr have "(a ⊗ x) ⊗ y = a ⊗ (x ⊗ y)"
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"
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"
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
```