src/HOL/Algebra/QuotRing.thy
changeset 68551 b680e74eb6f2
parent 67443 3abf6a722518
child 68582 b9b9e2985878
child 68583 654e73d05495
     1.1 --- a/src/HOL/Algebra/QuotRing.thy	Fri Jun 29 23:04:36 2018 +0200
     1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Sat Jun 30 15:44:04 2018 +0100
     1.3 @@ -1,5 +1,7 @@
     1.4  (*  Title:      HOL/Algebra/QuotRing.thy
     1.5      Author:     Stephan Hohe
     1.6 +    Author:     Paulo Emílio de Vilhena
     1.7 +
     1.8  *)
     1.9  
    1.10  theory QuotRing
    1.11 @@ -306,4 +308,831 @@
    1.12    qed
    1.13  qed
    1.14  
    1.15 +
    1.16 +lemma (in ring_hom_ring) trivial_hom_iff:
    1.17 +  "(h ` (carrier R) = { \<zero>\<^bsub>S\<^esub> }) = (a_kernel R S h = carrier R)"
    1.18 +  using group_hom.trivial_hom_iff[OF a_group_hom] by (simp add: a_kernel_def)
    1.19 +
    1.20 +lemma (in ring_hom_ring) trivial_ker_imp_inj:
    1.21 +  assumes "a_kernel R S h = { \<zero> }"
    1.22 +  shows "inj_on h (carrier R)"
    1.23 +  using group_hom.trivial_ker_imp_inj[OF a_group_hom] assms a_kernel_def[of R S h] by simp 
    1.24 +
    1.25 +lemma (in ring_hom_ring) non_trivial_field_hom_imp_inj:
    1.26 +  assumes "field R"
    1.27 +  shows "h ` (carrier R) \<noteq> { \<zero>\<^bsub>S\<^esub> } \<Longrightarrow> inj_on h (carrier R)"
    1.28 +proof -
    1.29 +  assume "h ` (carrier R) \<noteq> { \<zero>\<^bsub>S\<^esub> }"
    1.30 +  hence "a_kernel R S h \<noteq> carrier R"
    1.31 +    using trivial_hom_iff by linarith
    1.32 +  hence "a_kernel R S h = { \<zero> }"
    1.33 +    using field.all_ideals[OF assms] kernel_is_ideal by blast
    1.34 +  thus "inj_on h (carrier R)"
    1.35 +    using trivial_ker_imp_inj by blast
    1.36 +qed
    1.37 +
    1.38 +lemma (in ring_hom_ring) img_is_add_subgroup:
    1.39 +  assumes "subgroup H (add_monoid R)"
    1.40 +  shows "subgroup (h ` H) (add_monoid S)"
    1.41 +proof -
    1.42 +  have "group ((add_monoid R) \<lparr> carrier := H \<rparr>)"
    1.43 +    using assms R.add.subgroup_imp_group by blast
    1.44 +  moreover have "H \<subseteq> carrier R" by (simp add: R.add.subgroupE(1) assms)
    1.45 +  hence "h \<in> hom ((add_monoid R) \<lparr> carrier := H \<rparr>) (add_monoid S)"
    1.46 +    unfolding hom_def by (auto simp add: subsetD)
    1.47 +  ultimately have "subgroup (h ` carrier ((add_monoid R) \<lparr> carrier := H \<rparr>)) (add_monoid S)"
    1.48 +    using group_hom.img_is_subgroup[of "(add_monoid R) \<lparr> carrier := H \<rparr>" "add_monoid S" h]
    1.49 +    using a_group_hom group_hom_axioms.intro group_hom_def by blast
    1.50 +  thus "subgroup (h ` H) (add_monoid S)" by simp
    1.51 +qed
    1.52 +
    1.53 +lemma (in ring) ring_ideal_imp_quot_ideal:
    1.54 +  assumes "ideal I R"
    1.55 +  shows "ideal J R \<Longrightarrow> ideal ((+>) I ` J) (R Quot I)"
    1.56 +proof -
    1.57 +  assume A: "ideal J R" show "ideal (((+>) I) ` J) (R Quot I)"
    1.58 +  proof (rule idealI)
    1.59 +    show "ring (R Quot I)"
    1.60 +      by (simp add: assms(1) ideal.quotient_is_ring) 
    1.61 +  next
    1.62 +    have "subgroup J (add_monoid R)"
    1.63 +      by (simp add: additive_subgroup.a_subgroup A ideal.axioms(1))
    1.64 +    moreover have "((+>) I) \<in> ring_hom R (R Quot I)"
    1.65 +      by (simp add: assms(1) ideal.rcos_ring_hom)
    1.66 +    ultimately show "subgroup ((+>) I ` J) (add_monoid (R Quot I))"
    1.67 +      using assms(1) ideal.rcos_ring_hom_ring ring_hom_ring.img_is_add_subgroup by blast
    1.68 +  next
    1.69 +    fix a x assume "a \<in> (+>) I ` J" "x \<in> carrier (R Quot I)"
    1.70 +    then obtain i j where i: "i \<in> carrier R" "x = I +> i"
    1.71 +                      and j: "j \<in> J" "a = I +> j"
    1.72 +      unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto
    1.73 +    hence "a \<otimes>\<^bsub>R Quot I\<^esub> x = [mod I:] (I +> j) \<Otimes> (I +> i)"
    1.74 +      unfolding FactRing_def by simp
    1.75 +    hence "a \<otimes>\<^bsub>R Quot I\<^esub> x = I +> (j \<otimes> i)"
    1.76 +      using ideal.rcoset_mult_add[OF assms(1), of j i] i(1) j(1) A ideal.Icarr by force
    1.77 +    thus "a \<otimes>\<^bsub>R Quot I\<^esub> x \<in> (+>) I ` J"
    1.78 +      using A i(1) j(1) by (simp add: ideal.I_r_closed)
    1.79 +  
    1.80 +    have "x \<otimes>\<^bsub>R Quot I\<^esub> a = [mod I:] (I +> i) \<Otimes> (I +> j)"
    1.81 +      unfolding FactRing_def i j by simp
    1.82 +    hence "x \<otimes>\<^bsub>R Quot I\<^esub> a = I +> (i \<otimes> j)"
    1.83 +      using ideal.rcoset_mult_add[OF assms(1), of i j] i(1) j(1) A ideal.Icarr by force
    1.84 +    thus "x \<otimes>\<^bsub>R Quot I\<^esub> a \<in> (+>) I ` J"
    1.85 +      using A i(1) j(1) by (simp add: ideal.I_l_closed)
    1.86 +  qed
    1.87 +qed
    1.88 +
    1.89 +lemma (in ring_hom_ring) ideal_vimage:
    1.90 +  assumes "ideal I S"
    1.91 +  shows "ideal { r \<in> carrier R. h r \<in> I } R" (* or (carrier R) \<inter> (h -` I) *)
    1.92 +proof
    1.93 +  show "{ r \<in> carrier R. h r \<in> I } \<subseteq> carrier (add_monoid R)" by auto
    1.94 +next
    1.95 +  show "\<one>\<^bsub>add_monoid R\<^esub> \<in> { r \<in> carrier R. h r \<in> I }"
    1.96 +    by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1))
    1.97 +next
    1.98 +  fix a b
    1.99 +  assume "a \<in> { r \<in> carrier R. h r \<in> I }"
   1.100 +     and "b \<in> { r \<in> carrier R. h r \<in> I }"
   1.101 +  hence a: "a \<in> carrier R" "h a \<in> I"
   1.102 +    and b: "b \<in> carrier R" "h b \<in> I" by auto
   1.103 +  hence "h (a \<oplus> b) = (h a) \<oplus>\<^bsub>S\<^esub> (h b)" using hom_add by blast
   1.104 +  moreover have "(h a) \<oplus>\<^bsub>S\<^esub> (h b) \<in> I" using a b assms
   1.105 +    by (simp add: additive_subgroup.a_closed ideal.axioms(1))
   1.106 +  ultimately show "a \<otimes>\<^bsub>add_monoid R\<^esub> b \<in> { r \<in> carrier R. h r \<in> I }"
   1.107 +    using a(1) b (1) by auto
   1.108 +
   1.109 +  have "h (\<ominus> a) = \<ominus>\<^bsub>S\<^esub> (h a)" by (simp add: a)
   1.110 +  moreover have "\<ominus>\<^bsub>S\<^esub> (h a) \<in> I"
   1.111 +    by (simp add: a(2) additive_subgroup.a_inv_closed assms ideal.axioms(1))
   1.112 +  ultimately show "inv\<^bsub>add_monoid R\<^esub> a \<in> { r \<in> carrier R. h r \<in> I }"
   1.113 +    using a by (simp add: a_inv_def)
   1.114 +next
   1.115 +  fix a r
   1.116 +  assume "a \<in> { r \<in> carrier R. h r \<in> I }" and r: "r \<in> carrier R"
   1.117 +  hence a: "a \<in> carrier R" "h a \<in> I" by auto
   1.118 +
   1.119 +  have "h a \<otimes>\<^bsub>S\<^esub> h r \<in> I"
   1.120 +    using assms a r by (simp add: ideal.I_r_closed)
   1.121 +  thus "a \<otimes> r \<in> { r \<in> carrier R. h r \<in> I }" by (simp add: a(1) r)
   1.122 +
   1.123 +  have "h r \<otimes>\<^bsub>S\<^esub> h a \<in> I"
   1.124 +    using assms a r by (simp add: ideal.I_l_closed)
   1.125 +  thus "r \<otimes> a \<in> { r \<in> carrier R. h r \<in> I }" by (simp add: a(1) r)
   1.126 +qed
   1.127 +
   1.128 +lemma (in ring) canonical_proj_vimage_in_carrier:
   1.129 +  assumes "ideal I R"
   1.130 +  shows "J \<subseteq> carrier (R Quot I) \<Longrightarrow> \<Union> J \<subseteq> carrier R"
   1.131 +proof -
   1.132 +  assume A: "J \<subseteq> carrier (R Quot I)" show "\<Union> J \<subseteq> carrier R"
   1.133 +  proof
   1.134 +    fix j assume j: "j \<in> \<Union> J"
   1.135 +    then obtain j' where j': "j' \<in> J" "j \<in> j'" by blast
   1.136 +    then obtain r where r: "r \<in> carrier R" "j' = I +> r"
   1.137 +      using A j' unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto
   1.138 +    thus "j \<in> carrier R" using j' assms
   1.139 +      by (meson a_r_coset_subset_G additive_subgroup.a_subset contra_subsetD ideal.axioms(1)) 
   1.140 +  qed
   1.141 +qed
   1.142 +
   1.143 +lemma (in ring) canonical_proj_vimage_mem_iff:
   1.144 +  assumes "ideal I R" "J \<subseteq> carrier (R Quot I)"
   1.145 +  shows "\<And>a. a \<in> carrier R \<Longrightarrow> (a \<in> (\<Union> J)) = (I +> a \<in> J)"
   1.146 +proof -
   1.147 +  fix a assume a: "a \<in> carrier R" show "(a \<in> (\<Union> J)) = (I +> a \<in> J)"
   1.148 +  proof
   1.149 +    assume "a \<in> \<Union> J"
   1.150 +    then obtain j where j: "j \<in> J" "a \<in> j" by blast
   1.151 +    then obtain r where r: "r \<in> carrier R" "j = I +> r"
   1.152 +      using assms j unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto
   1.153 +    hence "I +> r = I +> a"
   1.154 +      using add.repr_independence[of a I r] j r
   1.155 +      by (metis a_r_coset_def additive_subgroup.a_subgroup assms(1) ideal.axioms(1))
   1.156 +    thus "I +> a \<in> J" using r j by simp
   1.157 +  next
   1.158 +    assume "I +> a \<in> J"
   1.159 +    hence "\<zero> \<oplus> a \<in> I +> a"
   1.160 +      using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]]
   1.161 +            a_r_coset_def'[of R I a] by blast
   1.162 +    thus "a \<in> \<Union> J" using a \<open>I +> a \<in> J\<close> by auto 
   1.163 +  qed
   1.164 +qed
   1.165 +
   1.166 +corollary (in ring) quot_ideal_imp_ring_ideal:
   1.167 +  assumes "ideal I R"
   1.168 +  shows "ideal J (R Quot I) \<Longrightarrow> ideal (\<Union> J) R"
   1.169 +proof -
   1.170 +  assume A: "ideal J (R Quot I)"
   1.171 +  have "\<Union> J = { r \<in> carrier R. I +> r \<in> J }"
   1.172 +    using canonical_proj_vimage_in_carrier[OF assms, of J]
   1.173 +          canonical_proj_vimage_mem_iff[OF assms, of J]
   1.174 +          additive_subgroup.a_subset[OF ideal.axioms(1)[OF A]] by blast
   1.175 +  thus "ideal (\<Union> J) R"
   1.176 +    using ring_hom_ring.ideal_vimage[OF ideal.rcos_ring_hom_ring[OF assms] A] by simp
   1.177 +qed
   1.178 +
   1.179 +lemma (in ring) ideal_incl_iff:
   1.180 +  assumes "ideal I R" "ideal J R"
   1.181 +  shows "(I \<subseteq> J) = (J = (\<Union> j \<in> J. I +> j))"
   1.182 +proof
   1.183 +  assume A: "J = (\<Union> j \<in> J. I +> j)" hence "I +> \<zero> \<subseteq> J"
   1.184 +    using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(2)]] by blast
   1.185 +  thus "I \<subseteq> J" using additive_subgroup.a_subset[OF ideal.axioms(1)[OF assms(1)]] by simp 
   1.186 +next
   1.187 +  assume A: "I \<subseteq> J" show "J = (\<Union>j\<in>J. I +> j)"
   1.188 +  proof
   1.189 +    show "J \<subseteq> (\<Union> j \<in> J. I +> j)"
   1.190 +    proof
   1.191 +      fix j assume j: "j \<in> J"
   1.192 +      have "\<zero> \<in> I" by (simp add: additive_subgroup.zero_closed assms(1) ideal.axioms(1))
   1.193 +      hence "\<zero> \<oplus> j \<in> I +> j"
   1.194 +        using a_r_coset_def'[of R I j] by blast
   1.195 +      thus "j \<in> (\<Union>j\<in>J. I +> j)"
   1.196 +        using assms(2) j additive_subgroup.a_Hcarr ideal.axioms(1) by fastforce 
   1.197 +    qed
   1.198 +  next
   1.199 +    show "(\<Union> j \<in> J. I +> j) \<subseteq> J"
   1.200 +    proof
   1.201 +      fix x assume "x \<in> (\<Union> j \<in> J. I +> j)"
   1.202 +      then obtain j where j: "j \<in> J" "x \<in> I +> j" by blast
   1.203 +      then obtain i where i: "i \<in> I" "x = i \<oplus> j"
   1.204 +        using a_r_coset_def'[of R I j] by blast
   1.205 +      thus "x \<in> J"
   1.206 +        using assms(2) j A additive_subgroup.a_closed[OF ideal.axioms(1)[OF assms(2)]] by blast
   1.207 +    qed
   1.208 +  qed
   1.209 +qed
   1.210 +
   1.211 +theorem (in ring) quot_ideal_correspondence:
   1.212 +  assumes "ideal I R"
   1.213 +  shows "bij_betw (\<lambda>J. (+>) I ` J) { J. ideal J R \<and> I \<subseteq> J } { J . ideal J (R Quot I) }"
   1.214 +proof (rule bij_betw_byWitness[where ?f' = "\<lambda>X. \<Union> X"])
   1.215 +  show "\<forall>J \<in> { J. ideal J R \<and> I \<subseteq> J }. (\<lambda>X. \<Union> X) ((+>) I ` J) = J"
   1.216 +    using assms ideal_incl_iff by blast
   1.217 +next
   1.218 +  show "(\<lambda>J. (+>) I ` J) ` { J. ideal J R \<and> I \<subseteq> J } \<subseteq> { J. ideal J (R Quot I) }"
   1.219 +    using assms ring_ideal_imp_quot_ideal by auto
   1.220 +next
   1.221 +  show "(\<lambda>X. \<Union> X) ` { J. ideal J (R Quot I) } \<subseteq> { J. ideal J R \<and> I \<subseteq> J }"
   1.222 +  proof
   1.223 +    fix J assume "J \<in> ((\<lambda>X. \<Union> X) ` { J. ideal J (R Quot I) })"
   1.224 +    then obtain J' where J': "ideal J' (R Quot I)" "J = \<Union> J'" by blast
   1.225 +    hence "ideal J R"
   1.226 +      using assms quot_ideal_imp_ring_ideal by auto
   1.227 +    moreover have "I \<in> J'"
   1.228 +      using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF J'(1)]] unfolding FactRing_def by simp
   1.229 +    ultimately show "J \<in> { J. ideal J R \<and> I \<subseteq> J }" using J'(2) by auto
   1.230 +  qed
   1.231 +next
   1.232 +  show "\<forall>J' \<in> { J. ideal J (R Quot I) }. ((+>) I ` (\<Union> J')) = J'"
   1.233 +  proof
   1.234 +    fix J' assume "J' \<in> { J. ideal J (R Quot I) }"
   1.235 +    hence subset: "J' \<subseteq> carrier (R Quot I) \<and> ideal J' (R Quot I)"
   1.236 +      using additive_subgroup.a_subset ideal_def by blast
   1.237 +    hence "((+>) I ` (\<Union> J')) \<subseteq> J'"
   1.238 +      using canonical_proj_vimage_in_carrier canonical_proj_vimage_mem_iff
   1.239 +      by (meson assms contra_subsetD image_subsetI)
   1.240 +    moreover have "J' \<subseteq> ((+>) I ` (\<Union> J'))"
   1.241 +    proof
   1.242 +      fix x assume "x \<in> J'"
   1.243 +      then obtain r where r: "r \<in> carrier R" "x = I +> r"
   1.244 +        using subset unfolding FactRing_def A_RCOSETS_def'[of R I] by auto
   1.245 +      hence "r \<in> (\<Union> J')"
   1.246 +        using \<open>x \<in> J'\<close> assms canonical_proj_vimage_mem_iff subset by blast
   1.247 +      thus "x \<in> ((+>) I ` (\<Union> J'))" using r(2) by blast
   1.248 +    qed
   1.249 +    ultimately show "((+>) I ` (\<Union> J')) = J'" by blast
   1.250 +  qed
   1.251 +qed
   1.252 +
   1.253 +lemma (in cring) quot_domain_imp_primeideal:
   1.254 +  assumes "ideal P R"
   1.255 +  shows "domain (R Quot P) \<Longrightarrow> primeideal P R"
   1.256 +proof -
   1.257 +  assume A: "domain (R Quot P)" show "primeideal P R"
   1.258 +  proof (rule primeidealI)
   1.259 +    show "ideal P R" using assms .
   1.260 +    show "cring R" using is_cring .
   1.261 +  next
   1.262 +    show "carrier R \<noteq> P"
   1.263 +    proof (rule ccontr)
   1.264 +      assume "\<not> carrier R \<noteq> P" hence "carrier R = P" by simp
   1.265 +      hence "\<And>I. I \<in> carrier (R Quot P) \<Longrightarrow> I = P"
   1.266 +        unfolding FactRing_def A_RCOSETS_def' apply simp
   1.267 +        using a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1) by blast
   1.268 +      hence "\<one>\<^bsub>(R Quot P)\<^esub> = \<zero>\<^bsub>(R Quot P)\<^esub>"
   1.269 +        by (metis assms ideal.quotient_is_ring ring.ring_simprules(2) ring.ring_simprules(6))
   1.270 +      thus False using domain.one_not_zero[OF A] by simp
   1.271 +    qed
   1.272 +  next
   1.273 +    fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and ab: "a \<otimes> b \<in> P"
   1.274 +    hence "P +> (a \<otimes> b) = \<zero>\<^bsub>(R Quot P)\<^esub>" unfolding FactRing_def
   1.275 +      by (simp add: a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1))
   1.276 +    moreover have "(P +> a) \<otimes>\<^bsub>(R Quot P)\<^esub> (P +> b) = P +> (a \<otimes> b)" unfolding FactRing_def
   1.277 +      using a b by (simp add: assms ideal.rcoset_mult_add)
   1.278 +    moreover have "P +> a \<in> carrier (R Quot P) \<and> P +> b \<in> carrier (R Quot P)"
   1.279 +      by (simp add: a b FactRing_def a_rcosetsI additive_subgroup.a_subset assms ideal.axioms(1))
   1.280 +    ultimately have "P +> a = \<zero>\<^bsub>(R Quot P)\<^esub> \<or> P +> b = \<zero>\<^bsub>(R Quot P)\<^esub>"
   1.281 +      using domain.integral[OF A, of "P +> a" "P +> b"] by auto
   1.282 +    thus "a \<in> P \<or> b \<in> P" unfolding FactRing_def apply simp
   1.283 +      using a b assms a_coset_join1 additive_subgroup.a_subgroup ideal.axioms(1) by blast
   1.284 +  qed
   1.285 +qed
   1.286 +
   1.287 +lemma (in cring) quot_domain_iff_primeideal:
   1.288 +  assumes "ideal P R"
   1.289 +  shows "domain (R Quot P) = primeideal P R"
   1.290 +  using quot_domain_imp_primeideal[OF assms] primeideal.quotient_is_domain[of P R] by auto
   1.291 +
   1.292 +
   1.293 +subsection \<open>Isomorphism\<close>
   1.294 +
   1.295 +definition
   1.296 +  ring_iso :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<Rightarrow> 'b) set"
   1.297 +  where "ring_iso R S = { h. h \<in> ring_hom R S \<and> bij_betw h (carrier R) (carrier S) }"
   1.298 +
   1.299 +definition
   1.300 +  is_ring_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<simeq>" 60)
   1.301 +  where "R \<simeq> S = (ring_iso R S \<noteq> {})"
   1.302 +
   1.303 +definition
   1.304 +  morphic_prop :: "_ \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   1.305 +  where "morphic_prop R P =
   1.306 +           ((P \<one>\<^bsub>R\<^esub>) \<and>
   1.307 +            (\<forall>r \<in> carrier R. P r) \<and>
   1.308 +            (\<forall>r1 \<in> carrier R. \<forall>r2 \<in> carrier R. P (r1 \<otimes>\<^bsub>R\<^esub> r2)) \<and>
   1.309 +            (\<forall>r1 \<in> carrier R. \<forall>r2 \<in> carrier R. P (r1 \<oplus>\<^bsub>R\<^esub> r2)))"
   1.310 +
   1.311 +lemma ring_iso_memI:
   1.312 +  fixes R (structure) and S (structure)
   1.313 +  assumes "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S"
   1.314 +      and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
   1.315 +      and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
   1.316 +      and "h \<one> = \<one>\<^bsub>S\<^esub>"
   1.317 +      and "bij_betw h (carrier R) (carrier S)"
   1.318 +  shows "h \<in> ring_iso R S"
   1.319 +  by (auto simp add: ring_hom_memI assms ring_iso_def)
   1.320 +
   1.321 +lemma ring_iso_memE:
   1.322 +  fixes R (structure) and S (structure)
   1.323 +  assumes "h \<in> ring_iso R S"
   1.324 +  shows "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S"
   1.325 +   and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
   1.326 +   and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
   1.327 +   and "h \<one> = \<one>\<^bsub>S\<^esub>"
   1.328 +   and "bij_betw h (carrier R) (carrier S)"
   1.329 +  using assms unfolding ring_iso_def ring_hom_def by auto
   1.330 +
   1.331 +lemma morphic_propI:
   1.332 +  fixes R (structure)
   1.333 +  assumes "P \<one>"
   1.334 +    and "\<And>r. r \<in> carrier R \<Longrightarrow> P r"
   1.335 +    and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<otimes> r2)"
   1.336 +    and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<oplus> r2)"
   1.337 +  shows "morphic_prop R P"
   1.338 +  unfolding morphic_prop_def using assms by auto
   1.339 +
   1.340 +lemma morphic_propE:
   1.341 +  fixes R (structure)
   1.342 +  assumes "morphic_prop R P"
   1.343 +  shows "P \<one>"
   1.344 +    and "\<And>r. r \<in> carrier R \<Longrightarrow> P r"
   1.345 +    and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<otimes> r2)"
   1.346 +    and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<oplus> r2)"
   1.347 +  using assms unfolding morphic_prop_def by auto
   1.348 +
   1.349 +lemma ring_iso_restrict:
   1.350 +  assumes "f \<in> ring_iso R S"
   1.351 +    and "\<And>r. r \<in> carrier R \<Longrightarrow> f r = g r"
   1.352 +    and "ring R"
   1.353 +  shows "g \<in> ring_iso R S"
   1.354 +proof (rule ring_iso_memI)
   1.355 +  show "bij_betw g (carrier R) (carrier S)"
   1.356 +    using assms(1-2) bij_betw_cong ring_iso_memE(5) by blast
   1.357 +  show "g \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
   1.358 +    using assms ring.ring_simprules(6) ring_iso_memE(4) by force
   1.359 +next
   1.360 +  fix x y assume x: "x \<in> carrier R" and y: "y \<in> carrier R"
   1.361 +  show "g x \<in> carrier S"
   1.362 +    using assms(1-2) ring_iso_memE(1) x by fastforce
   1.363 +  show "g (x \<otimes>\<^bsub>R\<^esub> y) = g x \<otimes>\<^bsub>S\<^esub> g y"
   1.364 +    by (metis assms ring.ring_simprules(5) ring_iso_memE(2) x y)
   1.365 +  show "g (x \<oplus>\<^bsub>R\<^esub> y) = g x \<oplus>\<^bsub>S\<^esub> g y"
   1.366 +    by (metis assms ring.ring_simprules(1) ring_iso_memE(3) x y)
   1.367 +qed
   1.368 +
   1.369 +lemma ring_iso_morphic_prop:
   1.370 +  assumes "f \<in> ring_iso R S"
   1.371 +    and "morphic_prop R P"
   1.372 +    and "\<And>r. P r \<Longrightarrow> f r = g r"
   1.373 +  shows "g \<in> ring_iso R S"
   1.374 +proof -
   1.375 +  have eq0: "\<And>r. r \<in> carrier R \<Longrightarrow> f r = g r"
   1.376 +   and eq1: "f \<one>\<^bsub>R\<^esub> = g \<one>\<^bsub>R\<^esub>"
   1.377 +   and eq2: "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> f (r1 \<otimes>\<^bsub>R\<^esub> r2) = g (r1 \<otimes>\<^bsub>R\<^esub> r2)"
   1.378 +   and eq3: "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> f (r1 \<oplus>\<^bsub>R\<^esub> r2) = g (r1 \<oplus>\<^bsub>R\<^esub> r2)"
   1.379 +    using assms(2-3) unfolding morphic_prop_def by auto
   1.380 +  show ?thesis
   1.381 +    apply (rule ring_iso_memI)
   1.382 +    using assms(1) eq0 ring_iso_memE(1) apply fastforce
   1.383 +    apply (metis assms(1) eq0 eq2 ring_iso_memE(2))
   1.384 +    apply (metis assms(1) eq0 eq3 ring_iso_memE(3))
   1.385 +    using assms(1) eq1 ring_iso_memE(4) apply fastforce
   1.386 +    using assms(1) bij_betw_cong eq0 ring_iso_memE(5) by blast
   1.387 +qed
   1.388 +
   1.389 +lemma (in ring) ring_hom_imp_img_ring:
   1.390 +  assumes "h \<in> ring_hom R S"
   1.391 +  shows "ring (S \<lparr> carrier := h ` (carrier R), one := h \<one>, zero := h \<zero> \<rparr>)" (is "ring ?h_img")
   1.392 +proof -
   1.393 +  have "h \<in> hom (add_monoid R) (add_monoid S)"
   1.394 +    using assms unfolding hom_def ring_hom_def by auto
   1.395 +  hence "comm_group ((add_monoid S) \<lparr>  carrier := h ` (carrier R), one := h \<zero> \<rparr>)"
   1.396 +    using add.hom_imp_img_comm_group[of h "add_monoid S"] by simp
   1.397 +  hence comm_group: "comm_group (add_monoid ?h_img)"
   1.398 +    by (auto intro: comm_monoidI simp add: monoid.defs)
   1.399 +
   1.400 +  moreover have "h \<in> hom R S"
   1.401 +    using assms unfolding ring_hom_def hom_def by auto
   1.402 +  hence "monoid (S \<lparr>  carrier := h ` (carrier R), one := h \<one> \<rparr>)"
   1.403 +    using hom_imp_img_monoid[of h S] by simp
   1.404 +  hence monoid: "monoid ?h_img"
   1.405 +    unfolding monoid_def by (simp add: monoid.defs)
   1.406 +
   1.407 +  show ?thesis
   1.408 +  proof (rule ringI, simp_all add: comm_group_abelian_groupI[OF comm_group] monoid)
   1.409 +    fix x y z assume "x \<in> h ` carrier R" "y \<in> h ` carrier R" "z \<in> h ` carrier R"
   1.410 +    then obtain r1 r2 r3
   1.411 +      where r1: "r1 \<in> carrier R" "x = h r1"
   1.412 +        and r2: "r2 \<in> carrier R" "y = h r2"
   1.413 +        and r3: "r3 \<in> carrier R" "z = h r3" by blast
   1.414 +    hence "(x \<oplus>\<^bsub>S\<^esub> y) \<otimes>\<^bsub>S\<^esub> z = h ((r1 \<oplus> r2) \<otimes> r3)"
   1.415 +      using ring_hom_memE[OF assms] by auto
   1.416 +    also have " ... = h ((r1 \<otimes> r3) \<oplus> (r2 \<otimes> r3))"
   1.417 +      using l_distr[OF r1(1) r2(1) r3(1)] by simp
   1.418 +    also have " ... = (x \<otimes>\<^bsub>S\<^esub> z) \<oplus>\<^bsub>S\<^esub> (y \<otimes>\<^bsub>S\<^esub> z)"
   1.419 +      using ring_hom_memE[OF assms] r1 r2 r3 by auto
   1.420 +    finally show "(x \<oplus>\<^bsub>S\<^esub> y) \<otimes>\<^bsub>S\<^esub> z = (x \<otimes>\<^bsub>S\<^esub> z) \<oplus>\<^bsub>S\<^esub> (y \<otimes>\<^bsub>S\<^esub> z)" .
   1.421 +
   1.422 +    have "z \<otimes>\<^bsub>S\<^esub> (x \<oplus>\<^bsub>S\<^esub> y) = h (r3 \<otimes> (r1 \<oplus> r2))"
   1.423 +      using ring_hom_memE[OF assms] r1 r2 r3 by auto
   1.424 +    also have " ... =  h ((r3 \<otimes> r1) \<oplus> (r3 \<otimes> r2))"
   1.425 +      using r_distr[OF r1(1) r2(1) r3(1)] by simp
   1.426 +    also have " ... = (z \<otimes>\<^bsub>S\<^esub> x) \<oplus>\<^bsub>S\<^esub> (z \<otimes>\<^bsub>S\<^esub> y)"
   1.427 +      using ring_hom_memE[OF assms] r1 r2 r3 by auto
   1.428 +    finally show "z \<otimes>\<^bsub>S\<^esub> (x \<oplus>\<^bsub>S\<^esub> y) = (z \<otimes>\<^bsub>S\<^esub> x) \<oplus>\<^bsub>S\<^esub> (z \<otimes>\<^bsub>S\<^esub> y)" .
   1.429 +  qed
   1.430 +qed
   1.431 +
   1.432 +lemma (in ring) ring_iso_imp_img_ring:
   1.433 +  assumes "h \<in> ring_iso R S"
   1.434 +  shows "ring (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)"
   1.435 +proof -
   1.436 +  have "ring (S \<lparr> carrier := h ` (carrier R), one := h \<one>, zero := h \<zero> \<rparr>)"
   1.437 +    using ring_hom_imp_img_ring[of h S] assms unfolding ring_iso_def by auto
   1.438 +  moreover have "h ` (carrier R) = carrier S"
   1.439 +    using assms unfolding ring_iso_def bij_betw_def by auto
   1.440 +  ultimately show ?thesis by simp
   1.441 +qed
   1.442 +
   1.443 +lemma (in cring) ring_iso_imp_img_cring:
   1.444 +  assumes "h \<in> ring_iso R S"
   1.445 +  shows "cring (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" (is "cring ?h_img")
   1.446 +proof -
   1.447 +  note m_comm
   1.448 +  interpret h_img?: ring ?h_img
   1.449 +    using ring_iso_imp_img_ring[OF assms] .
   1.450 +  show ?thesis 
   1.451 +  proof (unfold_locales)
   1.452 +    fix x y assume "x \<in> carrier ?h_img" "y \<in> carrier ?h_img"
   1.453 +    then obtain r1 r2
   1.454 +      where r1: "r1 \<in> carrier R" "x = h r1"
   1.455 +        and r2: "r2 \<in> carrier R" "y = h r2"
   1.456 +      using assms image_iff[where ?f = h and ?A = "carrier R"]
   1.457 +      unfolding ring_iso_def bij_betw_def by auto
   1.458 +    have "x \<otimes>\<^bsub>(?h_img)\<^esub> y = h (r1 \<otimes> r2)"
   1.459 +      using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto
   1.460 +    also have " ... = h (r2 \<otimes> r1)"
   1.461 +      using m_comm[OF r1(1) r2(1)] by simp
   1.462 +    also have " ... = y \<otimes>\<^bsub>(?h_img)\<^esub> x"
   1.463 +      using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto
   1.464 +    finally show "x \<otimes>\<^bsub>(?h_img)\<^esub> y = y \<otimes>\<^bsub>(?h_img)\<^esub> x" .
   1.465 +  qed
   1.466 +qed
   1.467 +
   1.468 +lemma (in domain) ring_iso_imp_img_domain:
   1.469 +  assumes "h \<in> ring_iso R S"
   1.470 +  shows "domain (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" (is "domain ?h_img")
   1.471 +proof -
   1.472 +  note aux = m_closed integral one_not_zero one_closed zero_closed
   1.473 +  interpret h_img?: cring ?h_img
   1.474 +    using ring_iso_imp_img_cring[OF assms] .
   1.475 +  show ?thesis 
   1.476 +  proof (unfold_locales)
   1.477 +    show "\<one>\<^bsub>?h_img\<^esub> \<noteq> \<zero>\<^bsub>?h_img\<^esub>"
   1.478 +      using ring_iso_memE(5)[OF assms] aux(3-4)
   1.479 +      unfolding bij_betw_def inj_on_def by force
   1.480 +  next
   1.481 +    fix a b
   1.482 +    assume A: "a \<otimes>\<^bsub>?h_img\<^esub> b = \<zero>\<^bsub>?h_img\<^esub>" "a \<in> carrier ?h_img" "b \<in> carrier ?h_img"
   1.483 +    then obtain r1 r2
   1.484 +      where r1: "r1 \<in> carrier R" "a = h r1"
   1.485 +        and r2: "r2 \<in> carrier R" "b = h r2"
   1.486 +      using assms image_iff[where ?f = h and ?A = "carrier R"]
   1.487 +      unfolding ring_iso_def bij_betw_def by auto
   1.488 +    hence "a \<otimes>\<^bsub>?h_img\<^esub> b = h (r1 \<otimes> r2)"
   1.489 +      using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto
   1.490 +    hence "h (r1 \<otimes> r2) = h \<zero>"
   1.491 +      using A(1) by simp
   1.492 +    hence "r1 \<otimes> r2 = \<zero>"
   1.493 +      using ring_iso_memE(5)[OF assms] aux(1)[OF r1(1) r2(1)] aux(5)
   1.494 +      unfolding bij_betw_def inj_on_def by force
   1.495 +    hence "r1 = \<zero> \<or> r2 = \<zero>"
   1.496 +      using aux(2)[OF _ r1(1) r2(1)] by simp
   1.497 +    thus "a = \<zero>\<^bsub>?h_img\<^esub> \<or> b = \<zero>\<^bsub>?h_img\<^esub>"
   1.498 +      unfolding r1 r2 by auto
   1.499 +  qed
   1.500 +qed
   1.501 +
   1.502 +lemma (in field) ring_iso_imp_img_field:
   1.503 +  assumes "h \<in> ring_iso R S"
   1.504 +  shows "field (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" (is "field ?h_img")
   1.505 +proof -
   1.506 +  interpret h_img?: domain ?h_img
   1.507 +    using ring_iso_imp_img_domain[OF assms] .
   1.508 +  show ?thesis
   1.509 +  proof (unfold_locales, auto simp add: Units_def)
   1.510 +    interpret field R using field_axioms .
   1.511 +    fix a assume a: "a \<in> carrier S" "a \<otimes>\<^bsub>S\<^esub> h \<zero> = h \<one>"
   1.512 +    then obtain r where r: "r \<in> carrier R" "a = h r"
   1.513 +      using assms image_iff[where ?f = h and ?A = "carrier R"]
   1.514 +      unfolding ring_iso_def bij_betw_def by auto
   1.515 +    have "a \<otimes>\<^bsub>S\<^esub> h \<zero> = h (r \<otimes> \<zero>)" unfolding r(2)
   1.516 +      using ring_iso_memE(2)[OF assms r(1)] by simp
   1.517 +    hence "h \<one> = h \<zero>"
   1.518 +      using r(1) a(2) by simp
   1.519 +    thus False
   1.520 +      using ring_iso_memE(5)[OF assms]
   1.521 +      unfolding bij_betw_def inj_on_def by force
   1.522 +  next
   1.523 +    interpret field R using field_axioms .
   1.524 +    fix s assume s: "s \<in> carrier S" "s \<noteq> h \<zero>"
   1.525 +    then obtain r where r: "r \<in> carrier R" "s = h r"
   1.526 +      using assms image_iff[where ?f = h and ?A = "carrier R"]
   1.527 +      unfolding ring_iso_def bij_betw_def by auto
   1.528 +    hence "r \<noteq> \<zero>" using s(2) by auto 
   1.529 +    hence inv_r: "inv r \<in> carrier R" "inv r \<noteq> \<zero>" "r \<otimes> inv r = \<one>" "inv r \<otimes> r = \<one>"
   1.530 +      using field_Units r(1) by auto
   1.531 +    have "h (inv r) \<otimes>\<^bsub>S\<^esub> h r = h \<one>" and "h r \<otimes>\<^bsub>S\<^esub> h (inv r) = h \<one>"
   1.532 +      using ring_iso_memE(2)[OF assms inv_r(1) r(1)] inv_r(3-4)
   1.533 +            ring_iso_memE(2)[OF assms r(1) inv_r(1)] by auto
   1.534 +    thus "\<exists>s' \<in> carrier S. s' \<otimes>\<^bsub>S\<^esub> s = h \<one> \<and> s \<otimes>\<^bsub>S\<^esub> s' = h \<one>"
   1.535 +      using ring_iso_memE(1)[OF assms inv_r(1)] r(2) by auto
   1.536 +  qed
   1.537 +qed
   1.538 +
   1.539 +lemma ring_iso_same_card: "R \<simeq> S \<Longrightarrow> card (carrier R) = card (carrier S)"
   1.540 +proof -
   1.541 +  assume "R \<simeq> S"
   1.542 +  then obtain h where "bij_betw h (carrier R) (carrier S)"
   1.543 +    unfolding is_ring_iso_def ring_iso_def by auto
   1.544 +  thus "card (carrier R) = card (carrier S)"
   1.545 +    using bij_betw_same_card[of h "carrier R" "carrier S"] by simp
   1.546 +qed
   1.547 +
   1.548 +lemma ring_iso_set_refl: "id \<in> ring_iso R R"
   1.549 +  by (rule ring_iso_memI) (auto)
   1.550 +
   1.551 +corollary ring_iso_refl: "R \<simeq> R"
   1.552 +  using is_ring_iso_def ring_iso_set_refl by auto 
   1.553 +
   1.554 +lemma ring_iso_set_trans:
   1.555 +  "\<lbrakk> f \<in> ring_iso R S; g \<in> ring_iso S Q \<rbrakk> \<Longrightarrow> (g \<circ> f) \<in> ring_iso R Q"
   1.556 +  unfolding ring_iso_def using bij_betw_trans ring_hom_trans by fastforce 
   1.557 +
   1.558 +corollary ring_iso_trans: "\<lbrakk> R \<simeq> S; S \<simeq> Q \<rbrakk> \<Longrightarrow> R \<simeq> Q"
   1.559 +  using ring_iso_set_trans unfolding is_ring_iso_def by blast 
   1.560 +
   1.561 +lemma ring_iso_set_sym:
   1.562 +  assumes "ring R"
   1.563 +  shows "h \<in> ring_iso R S \<Longrightarrow> (inv_into (carrier R) h) \<in> ring_iso S R"
   1.564 +proof -
   1.565 +  assume h: "h \<in> ring_iso R S"
   1.566 +  hence h_hom:  "h \<in> ring_hom R S"
   1.567 +    and h_surj: "h ` (carrier R) = (carrier S)"
   1.568 +    and h_inj:  "\<And> x1 x2. \<lbrakk> x1 \<in> carrier R; x2 \<in> carrier R \<rbrakk> \<Longrightarrow>  h x1 = h x2 \<Longrightarrow> x1 = x2"
   1.569 +    unfolding ring_iso_def bij_betw_def inj_on_def by auto
   1.570 +
   1.571 +  have h_inv_bij: "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)"
   1.572 +      using bij_betw_inv_into h ring_iso_def by fastforce
   1.573 +
   1.574 +  show "inv_into (carrier R) h \<in> ring_iso S R"
   1.575 +    apply (rule ring_iso_memI)
   1.576 +    apply (simp add: h_surj inv_into_into)
   1.577 +    apply (auto simp add: h_inv_bij)
   1.578 +    apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into
   1.579 +           ring.ring_simprules(5) ring_hom_closed ring_hom_mult)
   1.580 +    apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into
   1.581 +           ring.ring_simprules(1) ring_hom_add ring_hom_closed)
   1.582 +    by (metis (no_types, hide_lams) assms f_inv_into_f h_hom h_inj
   1.583 +        imageI inv_into_into ring.ring_simprules(6) ring_hom_one)
   1.584 +qed
   1.585 +
   1.586 +corollary ring_iso_sym:
   1.587 +  assumes "ring R"
   1.588 +  shows "R \<simeq> S \<Longrightarrow> S \<simeq> R"
   1.589 +  using assms ring_iso_set_sym unfolding is_ring_iso_def by auto 
   1.590 +
   1.591 +lemma (in ring_hom_ring) the_elem_simp [simp]:
   1.592 +  "\<And>x. x \<in> carrier R \<Longrightarrow> the_elem (h ` ((a_kernel R S h) +> x)) = h x"
   1.593 +proof -
   1.594 +  fix x assume x: "x \<in> carrier R"
   1.595 +  hence "h x \<in> h ` ((a_kernel R S h) +> x)"
   1.596 +    using homeq_imp_rcos by blast
   1.597 +  thus "the_elem (h ` ((a_kernel R S h) +> x)) = h x"
   1.598 +    by (metis (no_types, lifting) x empty_iff homeq_imp_rcos rcos_imp_homeq the_elem_image_unique)
   1.599 +qed
   1.600 +
   1.601 +lemma (in ring_hom_ring) the_elem_inj:
   1.602 +  "\<And>X Y. \<lbrakk> X \<in> carrier (R Quot (a_kernel R S h)); Y \<in> carrier (R Quot (a_kernel R S h)) \<rbrakk> \<Longrightarrow>
   1.603 +           the_elem (h ` X) = the_elem (h ` Y) \<Longrightarrow> X = Y"
   1.604 +proof -
   1.605 +  fix X Y
   1.606 +  assume "X \<in> carrier (R Quot (a_kernel R S h))"
   1.607 +     and "Y \<in> carrier (R Quot (a_kernel R S h))"
   1.608 +     and Eq: "the_elem (h ` X) = the_elem (h ` Y)"
   1.609 +  then obtain x y where x: "x \<in> carrier R" "X = (a_kernel R S h) +> x"
   1.610 +                    and y: "y \<in> carrier R" "Y = (a_kernel R S h) +> y"
   1.611 +    unfolding FactRing_def A_RCOSETS_def' by auto
   1.612 +  hence "h x = h y" using Eq by simp
   1.613 +  hence "x \<ominus> y \<in> (a_kernel R S h)"
   1.614 +    by (simp add: a_minus_def abelian_subgroup.a_rcos_module_imp
   1.615 +                  abelian_subgroup_a_kernel homeq_imp_rcos x(1) y(1))
   1.616 +  thus "X = Y"
   1.617 +    by (metis R.a_coset_add_inv1 R.minus_eq abelian_subgroup.a_rcos_const
   1.618 +        abelian_subgroup_a_kernel additive_subgroup.a_subset additive_subgroup_a_kernel x y)
   1.619 +qed
   1.620 +
   1.621 +lemma (in ring_hom_ring) quot_mem:
   1.622 +  "\<And>X. X \<in> carrier (R Quot (a_kernel R S h)) \<Longrightarrow> \<exists>x \<in> carrier R. X = (a_kernel R S h) +> x"
   1.623 +proof -
   1.624 +  fix X assume "X \<in> carrier (R Quot (a_kernel R S h))"
   1.625 +  thus "\<exists>x \<in> carrier R. X = (a_kernel R S h) +> x"
   1.626 +    unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (simp add: a_r_coset_def)
   1.627 +qed
   1.628 +
   1.629 +lemma (in ring_hom_ring) the_elem_wf:
   1.630 +  "\<And>X. X \<in> carrier (R Quot (a_kernel R S h)) \<Longrightarrow> \<exists>y \<in> carrier S. (h ` X) = { y }"
   1.631 +proof -
   1.632 +  fix X assume "X \<in> carrier (R Quot (a_kernel R S h))"
   1.633 +  then obtain x where x: "x \<in> carrier R" and X: "X = (a_kernel R S h) +> x"
   1.634 +    using quot_mem by blast
   1.635 +  hence "\<And>x'. x' \<in> X \<Longrightarrow> h x' = h x"
   1.636 +  proof -
   1.637 +    fix x' assume "x' \<in> X" hence "x' \<in> (a_kernel R S h) +> x" using X by simp
   1.638 +    then obtain k where k: "k \<in> a_kernel R S h" "x' = k \<oplus> x"
   1.639 +      by (metis R.add.inv_closed R.add.m_assoc R.l_neg R.r_zero
   1.640 +          abelian_subgroup.a_elemrcos_carrier
   1.641 +          abelian_subgroup.a_rcos_module_imp abelian_subgroup_a_kernel x)
   1.642 +    hence "h x' = h k \<oplus>\<^bsub>S\<^esub> h x"
   1.643 +      by (meson additive_subgroup.a_Hcarr additive_subgroup_a_kernel hom_add x)
   1.644 +    also have " ... =  h x"
   1.645 +      using k by (auto simp add: x)
   1.646 +    finally show "h x' = h x" .
   1.647 +  qed
   1.648 +  moreover have "h x \<in> h ` X"
   1.649 +    by (simp add: X homeq_imp_rcos x)
   1.650 +  ultimately have "(h ` X) = { h x }"
   1.651 +    by blast
   1.652 +  thus "\<exists>y \<in> carrier S. (h ` X) = { y }" using x by simp
   1.653 +qed
   1.654 +
   1.655 +corollary (in ring_hom_ring) the_elem_wf':
   1.656 +  "\<And>X. X \<in> carrier (R Quot (a_kernel R S h)) \<Longrightarrow> \<exists>r \<in> carrier R. (h ` X) = { h r }"
   1.657 +  using the_elem_wf by (metis quot_mem the_elem_eq the_elem_simp) 
   1.658 +
   1.659 +lemma (in ring_hom_ring) the_elem_hom:
   1.660 +  "(\<lambda>X. the_elem (h ` X)) \<in> ring_hom (R Quot (a_kernel R S h)) S"
   1.661 +proof (rule ring_hom_memI)
   1.662 +  show "\<And>x. x \<in> carrier (R Quot a_kernel R S h) \<Longrightarrow> the_elem (h ` x) \<in> carrier S"
   1.663 +    using the_elem_wf by fastforce
   1.664 +  
   1.665 +  show "the_elem (h ` \<one>\<^bsub>R Quot a_kernel R S h\<^esub>) = \<one>\<^bsub>S\<^esub>"
   1.666 +    unfolding FactRing_def  using the_elem_simp[of "\<one>\<^bsub>R\<^esub>"] by simp
   1.667 +
   1.668 +  fix X Y
   1.669 +  assume "X \<in> carrier (R Quot a_kernel R S h)"
   1.670 +     and "Y \<in> carrier (R Quot a_kernel R S h)"
   1.671 +  then obtain x y where x: "x \<in> carrier R" "X = (a_kernel R S h) +> x"
   1.672 +                    and y: "y \<in> carrier R" "Y = (a_kernel R S h) +> y"
   1.673 +    using quot_mem by blast
   1.674 +
   1.675 +  have "X \<otimes>\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \<otimes> y)"
   1.676 +    by (simp add: FactRing_def ideal.rcoset_mult_add kernel_is_ideal x y)
   1.677 +  thus "the_elem (h ` (X \<otimes>\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \<otimes>\<^bsub>S\<^esub> the_elem (h ` Y)"
   1.678 +    by (simp add: x y)
   1.679 +
   1.680 +  have "X \<oplus>\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \<oplus> y)"
   1.681 +    using ideal.rcos_ring_hom kernel_is_ideal ring_hom_add x y by fastforce
   1.682 +  thus "the_elem (h ` (X \<oplus>\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \<oplus>\<^bsub>S\<^esub> the_elem (h ` Y)"
   1.683 +    by (simp add: x y)
   1.684 +qed
   1.685 +
   1.686 +lemma (in ring_hom_ring) the_elem_surj:
   1.687 +    "(\<lambda>X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h)) = (h ` (carrier R))"
   1.688 +proof
   1.689 +  show "(\<lambda>X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h) \<subseteq> h ` carrier R"
   1.690 +    using the_elem_wf' by fastforce
   1.691 +next
   1.692 +  show "h ` carrier R \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h)"
   1.693 +  proof
   1.694 +    fix y assume "y \<in> h ` carrier R"
   1.695 +    then obtain x where x: "x \<in> carrier R" "h x = y"
   1.696 +      by (metis image_iff)
   1.697 +    hence "the_elem (h ` ((a_kernel R S h) +> x)) = y" by simp
   1.698 +    moreover have "(a_kernel R S h) +> x \<in> carrier (R Quot (a_kernel R S h))"
   1.699 +     unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (auto simp add: x a_r_coset_def)
   1.700 +    ultimately show "y \<in> (\<lambda>X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h))" by blast
   1.701 +  qed
   1.702 +qed
   1.703 +
   1.704 +proposition (in ring_hom_ring) FactRing_iso_set_aux:
   1.705 +  "(\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot (a_kernel R S h)) (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
   1.706 +proof -
   1.707 +  have "bij_betw (\<lambda>X. the_elem (h ` X)) (carrier (R Quot a_kernel R S h)) (h ` (carrier R))"
   1.708 +    unfolding bij_betw_def inj_on_def using the_elem_surj the_elem_inj by simp
   1.709 +
   1.710 +  moreover
   1.711 +  have "(\<lambda>X. the_elem (h ` X)): carrier (R Quot (a_kernel R S h)) \<rightarrow> h ` (carrier R)"
   1.712 +    using the_elem_wf' by fastforce
   1.713 +  hence "(\<lambda>X. the_elem (h ` X)) \<in> ring_hom (R Quot (a_kernel R S h)) (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
   1.714 +    using the_elem_hom the_elem_wf' unfolding ring_hom_def by simp
   1.715 +
   1.716 +  ultimately show ?thesis unfolding ring_iso_def using the_elem_hom by simp
   1.717 +qed
   1.718 +
   1.719 +theorem (in ring_hom_ring) FactRing_iso_set:
   1.720 +  assumes "h ` carrier R = carrier S"
   1.721 +  shows "(\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot (a_kernel R S h)) S"
   1.722 +  using FactRing_iso_set_aux assms by auto
   1.723 +
   1.724 +corollary (in ring_hom_ring) FactRing_iso:
   1.725 +  assumes "h ` carrier R = carrier S"
   1.726 +  shows "R Quot (a_kernel R S h) \<simeq> S"
   1.727 +  using FactRing_iso_set assms is_ring_iso_def by auto
   1.728 +
   1.729 +lemma (in ring_hom_ring) img_is_ring: "ring (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
   1.730 +proof -
   1.731 +  let ?the_elem = "\<lambda>X. the_elem (h ` X)"
   1.732 +  have FactRing_is_ring: "ring (R Quot (a_kernel R S h))"
   1.733 +    by (simp add: ideal.quotient_is_ring kernel_is_ideal)
   1.734 +  have "ring ((S \<lparr> carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \<rparr>)
   1.735 +                 \<lparr>     one := ?the_elem \<one>\<^bsub>(R Quot (a_kernel R S h))\<^esub>,
   1.736 +                      zero := ?the_elem \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub> \<rparr>)"
   1.737 +    using ring.ring_iso_imp_img_ring[OF FactRing_is_ring, of ?the_elem
   1.738 +          "S \<lparr> carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \<rparr>"]
   1.739 +          FactRing_iso_set_aux the_elem_surj by auto
   1.740 +
   1.741 +  moreover
   1.742 +  have "\<zero> \<in> (a_kernel R S h)"
   1.743 +    using a_kernel_def'[of R S h] by auto
   1.744 +  hence "\<one> \<in> (a_kernel R S h) +> \<one>"
   1.745 +    using a_r_coset_def'[of R "a_kernel R S h" \<one>] by force
   1.746 +  hence "\<one>\<^bsub>S\<^esub> \<in> (h ` ((a_kernel R S h) +> \<one>))"
   1.747 +    using hom_one by force
   1.748 +  hence "?the_elem \<one>\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \<one>\<^bsub>S\<^esub>"
   1.749 +    using the_elem_wf[of "(a_kernel R S h) +> \<one>"] by (simp add: FactRing_def)
   1.750 +  
   1.751 +  moreover
   1.752 +  have "\<zero>\<^bsub>S\<^esub> \<in> (h ` (a_kernel R S h))"
   1.753 +    using a_kernel_def'[of R S h] hom_zero by force
   1.754 +  hence "\<zero>\<^bsub>S\<^esub> \<in> (h ` \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub>)"
   1.755 +    by (simp add: FactRing_def)
   1.756 +  hence "?the_elem \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \<zero>\<^bsub>S\<^esub>"
   1.757 +    using the_elem_wf[OF ring.ring_simprules(2)[OF FactRing_is_ring]]
   1.758 +    by (metis singletonD the_elem_eq) 
   1.759 +
   1.760 +  ultimately
   1.761 +  have "ring ((S \<lparr> carrier := h ` (carrier R) \<rparr>) \<lparr> one := \<one>\<^bsub>S\<^esub>, zero := \<zero>\<^bsub>S\<^esub> \<rparr>)"
   1.762 +    using the_elem_surj by simp
   1.763 +  thus ?thesis
   1.764 +    by auto
   1.765 +qed
   1.766 +
   1.767 +lemma (in ring_hom_ring) img_is_cring:
   1.768 +  assumes "cring S"
   1.769 +  shows "cring (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
   1.770 +proof -
   1.771 +  interpret ring "S \<lparr> carrier := h ` (carrier R) \<rparr>"
   1.772 +    using img_is_ring .
   1.773 +  show ?thesis
   1.774 +    apply unfold_locales
   1.775 +    using assms unfolding cring_def comm_monoid_def comm_monoid_axioms_def by auto
   1.776 +qed
   1.777 +
   1.778 +lemma (in ring_hom_ring) img_is_domain:
   1.779 +  assumes "domain S"
   1.780 +  shows "domain (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
   1.781 +proof -
   1.782 +  interpret cring "S \<lparr> carrier := h ` (carrier R) \<rparr>"
   1.783 +    using img_is_cring assms unfolding domain_def by simp
   1.784 +  show ?thesis
   1.785 +    apply unfold_locales
   1.786 +    using assms unfolding domain_def domain_axioms_def apply auto
   1.787 +    using hom_closed by blast 
   1.788 +qed
   1.789 +
   1.790 +proposition (in ring_hom_ring) primeideal_vimage:
   1.791 +  assumes "cring R"
   1.792 +  shows "primeideal P S \<Longrightarrow> primeideal { r \<in> carrier R. h r \<in> P } R"
   1.793 +proof -
   1.794 +  assume A: "primeideal P S"
   1.795 +  hence is_ideal: "ideal P S" unfolding primeideal_def by simp
   1.796 +  have "ring_hom_ring R (S Quot P) (((+>\<^bsub>S\<^esub>) P) \<circ> h)" (is "ring_hom_ring ?A ?B ?h")
   1.797 +    using ring_hom_trans[OF homh, of "(+>\<^bsub>S\<^esub>) P" "S Quot P"]
   1.798 +          ideal.rcos_ring_hom_ring[OF is_ideal] assms
   1.799 +    unfolding ring_hom_ring_def ring_hom_ring_axioms_def cring_def by simp
   1.800 +  then interpret hom: ring_hom_ring R "S Quot P" "((+>\<^bsub>S\<^esub>) P) \<circ> h" by simp
   1.801 +  
   1.802 +  have "inj_on (\<lambda>X. the_elem (?h ` X)) (carrier (R Quot (a_kernel R (S Quot P) ?h)))"
   1.803 +    using hom.the_elem_inj unfolding inj_on_def by simp
   1.804 +  moreover
   1.805 +  have "ideal (a_kernel R (S Quot P) ?h) R"
   1.806 +    using hom.kernel_is_ideal by auto
   1.807 +  have hom': "ring_hom_ring (R Quot (a_kernel R (S Quot P) ?h)) (S Quot P) (\<lambda>X. the_elem (?h ` X))"
   1.808 +    using hom.the_elem_hom hom.kernel_is_ideal
   1.809 +    by (meson hom.ring_hom_ring_axioms ideal.rcos_ring_hom_ring ring_hom_ring_axioms_def ring_hom_ring_def)
   1.810 +  
   1.811 +  ultimately
   1.812 +  have "primeideal (a_kernel R (S Quot P) ?h) R"
   1.813 +    using ring_hom_ring.inj_on_domain[OF hom'] primeideal.quotient_is_domain[OF A]
   1.814 +          cring.quot_domain_imp_primeideal[OF assms hom.kernel_is_ideal] by simp
   1.815 +  
   1.816 +  moreover have "a_kernel R (S Quot P) ?h = { r \<in> carrier R. h r \<in> P }"
   1.817 +  proof
   1.818 +    show "a_kernel R (S Quot P) ?h \<subseteq> { r \<in> carrier R. h r \<in> P }"
   1.819 +    proof 
   1.820 +      fix r assume "r \<in> a_kernel R (S Quot P) ?h"
   1.821 +      hence r: "r \<in> carrier R" "P +>\<^bsub>S\<^esub> (h r) = P"
   1.822 +        unfolding a_kernel_def kernel_def FactRing_def by auto
   1.823 +      hence "h r \<in> P"
   1.824 +        using S.a_rcosI R.l_zero S.l_zero additive_subgroup.a_subset[OF ideal.axioms(1)[OF is_ideal]]
   1.825 +              additive_subgroup.zero_closed[OF ideal.axioms(1)[OF is_ideal]] hom_closed by metis
   1.826 +      thus "r \<in> { r \<in> carrier R. h r \<in> P }" using r by simp
   1.827 +    qed
   1.828 +  next
   1.829 +    show "{ r \<in> carrier R. h r \<in> P } \<subseteq> a_kernel R (S Quot P) ?h"
   1.830 +    proof
   1.831 +      fix r assume "r \<in> { r \<in> carrier R. h r \<in> P }"
   1.832 +      hence r: "r \<in> carrier R" "h r \<in> P" by simp_all
   1.833 +      hence "?h r = P"
   1.834 +        by (simp add: S.a_coset_join2 additive_subgroup.a_subgroup ideal.axioms(1) is_ideal)
   1.835 +      thus "r \<in> a_kernel R (S Quot P) ?h"
   1.836 +        unfolding a_kernel_def kernel_def FactRing_def using r(1) by auto
   1.837 +    qed
   1.838 +  qed
   1.839 +  ultimately show "primeideal { r \<in> carrier R. h r \<in> P } R" by simp
   1.840 +qed
   1.841 +
   1.842  end