author  wenzelm 
Fri, 02 Sep 2011 18:17:45 +0200  
changeset 44655  fe0365331566 
parent 35849  b5522b51cb1e 
child 61169  4de9ff3ea29a 
permissions  rwrr 
35849  1 
(* Title: HOL/Algebra/RingHom.thy 
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 NonCommutative Rings *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

10 

21502  11 
text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *} 
29240  12 
locale ring_hom_ring = R: ring R + S: ring S 
13 
for R (structure) and S (structure) + 

29237  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  19 
sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring 
44655  20 
by default (rule homh) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

21 

29246  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  34 
"ring_hom_ring R S h" 
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  38 
fixes R (structure) and S (structure) 
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  46 
proof  
29237  47 
interpret ring R by fact 
48 
interpret ring S by fact 

27611  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  51 
apply (simp add: hom_closed Pi_def) 
52 
apply (erule (1) compatible_mult) 

53 
apply (erule (1) compatible_add) 

54 
apply (rule compatible_one) 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

55 
done 
27611  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  59 
assumes "ring R" "ring S" 
23350  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  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  65 
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro) 
66 
apply (rule R.is_ring) 

67 
apply (rule S.is_ring) 

68 
apply (rule h) 

69 
done 

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  73 
fixes R (structure) and S (structure) 
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  78 
proof  
29237  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  82 
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring) 
83 
apply (insert group_hom.homh[OF a_group_hom]) 

84 
apply (unfold hom_def ring_hom_def, simp) 

85 
apply safe 

86 
apply (erule (1) compatible_mult) 

87 
apply (rule compatible_one) 

88 
done 

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  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  94 
proof  
29237  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  98 
show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro) 
23463  99 
(rule R.is_cring, rule S.is_cring, rule homh) 
27611  100 
qed 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

101 

35849  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  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  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  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  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 