src/HOL/Algebra/RingHom.thy
author wenzelm
Thu Jun 21 20:07:26 2007 +0200 (2007-06-21)
changeset 23464 bc2563c37b1a
parent 23463 9953ff53cc64
child 26204 da9778392d8c
permissions -rw-r--r--
tuned proofs -- avoid implicit prems;
     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 section {* Homomorphisms of Non-Commutative Rings *}
    12 
    13 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
    14 locale ring_hom_ring = ring R + ring S + var 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 interpretation ring_hom_cring \<subseteq> ring_hom_ring
    20   by (unfold_locales, rule homh)
    21 
    22 interpretation ring_hom_ring \<subseteq> 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   includes struct R + struct S
    35   shows "ring_hom_ring R S h"
    36 by fact
    37 
    38 lemma ring_hom_ringI:
    39   includes 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 apply unfold_locales
    47 apply (unfold ring_hom_def, safe)
    48    apply (simp add: hom_closed Pi_def)
    49   apply (erule (1) compatible_mult)
    50  apply (erule (1) compatible_add)
    51 apply (rule compatible_one)
    52 done
    53 
    54 lemma ring_hom_ringI2:
    55   includes ring R + ring S
    56   assumes h: "h \<in> ring_hom R S"
    57   shows "ring_hom_ring R S h"
    58 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    59 apply (rule R.is_ring)
    60 apply (rule S.is_ring)
    61 apply (rule h)
    62 done
    63 
    64 lemma ring_hom_ringI3:
    65   includes abelian_group_hom R S + ring R + ring S 
    66   assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    67       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    68   shows "ring_hom_ring R S h"
    69 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    70 apply (insert group_hom.homh[OF a_group_hom])
    71 apply (unfold hom_def ring_hom_def, simp)
    72 apply safe
    73 apply (erule (1) compatible_mult)
    74 apply (rule compatible_one)
    75 done
    76 
    77 lemma ring_hom_cringI:
    78   includes ring_hom_ring R S h + cring R + cring S
    79   shows "ring_hom_cring R S h"
    80   by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    81     (rule R.is_cring, rule S.is_cring, rule homh)
    82 
    83 
    84 subsection {* The kernel of a ring homomorphism *}
    85 
    86 --"the kernel of a ring homomorphism is an ideal"
    87 lemma (in ring_hom_ring) kernel_is_ideal:
    88   shows "ideal (a_kernel R S h) R"
    89 apply (rule idealI)
    90    apply (rule R.is_ring)
    91   apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
    92  apply (unfold a_kernel_def', simp+)
    93 done
    94 
    95 text {* Elements of the kernel are mapped to zero *}
    96 lemma (in abelian_group_hom) kernel_zero [simp]:
    97   "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
    98 by (simp add: a_kernel_defs)
    99 
   100 
   101 subsection {* Cosets *}
   102 
   103 text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
   104 lemma (in ring_hom_ring) rcos_imp_homeq:
   105   assumes acarr: "a \<in> carrier R"
   106       and xrcos: "x \<in> a_kernel R S h +> a"
   107   shows "h x = h a"
   108 proof -
   109   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   110 
   111   from xrcos
   112       have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
   113   from this obtain i
   114       where iker: "i \<in> a_kernel R S h"
   115         and x: "x = i \<oplus> a"
   116       by fast+
   117   note carr = acarr iker[THEN a_Hcarr]
   118 
   119   from x
   120       have "h x = h (i \<oplus> a)" by simp
   121   also from carr
   122       have "\<dots> = h i \<oplus>\<^bsub>S\<^esub> h a" by simp
   123   also from iker
   124       have "\<dots> = \<zero>\<^bsub>S\<^esub> \<oplus>\<^bsub>S\<^esub> h a" by simp
   125   also from carr
   126       have "\<dots> = h a" by simp
   127   finally
   128       show "h x = h a" .
   129 qed
   130 
   131 lemma (in ring_hom_ring) homeq_imp_rcos:
   132   assumes acarr: "a \<in> carrier R"
   133       and xcarr: "x \<in> carrier R"
   134       and hx: "h x = h a"
   135   shows "x \<in> a_kernel R S h +> a"
   136 proof -
   137   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   138  
   139   note carr = acarr xcarr
   140   note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
   141 
   142   from hx and hcarr
   143       have a: "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = \<zero>\<^bsub>S\<^esub>" by algebra
   144   from carr
   145       have "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = h (x \<oplus> \<ominus>a)" by simp
   146   from a and this
   147       have b: "h (x \<oplus> \<ominus>a) = \<zero>\<^bsub>S\<^esub>" by simp
   148 
   149   from carr have "x \<oplus> \<ominus>a \<in> carrier R" by simp
   150   from this and b
   151       have "x \<oplus> \<ominus>a \<in> a_kernel R S h" 
   152       unfolding a_kernel_def'
   153       by fast
   154 
   155   from this and carr
   156       show "x \<in> a_kernel R S h +> a" by (simp add: a_rcos_module_rev)
   157 qed
   158 
   159 corollary (in ring_hom_ring) rcos_eq_homeq:
   160   assumes acarr: "a \<in> carrier R"
   161   shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
   162 apply rule defer 1
   163 apply clarsimp defer 1
   164 proof
   165   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   166 
   167   fix x
   168   assume xrcos: "x \<in> a_kernel R S h +> a"
   169   from acarr and this
   170       have xcarr: "x \<in> carrier R"
   171       by (rule a_elemrcos_carrier)
   172 
   173   from xrcos
   174       have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
   175   from xcarr and this
   176       show "x \<in> {x \<in> carrier R. h x = h a}" by fast
   177 next
   178   interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   179 
   180   fix x
   181   assume xcarr: "x \<in> carrier R"
   182      and hx: "h x = h a"
   183   from acarr xcarr hx
   184       show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
   185 qed
   186 
   187 end