src/HOL/Algebra/Ideal.thy
changeset 61382 efac889fccbc
parent 47409 c5be1120980d
child 61506 436b7fe89cdc
     1.1 --- a/src/HOL/Algebra/Ideal.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Algebra/Ideal.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -6,11 +6,11 @@
     1.4  imports Ring AbelCoset
     1.5  begin
     1.6  
     1.7 -section {* Ideals *}
     1.8 +section \<open>Ideals\<close>
     1.9  
    1.10 -subsection {* Definitions *}
    1.11 +subsection \<open>Definitions\<close>
    1.12  
    1.13 -subsubsection {* General definition *}
    1.14 +subsubsection \<open>General definition\<close>
    1.15  
    1.16  locale ideal = additive_subgroup I R + ring R for I and R (structure) +
    1.17    assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    1.18 @@ -44,12 +44,12 @@
    1.19  qed
    1.20  
    1.21  
    1.22 -subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
    1.23 +subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
    1.24  
    1.25  definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
    1.26    where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
    1.27  
    1.28 -subsubsection {* Principal Ideals *}
    1.29 +subsubsection \<open>Principal Ideals\<close>
    1.30  
    1.31  locale principalideal = ideal +
    1.32    assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
    1.33 @@ -70,7 +70,7 @@
    1.34  qed
    1.35  
    1.36  
    1.37 -subsubsection {* Maximal Ideals *}
    1.38 +subsubsection \<open>Maximal Ideals\<close>
    1.39  
    1.40  locale maximalideal = ideal +
    1.41    assumes I_notcarr: "carrier R \<noteq> I"
    1.42 @@ -93,7 +93,7 @@
    1.43  qed
    1.44  
    1.45  
    1.46 -subsubsection {* Prime Ideals *}
    1.47 +subsubsection \<open>Prime Ideals\<close>
    1.48  
    1.49  locale primeideal = ideal + cring +
    1.50    assumes I_notcarr: "carrier R \<noteq> I"
    1.51 @@ -140,7 +140,7 @@
    1.52  qed
    1.53  
    1.54  
    1.55 -subsection {* Special Ideals *}
    1.56 +subsection \<open>Special Ideals\<close>
    1.57  
    1.58  lemma (in ring) zeroideal: "ideal {\<zero>} R"
    1.59    apply (intro idealI subgroup.intro)
    1.60 @@ -166,7 +166,7 @@
    1.61  qed
    1.62  
    1.63  
    1.64 -subsection {* General Ideal Properies *}
    1.65 +subsection \<open>General Ideal Properies\<close>
    1.66  
    1.67  lemma (in ideal) one_imp_carrier:
    1.68    assumes I_one_closed: "\<one> \<in> I"
    1.69 @@ -187,10 +187,10 @@
    1.70    using iI by (rule a_Hcarr)
    1.71  
    1.72  
    1.73 -subsection {* Intersection of Ideals *}
    1.74 +subsection \<open>Intersection of Ideals\<close>
    1.75  
    1.76 -text {* \paragraph{Intersection of two ideals} The intersection of any
    1.77 -  two ideals is again an ideal in @{term R} *}
    1.78 +text \<open>\paragraph{Intersection of two ideals} The intersection of any
    1.79 +  two ideals is again an ideal in @{term R}\<close>
    1.80  lemma (in ring) i_intersect:
    1.81    assumes "ideal I R"
    1.82    assumes "ideal J R"
    1.83 @@ -212,8 +212,8 @@
    1.84      done
    1.85  qed
    1.86  
    1.87 -text {* The intersection of any Number of Ideals is again
    1.88 -        an Ideal in @{term R} *}
    1.89 +text \<open>The intersection of any Number of Ideals is again
    1.90 +        an Ideal in @{term R}\<close>
    1.91  lemma (in ring) i_Intersect:
    1.92    assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"
    1.93      and notempty: "S \<noteq> {}"
    1.94 @@ -291,7 +291,7 @@
    1.95  qed
    1.96  
    1.97  
    1.98 -subsection {* Addition of Ideals *}
    1.99 +subsection \<open>Addition of Ideals\<close>
   1.100  
   1.101  lemma (in ring) add_ideals:
   1.102    assumes idealI: "ideal I R"
   1.103 @@ -335,9 +335,9 @@
   1.104  qed
   1.105  
   1.106  
   1.107 -subsection (in ring) {* Ideals generated by a subset of @{term "carrier R"} *}
   1.108 +subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close>
   1.109  
   1.110 -text {* @{term genideal} generates an ideal *}
   1.111 +text \<open>@{term genideal} generates an ideal\<close>
   1.112  lemma (in ring) genideal_ideal:
   1.113    assumes Scarr: "S \<subseteq> carrier R"
   1.114    shows "ideal (Idl S) R"
   1.115 @@ -360,14 +360,14 @@
   1.116    then show "i \<in> Idl {i}" by fast
   1.117  qed
   1.118  
   1.119 -text {* @{term genideal} generates the minimal ideal *}
   1.120 +text \<open>@{term genideal} generates the minimal ideal\<close>
   1.121  lemma (in ring) genideal_minimal:
   1.122    assumes a: "ideal I R"
   1.123      and b: "S \<subseteq> I"
   1.124    shows "Idl S \<subseteq> I"
   1.125    unfolding genideal_def by rule (elim InterD, simp add: a b)
   1.126  
   1.127 -text {* Generated ideals and subsets *}
   1.128 +text \<open>Generated ideals and subsets\<close>
   1.129  lemma (in ring) Idl_subset_ideal:
   1.130    assumes Iideal: "ideal I R"
   1.131      and Hcarr: "H \<subseteq> carrier R"
   1.132 @@ -425,12 +425,12 @@
   1.133  qed
   1.134  
   1.135  
   1.136 -text {* Generation of Principal Ideals in Commutative Rings *}
   1.137 +text \<open>Generation of Principal Ideals in Commutative Rings\<close>
   1.138  
   1.139  definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
   1.140    where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
   1.141  
   1.142 -text {* genhideal (?) really generates an ideal *}
   1.143 +text \<open>genhideal (?) really generates an ideal\<close>
   1.144  lemma (in cring) cgenideal_ideal:
   1.145    assumes acarr: "a \<in> carrier R"
   1.146    shows "ideal (PIdl a) R"
   1.147 @@ -499,7 +499,7 @@
   1.148      by fast
   1.149  qed
   1.150  
   1.151 -text {* @{const "cgenideal"} is minimal *}
   1.152 +text \<open>@{const "cgenideal"} is minimal\<close>
   1.153  
   1.154  lemma (in ring) cgenideal_minimal:
   1.155    assumes "ideal J R"
   1.156 @@ -544,7 +544,7 @@
   1.157  qed
   1.158  
   1.159  
   1.160 -subsection {* Union of Ideals *}
   1.161 +subsection \<open>Union of Ideals\<close>
   1.162  
   1.163  lemma (in ring) union_genideal:
   1.164    assumes idealI: "ideal I R"
   1.165 @@ -589,16 +589,16 @@
   1.166  qed
   1.167  
   1.168  
   1.169 -subsection {* Properties of Principal Ideals *}
   1.170 +subsection \<open>Properties of Principal Ideals\<close>
   1.171  
   1.172 -text {* @{text "\<zero>"} generates the zero ideal *}
   1.173 +text \<open>@{text "\<zero>"} generates the zero ideal\<close>
   1.174  lemma (in ring) zero_genideal: "Idl {\<zero>} = {\<zero>}"
   1.175    apply rule
   1.176    apply (simp add: genideal_minimal zeroideal)
   1.177    apply (fast intro!: genideal_self)
   1.178    done
   1.179  
   1.180 -text {* @{text "\<one>"} generates the unit ideal *}
   1.181 +text \<open>@{text "\<one>"} generates the unit ideal\<close>
   1.182  lemma (in ring) one_genideal: "Idl {\<one>} = carrier R"
   1.183  proof -
   1.184    have "\<one> \<in> Idl {\<one>}"
   1.185 @@ -608,14 +608,14 @@
   1.186  qed
   1.187  
   1.188  
   1.189 -text {* The zero ideal is a principal ideal *}
   1.190 +text \<open>The zero ideal is a principal ideal\<close>
   1.191  corollary (in ring) zeropideal: "principalideal {\<zero>} R"
   1.192    apply (rule principalidealI)
   1.193     apply (rule zeroideal)
   1.194    apply (blast intro!: zero_genideal[symmetric])
   1.195    done
   1.196  
   1.197 -text {* The unit ideal is a principal ideal *}
   1.198 +text \<open>The unit ideal is a principal ideal\<close>
   1.199  corollary (in ring) onepideal: "principalideal (carrier R) R"
   1.200    apply (rule principalidealI)
   1.201     apply (rule oneideal)
   1.202 @@ -623,7 +623,7 @@
   1.203    done
   1.204  
   1.205  
   1.206 -text {* Every principal ideal is a right coset of the carrier *}
   1.207 +text \<open>Every principal ideal is a right coset of the carrier\<close>
   1.208  lemma (in principalideal) rcos_generate:
   1.209    assumes "cring R"
   1.210    shows "\<exists>x\<in>I. I = carrier R #> x"
   1.211 @@ -650,7 +650,7 @@
   1.212  qed
   1.213  
   1.214  
   1.215 -subsection {* Prime Ideals *}
   1.216 +subsection \<open>Prime Ideals\<close>
   1.217  
   1.218  lemma (in ideal) primeidealCD:
   1.219    assumes "cring R"
   1.220 @@ -683,7 +683,7 @@
   1.221    then show thesis using primeidealCD [OF R.is_cring notprime] by blast
   1.222  qed
   1.223  
   1.224 -text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *}
   1.225 +text \<open>If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain\<close>
   1.226  lemma (in cring) zeroprimeideal_domainI:
   1.227    assumes pi: "primeideal {\<zero>} R"
   1.228    shows "domain R"
   1.229 @@ -713,7 +713,7 @@
   1.230    done
   1.231  
   1.232  
   1.233 -subsection {* Maximal Ideals *}
   1.234 +subsection \<open>Maximal Ideals\<close>
   1.235  
   1.236  lemma (in ideal) helper_I_closed:
   1.237    assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R"
   1.238 @@ -767,7 +767,7 @@
   1.239    qed
   1.240  qed
   1.241  
   1.242 -text {* In a cring every maximal ideal is prime *}
   1.243 +text \<open>In a cring every maximal ideal is prime\<close>
   1.244  lemma (in cring) maximalideal_is_prime:
   1.245    assumes "maximalideal I R"
   1.246    shows "primeideal I R"
   1.247 @@ -825,7 +825,7 @@
   1.248  qed
   1.249  
   1.250  
   1.251 -subsection {* Derived Theorems *}
   1.252 +subsection \<open>Derived Theorems\<close>
   1.253  
   1.254  --"A non-zero cring that has only the two trivial ideals is a field"
   1.255  lemma (in cring) trivialideals_fieldI:
   1.256 @@ -927,7 +927,7 @@
   1.257    by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals)
   1.258  
   1.259  
   1.260 -text {* Like zeroprimeideal for domains *}
   1.261 +text \<open>Like zeroprimeideal for domains\<close>
   1.262  lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R"
   1.263    apply (rule maximalidealI)
   1.264      apply (rule zeroideal)