src/HOL/Algebra/Ideal.thy

 imports Ring AbelCoset
 begin
 
 section {* Ideals *}
 
-subsection {* General definition *}
+subsection {* Definitions *}
+
+subsubsection {* General definition *}
 
 locale ideal = additive_subgroup I R + ring R +
   assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
       and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
 

    apply (erule (1) I_l_closed)
   apply (erule (1) I_r_closed)
   done
 qed
 
-subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
+subsubsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
 
 constdefs (structure R)
   genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
   "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
 
 
-subsection {* Principal Ideals *}
+subsubsection {* Principal Ideals *}
 
 locale principalideal = ideal +
   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
 
 lemma (in principalideal) is_principalideal:

 proof -
   interpret ideal [I R] by fact
   show ?thesis  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
 qed
 
-subsection {* Maximal Ideals *}
+subsubsection {* Maximal Ideals *}
 
 locale maximalideal = ideal +
   assumes I_notcarr: "carrier R \<noteq> I"
       and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
 

   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
 
-subsection {* Prime Ideals *}
+subsubsection {* Prime Ideals *}
 
 locale primeideal = ideal + cring +
   assumes I_notcarr: "carrier R \<noteq> I"
       and I_prime: "\<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
 

     apply (intro primeideal_axioms.intro)
     apply (rule I_notcarr)
     apply (erule (2) I_prime)
     done
 qed
-
-section {* Properties of Ideals *}
 
 subsection {* Special Ideals *}
 
 lemma (in ring) zeroideal:
   shows "ideal {\<zero>} R"

   apply (fast intro: ideal.I_l_closed ideal.intro assms)+
 apply (clarsimp, rule)
  apply (fast intro: ideal.I_r_closed ideal.intro assms)+
 done
 qed
-
-subsubsection {* Intersection of a Set of Ideals *}
 
 text {* The intersection of any Number of Ideals is again
         an Ideal in @{term R} *}
 lemma (in ring) i_Intersect:
   assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"

 
 
 subsection {* Ideals generated by a subset of @{term [locale=ring]
   "carrier R"} *}
 
-subsubsection {* Generation of Ideals in General Rings *}
-
 text {* @{term genideal} generates an ideal *}
 lemma (in ring) genideal_ideal:
   assumes Scarr: "S \<subseteq> carrier R"
   shows "ideal (Idl S) R"
 unfolding genideal_def

   apply (simp add: one_imp_carrier genideal_self')
   done
 qed
 
 
-subsubsection {* Generation of Principal Ideals in Commutative Rings *}
+text {* Generation of Principal Ideals in Commutative Rings *}
 
 constdefs (structure R)
   cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
   "cgenideal R a \<equiv> { x \<otimes> a | x. x \<in> carrier R }"
 

     from this and JnI and Jncarr
     show "False" by simp
   qed
 qed
 
-subsection {* Derived Theorems Involving Ideals *}
+subsection {* Derived Theorems *}
 
 --"A non-zero cring that has only the two trivial ideals is a field"
 lemma (in cring) trivialideals_fieldI:
   assumes carrnzero: "carrier R \<noteq> {\<zero>}"
       and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}"