src/HOL/Algebra/RingHom.thy
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (10 months ago)
changeset 68551 b680e74eb6f2
parent 67613 ce654b0e6d69
child 68664 bd0df72c16d5
permissions -rw-r--r--
More on Algebra by Paulo and Martin
wenzelm@35849
     1
(*  Title:      HOL/Algebra/RingHom.thy
wenzelm@35849
     2
    Author:     Stephan Hohe, TU Muenchen
ballarin@20318
     3
*)
ballarin@20318
     4
ballarin@20318
     5
theory RingHom
ballarin@20318
     6
imports Ideal
ballarin@20318
     7
begin
ballarin@20318
     8
wenzelm@61382
     9
section \<open>Homomorphisms of Non-Commutative Rings\<close>
ballarin@20318
    10
wenzelm@63167
    11
text \<open>Lifting existing lemmas in a \<open>ring_hom_ring\<close> locale\<close>
ballarin@61565
    12
locale ring_hom_ring = R?: ring R + S?: ring S
ballarin@29240
    13
    for R (structure) and S (structure) +
ballarin@29237
    14
  fixes h
ballarin@20318
    15
  assumes homh: "h \<in> ring_hom R S"
ballarin@20318
    16
  notes hom_mult [simp] = ring_hom_mult [OF homh]
ballarin@20318
    17
    and hom_one [simp] = ring_hom_one [OF homh]
ballarin@20318
    18
ballarin@29246
    19
sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
wenzelm@61169
    20
  by standard (rule homh)
ballarin@20318
    21
ballarin@61565
    22
sublocale ring_hom_ring \<subseteq> abelian_group?: abelian_group_hom R S
ballarin@20318
    23
apply (rule abelian_group_homI)
ballarin@20318
    24
  apply (rule R.is_abelian_group)
ballarin@20318
    25
 apply (rule S.is_abelian_group)
ballarin@20318
    26
apply (intro group_hom.intro group_hom_axioms.intro)
ballarin@20318
    27
  apply (rule R.a_group)
ballarin@20318
    28
 apply (rule S.a_group)
ballarin@20318
    29
apply (insert homh, unfold hom_def ring_hom_def)
ballarin@20318
    30
apply simp
ballarin@20318
    31
done
ballarin@20318
    32
ballarin@20318
    33
lemma (in ring_hom_ring) is_ring_hom_ring:
ballarin@27611
    34
  "ring_hom_ring R S h"
ballarin@27611
    35
  by (rule ring_hom_ring_axioms)
ballarin@20318
    36
ballarin@20318
    37
lemma ring_hom_ringI:
ballarin@27611
    38
  fixes R (structure) and S (structure)
ballarin@27611
    39
  assumes "ring R" "ring S"
ballarin@20318
    40
  assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
ballarin@20318
    41
          hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
wenzelm@67613
    42
      and compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
wenzelm@67613
    43
      and compatible_add: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
ballarin@20318
    44
      and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
ballarin@20318
    45
  shows "ring_hom_ring R S h"
ballarin@27611
    46
proof -
ballarin@29237
    47
  interpret ring R by fact
ballarin@29237
    48
  interpret ring S by fact
ballarin@27611
    49
  show ?thesis apply unfold_locales
ballarin@20318
    50
apply (unfold ring_hom_def, safe)
wenzelm@23463
    51
   apply (simp add: hom_closed Pi_def)
wenzelm@23463
    52
  apply (erule (1) compatible_mult)
wenzelm@23463
    53
 apply (erule (1) compatible_add)
wenzelm@23463
    54
apply (rule compatible_one)
ballarin@20318
    55
done
ballarin@27611
    56
qed
ballarin@20318
    57
ballarin@20318
    58
lemma ring_hom_ringI2:
ballarin@27611
    59
  assumes "ring R" "ring S"
wenzelm@23350
    60
  assumes h: "h \<in> ring_hom R S"
ballarin@20318
    61
  shows "ring_hom_ring R S h"
ballarin@27611
    62
proof -
wenzelm@30729
    63
  interpret R: ring R by fact
wenzelm@30729
    64
  interpret S: ring S by fact
ballarin@27611
    65
  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
ballarin@27611
    66
    apply (rule R.is_ring)
ballarin@27611
    67
    apply (rule S.is_ring)
ballarin@27611
    68
    apply (rule h)
ballarin@27611
    69
    done
ballarin@27611
    70
qed
ballarin@20318
    71
ballarin@20318
    72
lemma ring_hom_ringI3:
ballarin@27611
    73
  fixes R (structure) and S (structure)
ballarin@27611
    74
  assumes "abelian_group_hom R S h" "ring R" "ring S" 
wenzelm@67613
    75
  assumes compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
ballarin@20318
    76
      and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
ballarin@20318
    77
  shows "ring_hom_ring R S h"
ballarin@27611
    78
proof -
ballarin@29237
    79
  interpret abelian_group_hom R S h by fact
wenzelm@30729
    80
  interpret R: ring R by fact
wenzelm@30729
    81
  interpret S: ring S by fact
ballarin@27611
    82
  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
ballarin@27611
    83
    apply (insert group_hom.homh[OF a_group_hom])
ballarin@27611
    84
    apply (unfold hom_def ring_hom_def, simp)
ballarin@27611
    85
    apply safe
ballarin@27611
    86
    apply (erule (1) compatible_mult)
ballarin@27611
    87
    apply (rule compatible_one)
ballarin@27611
    88
    done
ballarin@27611
    89
qed
ballarin@20318
    90
ballarin@20318
    91
lemma ring_hom_cringI:
ballarin@27611
    92
  assumes "ring_hom_ring R S h" "cring R" "cring S"
ballarin@20318
    93
  shows "ring_hom_cring R S h"
ballarin@27611
    94
proof -
ballarin@29237
    95
  interpret ring_hom_ring R S h by fact
wenzelm@30729
    96
  interpret R: cring R by fact
wenzelm@30729
    97
  interpret S: cring S by fact
ballarin@27611
    98
  show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
wenzelm@23463
    99
    (rule R.is_cring, rule S.is_cring, rule homh)
ballarin@27611
   100
qed
ballarin@20318
   101
wenzelm@35849
   102
wenzelm@61382
   103
subsection \<open>The Kernel of a Ring Homomorphism\<close>
ballarin@20318
   104
wenzelm@67443
   105
\<comment> \<open>the kernel of a ring homomorphism is an ideal\<close>
ballarin@20318
   106
lemma (in ring_hom_ring) kernel_is_ideal:
ballarin@20318
   107
  shows "ideal (a_kernel R S h) R"
ballarin@20318
   108
apply (rule idealI)
ballarin@20318
   109
   apply (rule R.is_ring)
ballarin@20318
   110
  apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
ballarin@20318
   111
 apply (unfold a_kernel_def', simp+)
ballarin@20318
   112
done
ballarin@20318
   113
wenzelm@61382
   114
text \<open>Elements of the kernel are mapped to zero\<close>
ballarin@20318
   115
lemma (in abelian_group_hom) kernel_zero [simp]:
ballarin@20318
   116
  "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
ballarin@20318
   117
by (simp add: a_kernel_defs)
ballarin@20318
   118
ballarin@20318
   119
wenzelm@61382
   120
subsection \<open>Cosets\<close>
ballarin@20318
   121
wenzelm@61382
   122
text \<open>Cosets of the kernel correspond to the elements of the image of the homomorphism\<close>
ballarin@20318
   123
lemma (in ring_hom_ring) rcos_imp_homeq:
ballarin@20318
   124
  assumes acarr: "a \<in> carrier R"
ballarin@20318
   125
      and xrcos: "x \<in> a_kernel R S h +> a"
ballarin@20318
   126
  shows "h x = h a"
ballarin@20318
   127
proof -
ballarin@29237
   128
  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
ballarin@20318
   129
ballarin@20318
   130
  from xrcos
ballarin@20318
   131
      have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
ballarin@20318
   132
  from this obtain i
ballarin@20318
   133
      where iker: "i \<in> a_kernel R S h"
ballarin@20318
   134
        and x: "x = i \<oplus> a"
ballarin@20318
   135
      by fast+
ballarin@20318
   136
  note carr = acarr iker[THEN a_Hcarr]
ballarin@20318
   137
ballarin@20318
   138
  from x
ballarin@20318
   139
      have "h x = h (i \<oplus> a)" by simp
ballarin@20318
   140
  also from carr
ballarin@20318
   141
      have "\<dots> = h i \<oplus>\<^bsub>S\<^esub> h a" by simp
ballarin@20318
   142
  also from iker
ballarin@20318
   143
      have "\<dots> = \<zero>\<^bsub>S\<^esub> \<oplus>\<^bsub>S\<^esub> h a" by simp
ballarin@20318
   144
  also from carr
ballarin@20318
   145
      have "\<dots> = h a" by simp
ballarin@20318
   146
  finally
ballarin@20318
   147
      show "h x = h a" .
ballarin@20318
   148
qed
ballarin@20318
   149
ballarin@20318
   150
lemma (in ring_hom_ring) homeq_imp_rcos:
ballarin@20318
   151
  assumes acarr: "a \<in> carrier R"
ballarin@20318
   152
      and xcarr: "x \<in> carrier R"
ballarin@20318
   153
      and hx: "h x = h a"
ballarin@20318
   154
  shows "x \<in> a_kernel R S h +> a"
ballarin@20318
   155
proof -
ballarin@29237
   156
  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
ballarin@20318
   157
 
ballarin@20318
   158
  note carr = acarr xcarr
ballarin@20318
   159
  note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
ballarin@20318
   160
ballarin@20318
   161
  from hx and hcarr
ballarin@20318
   162
      have a: "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = \<zero>\<^bsub>S\<^esub>" by algebra
ballarin@20318
   163
  from carr
ballarin@20318
   164
      have "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = h (x \<oplus> \<ominus>a)" by simp
ballarin@20318
   165
  from a and this
ballarin@20318
   166
      have b: "h (x \<oplus> \<ominus>a) = \<zero>\<^bsub>S\<^esub>" by simp
ballarin@20318
   167
ballarin@20318
   168
  from carr have "x \<oplus> \<ominus>a \<in> carrier R" by simp
ballarin@20318
   169
  from this and b
ballarin@20318
   170
      have "x \<oplus> \<ominus>a \<in> a_kernel R S h" 
ballarin@20318
   171
      unfolding a_kernel_def'
ballarin@20318
   172
      by fast
ballarin@20318
   173
ballarin@20318
   174
  from this and carr
ballarin@20318
   175
      show "x \<in> a_kernel R S h +> a" by (simp add: a_rcos_module_rev)
ballarin@20318
   176
qed
ballarin@20318
   177
ballarin@20318
   178
corollary (in ring_hom_ring) rcos_eq_homeq:
ballarin@20318
   179
  assumes acarr: "a \<in> carrier R"
ballarin@20318
   180
  shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
ballarin@20318
   181
apply rule defer 1
ballarin@20318
   182
apply clarsimp defer 1
ballarin@20318
   183
proof
ballarin@29237
   184
  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
ballarin@20318
   185
ballarin@20318
   186
  fix x
ballarin@20318
   187
  assume xrcos: "x \<in> a_kernel R S h +> a"
ballarin@20318
   188
  from acarr and this
ballarin@20318
   189
      have xcarr: "x \<in> carrier R"
ballarin@20318
   190
      by (rule a_elemrcos_carrier)
ballarin@20318
   191
ballarin@20318
   192
  from xrcos
ballarin@20318
   193
      have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
ballarin@20318
   194
  from xcarr and this
ballarin@20318
   195
      show "x \<in> {x \<in> carrier R. h x = h a}" by fast
ballarin@20318
   196
next
ballarin@29237
   197
  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
ballarin@20318
   198
ballarin@20318
   199
  fix x
ballarin@20318
   200
  assume xcarr: "x \<in> carrier R"
ballarin@20318
   201
     and hx: "h x = h a"
ballarin@20318
   202
  from acarr xcarr hx
ballarin@20318
   203
      show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
ballarin@20318
   204
qed
ballarin@20318
   205
lp15@68551
   206
(*contributed by Paulo Emílio de Vilhena*)
lp15@68551
   207
lemma (in ring_hom_ring) inj_on_domain:
lp15@68551
   208
  assumes "inj_on h (carrier R)"
lp15@68551
   209
  shows "domain S \<Longrightarrow> domain R"
lp15@68551
   210
proof -
lp15@68551
   211
  assume A: "domain S" show "domain R"
lp15@68551
   212
  proof
lp15@68551
   213
    have "h \<one> = \<one>\<^bsub>S\<^esub> \<and> h \<zero> = \<zero>\<^bsub>S\<^esub>" by simp
lp15@68551
   214
    hence "h \<one> \<noteq> h \<zero>"
lp15@68551
   215
      using domain.one_not_zero[OF A] by simp
lp15@68551
   216
    thus "\<one> \<noteq> \<zero>"
lp15@68551
   217
      using assms unfolding inj_on_def by fastforce 
lp15@68551
   218
  next
lp15@68551
   219
    fix a b
lp15@68551
   220
    assume a: "a \<in> carrier R"
lp15@68551
   221
       and b: "b \<in> carrier R"
lp15@68551
   222
    have "h (a \<otimes> b) = (h a) \<otimes>\<^bsub>S\<^esub> (h b)" by (simp add: a b)
lp15@68551
   223
    also have " ... = (h b) \<otimes>\<^bsub>S\<^esub> (h a)" using a b A cringE(1)[of S]
lp15@68551
   224
      by (simp add: cring.cring_simprules(14) domain_def)
lp15@68551
   225
    also have " ... = h (b \<otimes> a)" by (simp add: a b)
lp15@68551
   226
    finally have "h (a \<otimes> b) = h (b \<otimes> a)" .
lp15@68551
   227
    thus "a \<otimes> b = b \<otimes> a"
lp15@68551
   228
      using assms a b unfolding inj_on_def by simp 
lp15@68551
   229
    
lp15@68551
   230
    assume  ab: "a \<otimes> b = \<zero>"
lp15@68551
   231
    hence "h (a \<otimes> b) = \<zero>\<^bsub>S\<^esub>" by simp
lp15@68551
   232
    hence "(h a) \<otimes>\<^bsub>S\<^esub> (h b) = \<zero>\<^bsub>S\<^esub>" using a b by simp
lp15@68551
   233
    hence "h a =  \<zero>\<^bsub>S\<^esub> \<or> h b =  \<zero>\<^bsub>S\<^esub>" using a b domain.integral[OF A] by simp
lp15@68551
   234
    thus "a = \<zero> \<or> b = \<zero>"
lp15@68551
   235
      using a b assms unfolding inj_on_def by force
lp15@68551
   236
  qed
lp15@68551
   237
qed
lp15@68551
   238
ballarin@20318
   239
end