src/HOL/Algebra/RingHom.thy
author nipkow
Fri, 13 Nov 2009 14:14:04 +0100
changeset 33657 a4179bf442d1
parent 30729 461ee3e49ad3
child 35849 b5522b51cb1e
permissions -rw-r--r--
renamed lemmas "anti_sym" -> "antisym"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     1
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     2
  Title:     HOL/Algebra/RingHom.thy
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     3
  Author:    Stephan Hohe, TU Muenchen
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
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     6
theory RingHom
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     7
imports Ideal
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     8
begin
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     9
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    10
section {* Homomorphisms of Non-Commutative Rings *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    11
21502
7f3ea2b3bab6 prefer antiquotations over LaTeX macros;
wenzelm
parents: 20318
diff changeset
    12
text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
29240
bb81c3709fb6 More porting to new locales.
ballarin
parents: 29237
diff changeset
    13
locale ring_hom_ring = R: ring R + S: ring S
bb81c3709fb6 More porting to new locales.
ballarin
parents: 29237
diff changeset
    14
    for R (structure) and S (structure) +
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    15
  fixes h
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    16
  assumes homh: "h \<in> ring_hom R S"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    17
  notes hom_mult [simp] = ring_hom_mult [OF homh]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    18
    and hom_one [simp] = ring_hom_one [OF homh]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    19
29246
3593802c9cf1 More porting to new locales.
ballarin
parents: 29240
diff changeset
    20
sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 27717
diff changeset
    21
  proof qed (rule homh)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    22
29246
3593802c9cf1 More porting to new locales.
ballarin
parents: 29240
diff changeset
    23
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
    24
apply (rule abelian_group_homI)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    25
  apply (rule R.is_abelian_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    26
 apply (rule S.is_abelian_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    27
apply (intro group_hom.intro group_hom_axioms.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    28
  apply (rule R.a_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    29
 apply (rule S.a_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    30
apply (insert homh, unfold hom_def ring_hom_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    31
apply simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    32
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    33
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    34
lemma (in ring_hom_ring) is_ring_hom_ring:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    35
  "ring_hom_ring R S h"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    36
  by (rule ring_hom_ring_axioms)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    37
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    38
lemma ring_hom_ringI:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    39
  fixes R (structure) and S (structure)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    40
  assumes "ring R" "ring S"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    41
  assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    42
          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
    43
      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
    44
      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
    45
      and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    46
  shows "ring_hom_ring R S h"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    47
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    48
  interpret ring R by fact
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    49
  interpret ring S by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    50
  show ?thesis apply unfold_locales
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    51
apply (unfold ring_hom_def, safe)
23463
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
    52
   apply (simp add: hom_closed Pi_def)
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
    53
  apply (erule (1) compatible_mult)
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
    54
 apply (erule (1) compatible_add)
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
    55
apply (rule compatible_one)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    56
done
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    57
qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    58
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    59
lemma ring_hom_ringI2:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    60
  assumes "ring R" "ring S"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 21502
diff changeset
    61
  assumes h: "h \<in> ring_hom R S"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    62
  shows "ring_hom_ring R S h"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    63
proof -
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    64
  interpret R: ring R by fact
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    65
  interpret S: ring S by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    66
  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
    67
    apply (rule R.is_ring)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    68
    apply (rule S.is_ring)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    69
    apply (rule h)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    70
    done
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    71
qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    72
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    73
lemma ring_hom_ringI3:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    74
  fixes R (structure) and S (structure)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    75
  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
    76
  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
    77
      and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    78
  shows "ring_hom_ring R S h"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    79
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    80
  interpret abelian_group_hom R S h by fact
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    81
  interpret R: ring R by fact
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    82
  interpret S: ring S by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    83
  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
    84
    apply (insert group_hom.homh[OF a_group_hom])
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    85
    apply (unfold hom_def ring_hom_def, simp)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    86
    apply safe
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    87
    apply (erule (1) compatible_mult)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    88
    apply (rule compatible_one)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    89
    done
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    90
qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    91
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    92
lemma ring_hom_cringI:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    93
  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
    94
  shows "ring_hom_cring R S h"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    95
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    96
  interpret ring_hom_ring R S h by fact
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    97
  interpret R: cring R by fact
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29246
diff changeset
    98
  interpret S: cring S by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
    99
  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
   100
    (rule R.is_cring, rule S.is_cring, rule homh)
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26204
diff changeset
   101
qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
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