diff -r 516e81f75957 -r b680e74eb6f2 src/HOL/Algebra/RingHom.thy --- a/src/HOL/Algebra/RingHom.thy Fri Jun 29 23:04:36 2018 +0200 +++ b/src/HOL/Algebra/RingHom.thy Sat Jun 30 15:44:04 2018 +0100 @@ -203,4 +203,37 @@ show "x \ a_kernel R S h +> a" by (rule homeq_imp_rcos) qed +(*contributed by Paulo EmÃ­lio de Vilhena*) +lemma (in ring_hom_ring) inj_on_domain: + assumes "inj_on h (carrier R)" + shows "domain S \ domain R" +proof - + assume A: "domain S" show "domain R" + proof + have "h \ = \\<^bsub>S\<^esub> \ h \ = \\<^bsub>S\<^esub>" by simp + hence "h \ \ h \" + using domain.one_not_zero[OF A] by simp + thus "\ \ \" + using assms unfolding inj_on_def by fastforce + next + fix a b + assume a: "a \ carrier R" + and b: "b \ carrier R" + have "h (a \ b) = (h a) \\<^bsub>S\<^esub> (h b)" by (simp add: a b) + also have " ... = (h b) \\<^bsub>S\<^esub> (h a)" using a b A cringE(1)[of S] + by (simp add: cring.cring_simprules(14) domain_def) + also have " ... = h (b \ a)" by (simp add: a b) + finally have "h (a \ b) = h (b \ a)" . + thus "a \ b = b \ a" + using assms a b unfolding inj_on_def by simp + + assume ab: "a \ b = \" + hence "h (a \ b) = \\<^bsub>S\<^esub>" by simp + hence "(h a) \\<^bsub>S\<^esub> (h b) = \\<^bsub>S\<^esub>" using a b by simp + hence "h a = \\<^bsub>S\<^esub> \ h b = \\<^bsub>S\<^esub>" using a b domain.integral[OF A] by simp + thus "a = \ \ b = \" + using a b assms unfolding inj_on_def by force + qed +qed + end