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.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.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.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.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.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.276 +    moreover have "(P +> a) \<otimes>\<^bsub>(R Quot P)\<^esub> (P +> b) = P +> (a \<otimes> b)" unfolding FactRing_def
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.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.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.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.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.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.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.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"