src/HOL/Algebra/RingHom.thy
 author wenzelm Mon Mar 16 18:24:30 2009 +0100 (2009-03-16) changeset 30549 d2d7874648bd parent 29246 3593802c9cf1 child 30729 461ee3e49ad3 permissions -rw-r--r--
simplified method setup;
```     1 (*
```
```     2   Title:     HOL/Algebra/RingHom.thy
```
```     3   Author:    Stephan Hohe, TU Muenchen
```
```     4 *)
```
```     5
```
```     6 theory RingHom
```
```     7 imports Ideal
```
```     8 begin
```
```     9
```
```    10 section {* Homomorphisms of Non-Commutative Rings *}
```
```    11
```
```    12 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
```
```    13 locale ring_hom_ring = R: ring R + S: ring S
```
```    14     for R (structure) and S (structure) +
```
```    15   fixes h
```
```    16   assumes homh: "h \<in> ring_hom R S"
```
```    17   notes hom_mult [simp] = ring_hom_mult [OF homh]
```
```    18     and hom_one [simp] = ring_hom_one [OF homh]
```
```    19
```
```    20 sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
```
```    21   proof qed (rule homh)
```
```    22
```
```    23 sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
```
```    24 apply (rule abelian_group_homI)
```
```    25   apply (rule R.is_abelian_group)
```
```    26  apply (rule S.is_abelian_group)
```
```    27 apply (intro group_hom.intro group_hom_axioms.intro)
```
```    28   apply (rule R.a_group)
```
```    29  apply (rule S.a_group)
```
```    30 apply (insert homh, unfold hom_def ring_hom_def)
```
```    31 apply simp
```
```    32 done
```
```    33
```
```    34 lemma (in ring_hom_ring) is_ring_hom_ring:
```
```    35   "ring_hom_ring R S h"
```
```    36   by (rule ring_hom_ring_axioms)
```
```    37
```
```    38 lemma ring_hom_ringI:
```
```    39   fixes R (structure) and S (structure)
```
```    40   assumes "ring R" "ring S"
```
```    41   assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
```
```    42           hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
```
```    43       and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
```
```    44       and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
```
```    45       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
```
```    46   shows "ring_hom_ring R S h"
```
```    47 proof -
```
```    48   interpret ring R by fact
```
```    49   interpret ring S by fact
```
```    50   show ?thesis apply unfold_locales
```
```    51 apply (unfold ring_hom_def, safe)
```
```    52    apply (simp add: hom_closed Pi_def)
```
```    53   apply (erule (1) compatible_mult)
```
```    54  apply (erule (1) compatible_add)
```
```    55 apply (rule compatible_one)
```
```    56 done
```
```    57 qed
```
```    58
```
```    59 lemma ring_hom_ringI2:
```
```    60   assumes "ring R" "ring S"
```
```    61   assumes h: "h \<in> ring_hom R S"
```
```    62   shows "ring_hom_ring R S h"
```
```    63 proof -
```
```    64   interpret R!: ring R by fact
```
```    65   interpret S!: ring S by fact
```
```    66   show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
```
```    67     apply (rule R.is_ring)
```
```    68     apply (rule S.is_ring)
```
```    69     apply (rule h)
```
```    70     done
```
```    71 qed
```
```    72
```
```    73 lemma ring_hom_ringI3:
```
```    74   fixes R (structure) and S (structure)
```
```    75   assumes "abelian_group_hom R S h" "ring R" "ring S"
```
```    76   assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
```
```    77       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
```
```    78   shows "ring_hom_ring R S h"
```
```    79 proof -
```
```    80   interpret abelian_group_hom R S h by fact
```
```    81   interpret R!: ring R by fact
```
```    82   interpret S!: ring S by fact
```
```    83   show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
```
```    84     apply (insert group_hom.homh[OF a_group_hom])
```
```    85     apply (unfold hom_def ring_hom_def, simp)
```
```    86     apply safe
```
```    87     apply (erule (1) compatible_mult)
```
```    88     apply (rule compatible_one)
```
```    89     done
```
```    90 qed
```
```    91
```
```    92 lemma ring_hom_cringI:
```
```    93   assumes "ring_hom_ring R S h" "cring R" "cring S"
```
```    94   shows "ring_hom_cring R S h"
```
```    95 proof -
```
```    96   interpret ring_hom_ring R S h by fact
```
```    97   interpret R!: cring R by fact
```
```    98   interpret S!: cring S by fact
```
```    99   show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
```
```   100     (rule R.is_cring, rule S.is_cring, rule homh)
```
```   101 qed
```
```   102
```
```   103 subsection {* The Kernel of a Ring Homomorphism *}
```
```   104
```
```   105 --"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 {* Elements of the kernel are mapped to zero *}
```
```   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 {* Cosets *}
```
```   121
```
```   122 text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
```
```   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
```