src/HOL/Algebra/RingHom.thy
 changeset 68551 b680e74eb6f2 parent 67613 ce654b0e6d69 child 68664 bd0df72c16d5
```     1.1 --- a/src/HOL/Algebra/RingHom.thy	Fri Jun 29 23:04:36 2018 +0200
1.2 +++ b/src/HOL/Algebra/RingHom.thy	Sat Jun 30 15:44:04 2018 +0100
1.3 @@ -203,4 +203,37 @@
1.4        show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
1.5  qed
1.6
1.7 +(*contributed by Paulo EmÃ­lio de Vilhena*)
1.8 +lemma (in ring_hom_ring) inj_on_domain:
1.9 +  assumes "inj_on h (carrier R)"
1.10 +  shows "domain S \<Longrightarrow> domain R"
1.11 +proof -
1.12 +  assume A: "domain S" show "domain R"
1.13 +  proof
1.14 +    have "h \<one> = \<one>\<^bsub>S\<^esub> \<and> h \<zero> = \<zero>\<^bsub>S\<^esub>" by simp
1.15 +    hence "h \<one> \<noteq> h \<zero>"
1.16 +      using domain.one_not_zero[OF A] by simp
1.17 +    thus "\<one> \<noteq> \<zero>"
1.18 +      using assms unfolding inj_on_def by fastforce
1.19 +  next
1.20 +    fix a b
1.21 +    assume a: "a \<in> carrier R"
1.22 +       and b: "b \<in> carrier R"
1.23 +    have "h (a \<otimes> b) = (h a) \<otimes>\<^bsub>S\<^esub> (h b)" by (simp add: a b)
1.24 +    also have " ... = (h b) \<otimes>\<^bsub>S\<^esub> (h a)" using a b A cringE(1)[of S]
1.25 +      by (simp add: cring.cring_simprules(14) domain_def)
1.26 +    also have " ... = h (b \<otimes> a)" by (simp add: a b)
1.27 +    finally have "h (a \<otimes> b) = h (b \<otimes> a)" .
1.28 +    thus "a \<otimes> b = b \<otimes> a"
1.29 +      using assms a b unfolding inj_on_def by simp
1.30 +
1.31 +    assume  ab: "a \<otimes> b = \<zero>"
1.32 +    hence "h (a \<otimes> b) = \<zero>\<^bsub>S\<^esub>" by simp
1.33 +    hence "(h a) \<otimes>\<^bsub>S\<^esub> (h b) = \<zero>\<^bsub>S\<^esub>" using a b by simp
1.34 +    hence "h a =  \<zero>\<^bsub>S\<^esub> \<or> h b =  \<zero>\<^bsub>S\<^esub>" using a b domain.integral[OF A] by simp
1.35 +    thus "a = \<zero> \<or> b = \<zero>"
1.36 +      using a b assms unfolding inj_on_def by force
1.37 +  qed
1.38 +qed
1.39 +
1.40  end
```