Quelle Ideal.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/Ideal.thy
    Author:     Stephan Hohe, TU Muenchen
*)

theory Ideal
imports Ring AbelCoset
begin

section \<open>Ideals\<close>

subsection \<open>Definitions\<close>

subsubsection \<open>General definition\<close>

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 \<subseteq> 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 ring_axioms I_l_closed I_r_closed)
qed

subsubsection (in ring) \<open>Ideals Generated by a Subset of \<^term>\<open>carrier R\<close>\<close>

definition genideal :: "_ \ 'a set \ 'a set"
    (\<open>(\<open>open_block notation=\<open>prefix Idl\<close>\<close>Idl\<index> _)\<close> [80] 79)
  where "Idl\<^bsub>R\<^esub> S = \{I. ideal I R \ S \ I}"

subsubsection \<open>Principal Ideals\<close>

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"
  using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF ideal_axioms]] assms
  by (force simp add: a_r_coset_def')
(* ========== *)

(* 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]
  by (simp add: abelian_subgroup.a_rcos_const assms)
(* ========== *)

(* 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
  unfolding set_add_def a_r_coset_def by simp
(* ========== *)

(* NEW ====== *)
lemma (in ring) set_add_comm:
  assumes "I \ carrier R" "J \ carrier R" shows "I <+> J = J <+> I"
proof -
  have "I <+> J \ J <+> I" if "I \ carrier R" "J \ carrier R" for I J
    using that a_comm unfolding set_add_def' by (auto, blast)
  thus ?thesis
    using assms by auto
qed
(* ========== *)

subsubsection \<open>Maximal Ideals\<close>

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 \<open>Prime Ideals\<close>

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 \<open>Special Ideals\<close>

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 \ {\}"
    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 \<open>General Ideal Properties\<close>

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"
    using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2)
    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 \<open>i \<in> I\<close> show "a \<ominus> b \<in> 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)
    by (metis a_minus_def add.inv_solve_right)
  hence "I +> a = (I +> i) +> b"
    using ideal.Icarr[OF assms(1)] assms(3)
    by (simp add: a_coset_add_assoc subsetI)
  with \<open>i \<in> I\<close> show "I +> a = I +> b"
    using a_rcos_zero[OF assms(1)] by simp
qed

subsection \<open>Intersection of Ideals\<close>

paragraph \<open>Intersection of two ideals\<close>
text \<open>The intersection of any two ideals is again an ideal in \<^term>\<open>R\<close>\<close>

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 \<open>The intersection of any Number of Ideals is again an Ideal in \<^term>\<open>R\<close>\<close>

lemma (in ring) i_Intersect:
  assumes Sideals: "\I. I \ S \ ideal I R" and notempty: "S \ {}"
  shows "ideal (\S) R"
proof -
  have "x \ y \ J" if "\I\S. x \ I" "\I\S. y \ I" and JS: "J \ S" for x y J
  proof -
    interpret ideal J R by (rule Sideals[OF JS])
    show ?thesis by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close> \<open>\<forall>I\<in>S. y \<in> I\<close>)
  qed
  moreover have "\ \ J" if "J \ S" for J
    by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1))
  moreover have "\ x \ J" if "\I\S. x \ I" and JS: "J \ S" for x J
  proof -
    interpret ideal J R by (rule Sideals[OF JS])
    show ?thesis by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close>)
  qed
  moreover have "y \ x \ J" "x \ y \ J"
    if "\I\S. x \ I" and ycarr: "y \ carrier R" and JS: "J \ S" for x y J
  proof -
    interpret ideal J R by (rule Sideals[OF JS])
    show "y \ x \ J" "x \ y \ J" using I_l_closed I_r_closed JS \\I\S. x \ I\ ycarr by blast+
  qed
  moreover have "x \ carrier R" if "\I\S. x \ I" for x
    proof -
    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 \<open>\<forall>I\<in>S. x \<in> I\<close>)
    with a_subset show ?thesis by fast
  qed
  ultimately show ?thesis
    by unfold_locales (auto simp: Inter_eq simp flip: a_inv_def)
qed

subsection \<open>Addition of Ideals\<close>

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 ring_axioms)
  show "ideal_axioms (I <+> J) R"
  proof -
    have "\h\I. \k\J. (i \ j) \ x = h \ k"
      if xcarr: "x \ carrier R" and iI: "i \ I" and jJ: "j \ J" for x i j
      using xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
      by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI)
    moreover have "\h\I. \k\J. x \ (i \ j) = h \ k"
      if xcarr: "x \ carrier R" and iI: "i \ I" and jJ: "j \ J" for x i j
      using xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
        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) \<open>Ideals generated by a subset of \<^term>\<open>carrier R\<close>\<close>

text \<open>\<^term>\<open>genideal\<close> generates an ideal\<close>
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 \<open>\<^term>\<open>genideal\<close> generates the minimal ideal\<close>
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 \<open>Generated ideals and subsets\<close>
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 \<open>Generation of Principal Ideals in Commutative Rings\<close>

definition cgenideal :: "_ \ 'a \ 'a set"
    (\<open>(\<open>open_block notation=\<open>prefix PIdl\<close>\<close>PIdl\<index> _)\<close> [80] 79)
  where "PIdl\<^bsub>R\<^esub> a = {x \\<^bsub>R\<^esub> a | x. x \ carrier R}"

text \<open>genhideal (?) really generates an ideal\<close>
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\
              \<Longrightarrow> \<exists>v. x \<oplus> y = v \<otimes> a \<and> v \<in> 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
            \<Longrightarrow> \<exists>v. inv\<^bsub>add_monoid R\<^esub> x = v \<otimes> a \<and> v \<in> 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\
       \<Longrightarrow> \<exists>z. x \<otimes> b = z \<otimes> a \<and> z \<in> carrier R"
    by (metis assms m_assoc m_closed)
  show "\b x. \\x. b = x \ a \ x \ carrier R; x \ carrier R\
       \<Longrightarrow> \<exists>z. b \<otimes> x = z \<otimes> a \<and> z \<in> 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 \<open>\<^const>\<open>cgenideal\<close> is minimal\<close>

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 \<open>Union of Ideals\<close>

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"
      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 subsetD)
qed

subsection \<open>Properties of Principal Ideals\<close>

text \<open>The zero ideal is a principal ideal\<close>
corollary (in ring) zeropideal: "principalideal {\} R"
  using genideal_zero principalidealI zeroideal by blast

text \<open>The unit ideal is a principal ideal\<close>
corollary (in ring) onepideal: "principalideal (carrier R) R"
  using genideal_one oneideal principalidealI by blast

text \<open>Every principal ideal is a right coset of the carrier\<close>
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

text \<open>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).\<close>

lemma (in cring) cgenideal_prod: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  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 \<open>Prime Ideals\<close>

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 \<open>If \<open>{\<zero>}\<close> is a prime ideal of a commutative ring, the ring is a domain\<close>
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 \<open>Maximal Ideals\<close>

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\
                 \<Longrightarrow> a \<otimes> (x \<otimes> b) \<in> I"
      using acarr helper_I_closed m_comm by auto
    show "\b x. \b \ carrier R \ a \ b \ I; x \ carrier R\
                \<Longrightarrow> a \<otimes> (b \<otimes> x) \<in> I"
      by (simp add: acarr helper_I_closed)
  qed
qed

text \<open>In a cring every maximal ideal is prime\<close>
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 \<open>Derived Theorems\<close>

text \<open>A non-zero cring that has only the two trivial ideals is a field\<close>
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)

\<comment>\<open>"Jacobson Theorem 2.2"\<close>
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 \<open>Like zeroprimeideal for domains\<close>
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

quality99%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.17Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.