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