author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 30729  461ee3e49ad3 
child 35849  b5522b51cb1e 
permissions  rwrr 
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 NonCommutative Rings *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

11 

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

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

22 

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

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

54 
apply (erule (1) compatible_add) 

55 
apply (rule compatible_one) 

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

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

68 
apply (rule S.is_ring) 

69 
apply (rule h) 

70 
done 

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

85 
apply (unfold hom_def ring_hom_def, simp) 

86 
apply safe 

87 
apply (erule (1) compatible_mult) 

88 
apply (rule compatible_one) 

89 
done 

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  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  95 
proof  
29237  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  99 
show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro) 
23463  100 
(rule R.is_cring, rule S.is_cring, rule homh) 
27611  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  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 