src/HOL/Algebra/Ideal.thy
 changeset 68445 c183a6a69f2d parent 68443 43055b016688 child 68458 023b353911c5
```     1.1 --- a/src/HOL/Algebra/Ideal.thy	Tue Jun 12 16:09:12 2018 +0100
1.2 +++ b/src/HOL/Algebra/Ideal.thy	Thu Jun 14 14:23:38 2018 +0100
1.3 @@ -14,7 +14,7 @@
1.4
1.5  locale ideal = additive_subgroup I R + ring R for I and R (structure) +
1.6    assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
1.7 -    and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
1.8 +      and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
1.9
1.10  sublocale ideal \<subseteq> abelian_subgroup I R
1.11    apply (intro abelian_subgroupI3 abelian_group.intro)
1.12 @@ -74,7 +74,7 @@
1.13
1.14  locale maximalideal = ideal +
1.15    assumes I_notcarr: "carrier R \<noteq> I"
1.16 -    and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
1.17 +    and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)"
1.18
1.19  lemma (in maximalideal) is_maximalideal: "maximalideal I R"
1.20    by (rule maximalideal_axioms)
1.21 @@ -83,7 +83,7 @@
1.22    fixes R
1.23    assumes "ideal I R"
1.24      and I_notcarr: "carrier R \<noteq> I"
1.25 -    and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
1.26 +    and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)"
1.27    shows "maximalideal I R"
1.28  proof -
1.29    interpret ideal I R by fact
1.30 @@ -143,26 +143,17 @@
1.31  subsection \<open>Special Ideals\<close>
1.32
1.33  lemma (in ring) zeroideal: "ideal {\<zero>} R"
1.34 -  apply (intro idealI subgroup.intro)
1.35 -        apply (rule is_ring)
1.36 -       apply simp+
1.37 -    apply (fold a_inv_def, simp)
1.38 -   apply simp+
1.39 -  done
1.40 +  by (intro idealI subgroup.intro) (simp_all add: is_ring)
1.41
1.42  lemma (in ring) oneideal: "ideal (carrier R) R"
1.43    by (rule idealI) (auto intro: is_ring add.subgroupI)
1.44
1.45  lemma (in "domain") zeroprimeideal: "primeideal {\<zero>} R"
1.46 -  apply (intro primeidealI)
1.47 -     apply (rule zeroideal)
1.48 -    apply (rule domain.axioms, rule domain_axioms)
1.49 -   defer 1
1.50 -   apply (simp add: integral)
1.51 -proof (rule ccontr, simp)
1.52 -  assume "carrier R = {\<zero>}"
1.53 -  then have "\<one> = \<zero>" by (rule one_zeroI)
1.54 -  with one_not_zero show False by simp
1.55 +proof -
1.56 +  have "carrier R \<noteq> {\<zero>}"
1.57 +    by (simp add: carrier_one_not_zero)
1.58 +  then show ?thesis
1.59 +    by (metis (no_types, lifting) domain_axioms domain_def integral primeidealI singleton_iff zeroideal)
1.60  qed
1.61
1.62
1.63 @@ -651,6 +642,46 @@
1.64  qed
1.65
1.66
1.67 +(* Next lemma contributed by Paulo Emílio de Vilhena. *)
1.68 +
1.69 +text \<open>This next lemma would be trivial if placed in a theory that imports QuotRing,
1.70 +      but it makes more sense to have it here (easier to find and coherent with the
1.71 +      previous developments).\<close>
1.72 +
1.73 +lemma (in cring) cgenideal_prod:
1.74 +  assumes "a \<in> carrier R" "b \<in> carrier R"
1.75 +  shows "(PIdl a) <#> (PIdl b) = PIdl (a \<otimes> b)"
1.76 +proof -
1.77 +  have "(carrier R #> a) <#> (carrier R #> b) = carrier R #> (a \<otimes> b)"
1.78 +  proof
1.79 +    show "(carrier R #> a) <#> (carrier R #> b) \<subseteq> carrier R #> a \<otimes> b"
1.80 +    proof
1.81 +      fix x assume "x \<in> (carrier R #> a) <#> (carrier R #> b)"
1.82 +      then obtain r1 r2 where r1: "r1 \<in> carrier R" and r2: "r2 \<in> carrier R"
1.83 +                          and "x = (r1 \<otimes> a) \<otimes> (r2 \<otimes> b)"
1.84 +        unfolding set_mult_def r_coset_def by blast
1.85 +      hence "x = (r1 \<otimes> r2) \<otimes> (a \<otimes> b)"
1.86 +        by (simp add: assms local.ring_axioms m_lcomm ring.ring_simprules(11))
1.87 +      thus "x \<in> carrier R #> a \<otimes> b"
1.88 +        unfolding r_coset_def using r1 r2 assms by blast
1.89 +    qed
1.90 +  next
1.91 +    show "carrier R #> a \<otimes> b \<subseteq> (carrier R #> a) <#> (carrier R #> b)"
1.92 +    proof
1.93 +      fix x assume "x \<in> carrier R #> a \<otimes> b"
1.94 +      then obtain r where r: "r \<in> carrier R" "x = r \<otimes> (a \<otimes> b)"
1.95 +        unfolding r_coset_def by blast
1.96 +      hence "x = (r \<otimes> a) \<otimes> (\<one> \<otimes> b)"
1.97 +        using assms by (simp add: m_assoc)
1.98 +      thus "x \<in> (carrier R #> a) <#> (carrier R #> b)"
1.99 +        unfolding set_mult_def r_coset_def using assms r by blast
1.100 +    qed
1.101 +  qed
1.102 +  thus ?thesis
1.103 +    using cgenideal_eq_rcos[of a] cgenideal_eq_rcos[of b] cgenideal_eq_rcos[of "a \<otimes> b"] by simp
1.104 +qed
1.105 +
1.106 +
1.107  subsection \<open>Prime Ideals\<close>
1.108
1.109  lemma (in ideal) primeidealCD:
1.110 @@ -918,7 +949,7 @@
1.111    qed
1.112  qed (simp add: zeroideal oneideal)
1.113
1.114 -\<comment> \<open>Jacobson Theorem 2.2\<close>
1.115 +\<comment>\<open>"Jacobson Theorem 2.2"\<close>
1.116  lemma (in cring) trivialideals_eq_field:
1.117    assumes carrnzero: "carrier R \<noteq> {\<zero>}"
1.118    shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R"
```