src/HOL/Algebra/RingHom.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (21 months ago)
changeset 67022 49309fe530fd
parent 63167 0909deb8059b
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 (*  Title:      HOL/Algebra/RingHom.thy
     2     Author:     Stephan Hohe, TU Muenchen
     3 *)
     4 
     5 theory RingHom
     6 imports Ideal
     7 begin
     8 
     9 section \<open>Homomorphisms of Non-Commutative Rings\<close>
    10 
    11 text \<open>Lifting existing lemmas in a \<open>ring_hom_ring\<close> locale\<close>
    12 locale ring_hom_ring = R?: ring R + S?: ring S
    13     for R (structure) and S (structure) +
    14   fixes h
    15   assumes homh: "h \<in> ring_hom R S"
    16   notes hom_mult [simp] = ring_hom_mult [OF homh]
    17     and hom_one [simp] = ring_hom_one [OF homh]
    18 
    19 sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
    20   by standard (rule homh)
    21 
    22 sublocale ring_hom_ring \<subseteq> abelian_group?: abelian_group_hom R S
    23 apply (rule abelian_group_homI)
    24   apply (rule R.is_abelian_group)
    25  apply (rule S.is_abelian_group)
    26 apply (intro group_hom.intro group_hom_axioms.intro)
    27   apply (rule R.a_group)
    28  apply (rule S.a_group)
    29 apply (insert homh, unfold hom_def ring_hom_def)
    30 apply simp
    31 done
    32 
    33 lemma (in ring_hom_ring) is_ring_hom_ring:
    34   "ring_hom_ring R S h"
    35   by (rule ring_hom_ring_axioms)
    36 
    37 lemma ring_hom_ringI:
    38   fixes R (structure) and S (structure)
    39   assumes "ring R" "ring S"
    40   assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
    41           hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
    42       and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    43       and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
    44       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    45   shows "ring_hom_ring R S h"
    46 proof -
    47   interpret ring R by fact
    48   interpret ring S by fact
    49   show ?thesis apply unfold_locales
    50 apply (unfold ring_hom_def, safe)
    51    apply (simp add: hom_closed Pi_def)
    52   apply (erule (1) compatible_mult)
    53  apply (erule (1) compatible_add)
    54 apply (rule compatible_one)
    55 done
    56 qed
    57 
    58 lemma ring_hom_ringI2:
    59   assumes "ring R" "ring S"
    60   assumes h: "h \<in> ring_hom R S"
    61   shows "ring_hom_ring R S h"
    62 proof -
    63   interpret R: ring R by fact
    64   interpret S: ring S by fact
    65   show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    66     apply (rule R.is_ring)
    67     apply (rule S.is_ring)
    68     apply (rule h)
    69     done
    70 qed
    71 
    72 lemma ring_hom_ringI3:
    73   fixes R (structure) and S (structure)
    74   assumes "abelian_group_hom R S h" "ring R" "ring S" 
    75   assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    76       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    77   shows "ring_hom_ring R S h"
    78 proof -
    79   interpret abelian_group_hom R S h by fact
    80   interpret R: ring R by fact
    81   interpret S: ring S by fact
    82   show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    83     apply (insert group_hom.homh[OF a_group_hom])
    84     apply (unfold hom_def ring_hom_def, simp)
    85     apply safe
    86     apply (erule (1) compatible_mult)
    87     apply (rule compatible_one)
    88     done
    89 qed
    90 
    91 lemma ring_hom_cringI:
    92   assumes "ring_hom_ring R S h" "cring R" "cring S"
    93   shows "ring_hom_cring R S h"
    94 proof -
    95   interpret ring_hom_ring R S h by fact
    96   interpret R: cring R by fact
    97   interpret S: cring S by fact
    98   show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    99     (rule R.is_cring, rule S.is_cring, rule homh)
   100 qed
   101 
   102 
   103 subsection \<open>The Kernel of a Ring Homomorphism\<close>
   104 
   105 \<comment>"the kernel of a ring homomorphism is an ideal"
   106 lemma (in ring_hom_ring) kernel_is_ideal:
   107   shows "ideal (a_kernel R S h) R"
   108 apply (rule idealI)
   109    apply (rule R.is_ring)
   110   apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
   111  apply (unfold a_kernel_def', simp+)
   112 done
   113 
   114 text \<open>Elements of the kernel are mapped to zero\<close>
   115 lemma (in abelian_group_hom) kernel_zero [simp]:
   116   "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
   117 by (simp add: a_kernel_defs)
   118 
   119 
   120 subsection \<open>Cosets\<close>
   121 
   122 text \<open>Cosets of the kernel correspond to the elements of the image of the homomorphism\<close>
   123 lemma (in ring_hom_ring) rcos_imp_homeq:
   124   assumes acarr: "a \<in> carrier R"
   125       and xrcos: "x \<in> a_kernel R S h +> a"
   126   shows "h x = h a"
   127 proof -
   128   interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
   129 
   130   from xrcos
   131       have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
   132   from this obtain i
   133       where iker: "i \<in> a_kernel R S h"
   134         and x: "x = i \<oplus> a"
   135       by fast+
   136   note carr = acarr iker[THEN a_Hcarr]
   137 
   138   from x
   139       have "h x = h (i \<oplus> a)" by simp
   140   also from carr
   141       have "\<dots> = h i \<oplus>\<^bsub>S\<^esub> h a" by simp
   142   also from iker
   143       have "\<dots> = \<zero>\<^bsub>S\<^esub> \<oplus>\<^bsub>S\<^esub> h a" by simp
   144   also from carr
   145       have "\<dots> = h a" by simp
   146   finally
   147       show "h x = h a" .
   148 qed
   149 
   150 lemma (in ring_hom_ring) homeq_imp_rcos:
   151   assumes acarr: "a \<in> carrier R"
   152       and xcarr: "x \<in> carrier R"
   153       and hx: "h x = h a"
   154   shows "x \<in> a_kernel R S h +> a"
   155 proof -
   156   interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
   157  
   158   note carr = acarr xcarr
   159   note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
   160 
   161   from hx and hcarr
   162       have a: "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = \<zero>\<^bsub>S\<^esub>" by algebra
   163   from carr
   164       have "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = h (x \<oplus> \<ominus>a)" by simp
   165   from a and this
   166       have b: "h (x \<oplus> \<ominus>a) = \<zero>\<^bsub>S\<^esub>" by simp
   167 
   168   from carr have "x \<oplus> \<ominus>a \<in> carrier R" by simp
   169   from this and b
   170       have "x \<oplus> \<ominus>a \<in> a_kernel R S h" 
   171       unfolding a_kernel_def'
   172       by fast
   173 
   174   from this and carr
   175       show "x \<in> a_kernel R S h +> a" by (simp add: a_rcos_module_rev)
   176 qed
   177 
   178 corollary (in ring_hom_ring) rcos_eq_homeq:
   179   assumes acarr: "a \<in> carrier R"
   180   shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
   181 apply rule defer 1
   182 apply clarsimp defer 1
   183 proof
   184   interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
   185 
   186   fix x
   187   assume xrcos: "x \<in> a_kernel R S h +> a"
   188   from acarr and this
   189       have xcarr: "x \<in> carrier R"
   190       by (rule a_elemrcos_carrier)
   191 
   192   from xrcos
   193       have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
   194   from xcarr and this
   195       show "x \<in> {x \<in> carrier R. h x = h a}" by fast
   196 next
   197   interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
   198 
   199   fix x
   200   assume xcarr: "x \<in> carrier R"
   201      and hx: "h x = h a"
   202   from acarr xcarr hx
   203       show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
   204 qed
   205 
   206 end