src/HOL/Algebra/RingHom.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21502 7f3ea2b3bab6
child 23350 50c5b0912a0c
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (*
     2   Title:     HOL/Algebra/RingHom.thy
     3   Id:        $Id$
     4   Author:    Stephan Hohe, TU Muenchen
     5 *)
     6 
     7 theory RingHom
     8 imports Ideal
     9 begin
    10 
    11 
    12 section {* Homomorphisms of Non-Commutative Rings *}
    13 
    14 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
    15 locale ring_hom_ring = ring R + ring S + var 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 interpretation ring_hom_cring \<subseteq> ring_hom_ring
    21   by (unfold_locales, rule homh)
    22 
    23 interpretation ring_hom_ring \<subseteq> 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   includes struct R + struct S
    36   shows "ring_hom_ring R S h"
    37 by -
    38 
    39 lemma ring_hom_ringI:
    40   includes 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 apply unfold_locales
    48 apply (unfold ring_hom_def, safe)
    49    apply (simp add: hom_closed Pi_def, assumption+)
    50 done
    51 
    52 lemma ring_hom_ringI2:
    53   includes ring R + ring S
    54   assumes "h \<in> ring_hom R S"
    55   shows "ring_hom_ring R S h"
    56 by (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    57 
    58 lemma ring_hom_ringI3:
    59   includes abelian_group_hom R S + ring R + ring S 
    60   assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    61       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    62   shows "ring_hom_ring R S h"
    63 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+)
    64 apply (insert group_hom.homh[OF a_group_hom])
    65 apply (unfold hom_def ring_hom_def, simp)
    66 apply (safe, assumption+)
    67 done
    68 
    69 lemma ring_hom_cringI:
    70   includes ring_hom_ring R S h + cring R + cring S
    71   shows "ring_hom_cring R S h"
    72 by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro, assumption+, rule homh)
    73 
    74 
    75 subsection {* The kernel of a ring homomorphism *}
    76 
    77 --"the kernel of a ring homomorphism is an ideal"
    78 lemma (in ring_hom_ring) kernel_is_ideal:
    79   shows "ideal (a_kernel R S h) R"
    80 apply (rule idealI)
    81    apply (rule R.is_ring)
    82   apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
    83  apply (unfold a_kernel_def', simp+)
    84 done
    85 
    86 text {* Elements of the kernel are mapped to zero *}
    87 lemma (in abelian_group_hom) kernel_zero [simp]:
    88   "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
    89 by (simp add: a_kernel_defs)
    90 
    91 
    92 subsection {* Cosets *}
    93 
    94 text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
    95 lemma (in ring_hom_ring) rcos_imp_homeq:
    96   assumes acarr: "a \<in> carrier R"
    97       and xrcos: "x \<in> a_kernel R S h +> a"
    98   shows "h x = h a"
    99 proof -
   100   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   101 
   102   from xrcos
   103       have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
   104   from this obtain i
   105       where iker: "i \<in> a_kernel R S h"
   106         and x: "x = i \<oplus> a"
   107       by fast+
   108   note carr = acarr iker[THEN a_Hcarr]
   109 
   110   from x
   111       have "h x = h (i \<oplus> a)" by simp
   112   also from carr
   113       have "\<dots> = h i \<oplus>\<^bsub>S\<^esub> h a" by simp
   114   also from iker
   115       have "\<dots> = \<zero>\<^bsub>S\<^esub> \<oplus>\<^bsub>S\<^esub> h a" by simp
   116   also from carr
   117       have "\<dots> = h a" by simp
   118   finally
   119       show "h x = h a" .
   120 qed
   121 
   122 lemma (in ring_hom_ring) homeq_imp_rcos:
   123   assumes acarr: "a \<in> carrier R"
   124       and xcarr: "x \<in> carrier R"
   125       and hx: "h x = h a"
   126   shows "x \<in> a_kernel R S h +> a"
   127 proof -
   128   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   129  
   130   note carr = acarr xcarr
   131   note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
   132 
   133   from hx and hcarr
   134       have a: "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = \<zero>\<^bsub>S\<^esub>" by algebra
   135   from carr
   136       have "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = h (x \<oplus> \<ominus>a)" by simp
   137   from a and this
   138       have b: "h (x \<oplus> \<ominus>a) = \<zero>\<^bsub>S\<^esub>" by simp
   139 
   140   from carr have "x \<oplus> \<ominus>a \<in> carrier R" by simp
   141   from this and b
   142       have "x \<oplus> \<ominus>a \<in> a_kernel R S h" 
   143       unfolding a_kernel_def'
   144       by fast
   145 
   146   from this and carr
   147       show "x \<in> a_kernel R S h +> a" by (simp add: a_rcos_module_rev)
   148 qed
   149 
   150 corollary (in ring_hom_ring) rcos_eq_homeq:
   151   assumes acarr: "a \<in> carrier R"
   152   shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
   153 apply rule defer 1
   154 apply clarsimp defer 1
   155 proof
   156   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   157 
   158   fix x
   159   assume xrcos: "x \<in> a_kernel R S h +> a"
   160   from acarr and this
   161       have xcarr: "x \<in> carrier R"
   162       by (rule a_elemrcos_carrier)
   163 
   164   from xrcos
   165       have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
   166   from xcarr and this
   167       show "x \<in> {x \<in> carrier R. h x = h a}" by fast
   168 next
   169   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   170 
   171   fix x
   172   assume xcarr: "x \<in> carrier R"
   173      and hx: "h x = h a"
   174   from acarr xcarr hx
   175       show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
   176 qed
   177 
   178 end