src/HOL/Algebra/RingHom.thy
author wenzelm
Fri, 02 Sep 2011 18:17:45 +0200
changeset 44655 fe0365331566
parent 35849 b5522b51cb1e
child 61169 4de9ff3ea29a
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35849
b5522b51cb1e standard headers;
wenzelm
parents: 30729
diff changeset
     1
(*  Title:      HOL/Algebra/RingHom.thy
b5522b51cb1e standard headers;
wenzelm
parents: 30729
diff changeset
     2
    Author:     Stephan Hohe, TU Muenchen
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     3
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     4
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     5
theory RingHom
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     6
imports Ideal
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     7
begin
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     8
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     9
section {* Homomorphisms of Non-Commutative Rings *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    10
21502
7f3ea2b3bab6 prefer antiquotations over LaTeX macros;
wenzelm
parents: 20318
diff changeset
    11
text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
29240
bb81c3709fb6 More porting to new locales.
ballarin
parents: 29237
diff changeset
    12
locale ring_hom_ring = R: ring R + S: ring S
bb81c3709fb6 More porting to new locales.
ballarin
parents: 29237
diff changeset
    13
    for R (structure) and S (structure) +
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    14
  fixes h
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    15
  assumes homh: "h \<in> ring_hom R S"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    16
  notes hom_mult [simp] = ring_hom_mult [OF homh]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    17
    and hom_one [simp] = ring_hom_one [OF homh]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    18
29246
3593802c9cf1 More porting to new locales.
ballarin
parents: 29240
diff changeset
    19
sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
44655
fe0365331566 tuned proofs;
wenzelm
parents: 35849
diff changeset
    20
  by default (rule homh)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    21
29246
3593802c9cf1 More porting to new locales.
ballarin
parents: 29240
diff changeset
    22
sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    23
apply (rule abelian_group_homI)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    24
  apply (rule R.is_abelian_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    25
 apply (rule S.is_abelian_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    26
apply (intro group_hom.intro group_hom_axioms.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    27
  apply (rule R.a_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    28
 apply (rule S.a_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    29
apply (insert homh, unfold hom_def ring_hom_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    30
apply simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    31
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    32
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    33
lemma (in ring_hom_ring) is_ring_hom_ring:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    34
  "ring_hom_ring R S h"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    35
  by (rule ring_hom_ring_axioms)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    36
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    37
lemma ring_hom_ringI:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    38
  fixes R (structure) and S (structure)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    39
  assumes "ring R" "ring S"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    40
  assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    41
          hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    42
      and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    43
      and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    44
      and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    45
  shows "ring_hom_ring R S h"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    46
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    47
  interpret ring R by fact
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    48
  interpret ring S by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    49
  show ?thesis apply unfold_locales
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    50
apply (unfold ring_hom_def, safe)
23463
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
    51
   apply (simp add: hom_closed Pi_def)
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
    52
  apply (erule (1) compatible_mult)
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
    53
 apply (erule (1) compatible_add)
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
    54
apply (rule compatible_one)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    55
done
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    56
qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    57
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    58
lemma ring_hom_ringI2:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    59
  assumes "ring R" "ring S"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 21502
diff changeset
    60
  assumes h: "h \<in> ring_hom R S"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    61
  shows "ring_hom_ring R S h"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    62
proof -
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    63
  interpret R: ring R by fact
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    64
  interpret S: ring S by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    65
  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    66
    apply (rule R.is_ring)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    67
    apply (rule S.is_ring)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    68
    apply (rule h)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    69
    done
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    70
qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    71
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    72
lemma ring_hom_ringI3:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    73
  fixes R (structure) and S (structure)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    74
  assumes "abelian_group_hom R S h" "ring R" "ring S" 
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    75
  assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    76
      and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    77
  shows "ring_hom_ring R S h"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    78
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    79
  interpret abelian_group_hom R S h by fact
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    80
  interpret R: ring R by fact
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    81
  interpret S: ring S by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    82
  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    83
    apply (insert group_hom.homh[OF a_group_hom])
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    84
    apply (unfold hom_def ring_hom_def, simp)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    85
    apply safe
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    86
    apply (erule (1) compatible_mult)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    87
    apply (rule compatible_one)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    88
    done
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    89
qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    90
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    91
lemma ring_hom_cringI:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    92
  assumes "ring_hom_ring R S h" "cring R" "cring S"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    93
  shows "ring_hom_cring R S h"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    94
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    95
  interpret ring_hom_ring R S h by fact
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    96
  interpret R: cring R by fact
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    97
  interpret S: cring S by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    98
  show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
23463
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
    99
    (rule R.is_cring, rule S.is_cring, rule homh)
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
   100
qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   101
35849
b5522b51cb1e standard headers;
wenzelm
parents: 30729
diff changeset
   102
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27611
diff changeset
   103
subsection {* The Kernel of a Ring Homomorphism *}
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   104
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   105
--"the kernel of a ring homomorphism is an ideal"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   106
lemma (in ring_hom_ring) kernel_is_ideal:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   107
  shows "ideal (a_kernel R S h) R"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   108
apply (rule idealI)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   109
   apply (rule R.is_ring)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   110
  apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   111
 apply (unfold a_kernel_def', simp+)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   112
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   113
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   114
text {* Elements of the kernel are mapped to zero *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   115
lemma (in abelian_group_hom) kernel_zero [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   116
  "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   117
by (simp add: a_kernel_defs)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   118
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   119
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   120
subsection {* Cosets *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   121
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   122
text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   123
lemma (in ring_hom_ring) rcos_imp_homeq:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   124
  assumes acarr: "a \<in> carrier R"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   125
      and xrcos: "x \<in> a_kernel R S h +> a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   126
  shows "h x = h a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   127
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
   128
  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   129
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   130
  from xrcos
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   131
      have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   132
  from this obtain i
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   133
      where iker: "i \<in> a_kernel R S h"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   134
        and x: "x = i \<oplus> a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   135
      by fast+
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   136
  note carr = acarr iker[THEN a_Hcarr]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   137
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   138
  from x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   139
      have "h x = h (i \<oplus> a)" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   140
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   141
      have "\<dots> = h i \<oplus>\<^bsub>S\<^esub> h a" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   142
  also from iker
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   143
      have "\<dots> = \<zero>\<^bsub>S\<^esub> \<oplus>\<^bsub>S\<^esub> h a" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   144
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   145
      have "\<dots> = h a" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   146
  finally
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   147
      show "h x = h a" .
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   148
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   149
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   150
lemma (in ring_hom_ring) homeq_imp_rcos:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   151
  assumes acarr: "a \<in> carrier R"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   152
      and xcarr: "x \<in> carrier R"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   153
      and hx: "h x = h a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   154
  shows "x \<in> a_kernel R S h +> a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   155
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
   156
  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   157
 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   158
  note carr = acarr xcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   159
  note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   160
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   161
  from hx and hcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   162
      have a: "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = \<zero>\<^bsub>S\<^esub>" by algebra
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   163
  from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   164
      have "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = h (x \<oplus> \<ominus>a)" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   165
  from a and this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   166
      have b: "h (x \<oplus> \<ominus>a) = \<zero>\<^bsub>S\<^esub>" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   167
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   168
  from carr have "x \<oplus> \<ominus>a \<in> carrier R" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   169
  from this and b
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   170
      have "x \<oplus> \<ominus>a \<in> a_kernel R S h" 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   171
      unfolding a_kernel_def'
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   172
      by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   173
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   174
  from this and carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   175
      show "x \<in> a_kernel R S h +> a" by (simp add: a_rcos_module_rev)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   176
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   177
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   178
corollary (in ring_hom_ring) rcos_eq_homeq:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   179
  assumes acarr: "a \<in> carrier R"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   180
  shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   181
apply rule defer 1
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   182
apply clarsimp defer 1
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   183
proof
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
   184
  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   185
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   186
  fix x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   187
  assume xrcos: "x \<in> a_kernel R S h +> a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   188
  from acarr and this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   189
      have xcarr: "x \<in> carrier R"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   190
      by (rule a_elemrcos_carrier)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   191
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   192
  from xrcos
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   193
      have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   194
  from xcarr and this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   195
      show "x \<in> {x \<in> carrier R. h x = h a}" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   196
next
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
   197
  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   198
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   199
  fix x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   200
  assume xcarr: "x \<in> carrier R"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   201
     and hx: "h x = h a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   202
  from acarr xcarr hx
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   203
      show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   204
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   205
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   206
end