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"