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