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.100
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)
```