author  paulson <lp15@cam.ac.uk> 
Sat, 30 Jun 2018 15:44:04 +0100  
changeset 68551  b680e74eb6f2 
parent 67443  3abf6a722518 
child 68582  b9b9e2985878 
child 68583  654e73d05495 
permissions  rwrr 
35849  1 
(* Title: HOL/Algebra/QuotRing.thy 
2 
Author: Stephan Hohe 

68551
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

3 
Author: Paulo EmÃlio de Vilhena 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

4 

20318
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 

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

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

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

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

10 

61382  11 
section \<open>Quotient Rings\<close> 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27611
diff
changeset

12 

61382  13 
subsection \<open>Multiplication on Cosets\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

14 

45005  15 
definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set" 
23463  16 
("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80) 
35848
5443079512ea
slightly more uniform definitions  eliminated oldstyle metaequality;
wenzelm
parents:
35847
diff
changeset

17 
where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

18 

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

19 

61382  20 
text \<open>@{const "rcoset_mult"} fulfils the properties required by 
21 
congruences\<close> 

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

22 
lemma (in ideal) rcoset_mult_add: 
45005  23 
"x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> [mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)" 
24 
apply rule 

25 
apply (rule, simp add: rcoset_mult_def, clarsimp) 

26 
defer 1 

27 
apply (rule, simp add: rcoset_mult_def) 

28 
defer 1 

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

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

30 
fix z x' y' 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

31 
assume carr: "x \<in> carrier R" "y \<in> carrier R" 
45005  32 
and x'rcos: "x' \<in> I +> x" 
33 
and y'rcos: "y' \<in> I +> y" 

34 
and zrcos: "z \<in> I +> x' \<otimes> y'" 

35 

36 
from x'rcos have "\<exists>h\<in>I. x' = h \<oplus> x" 

37 
by (simp add: a_r_coset_def r_coset_def) 

38 
then obtain hx where hxI: "hx \<in> I" and x': "x' = hx \<oplus> x" 

39 
by fast+ 

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

40 

45005  41 
from y'rcos have "\<exists>h\<in>I. y' = h \<oplus> y" 
42 
by (simp add: a_r_coset_def r_coset_def) 

43 
then obtain hy where hyI: "hy \<in> I" and y': "y' = hy \<oplus> y" 

44 
by fast+ 

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

45 

45005  46 
from zrcos have "\<exists>h\<in>I. z = h \<oplus> (x' \<otimes> y')" 
47 
by (simp add: a_r_coset_def r_coset_def) 

48 
then obtain hz where hzI: "hz \<in> I" and z: "z = hz \<oplus> (x' \<otimes> y')" 

49 
by fast+ 

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

50 

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

51 
note carr = carr hxI[THEN a_Hcarr] hyI[THEN a_Hcarr] hzI[THEN a_Hcarr] 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

52 

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

53 
from z have "z = hz \<oplus> (x' \<otimes> y')" . 
45005  54 
also from x' y' have "\<dots> = hz \<oplus> ((hx \<oplus> x) \<otimes> (hy \<oplus> y))" by simp 
55 
also from carr have "\<dots> = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" by algebra 

56 
finally have z2: "z = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" . 

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

57 

45005  58 
from hxI hyI hzI carr have "hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy \<in> I" 
59 
by (simp add: I_l_closed I_r_closed) 

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

60 

45005  61 
with z2 have "\<exists>h\<in>I. z = h \<oplus> x \<otimes> y" by fast 
62 
then show "z \<in> I +> x \<otimes> y" by (simp add: a_r_coset_def r_coset_def) 

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

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

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

65 
assume xcarr: "x \<in> carrier R" 
45005  66 
and ycarr: "y \<in> carrier R" 
67 
and zrcos: "z \<in> I +> x \<otimes> y" 

68 
from xcarr have xself: "x \<in> I +> x" by (intro a_rcos_self) 

69 
from ycarr have yself: "y \<in> I +> y" by (intro a_rcos_self) 

70 
show "\<exists>a\<in>I +> x. \<exists>b\<in>I +> y. z \<in> I +> a \<otimes> b" 

71 
using xself and yself and zrcos by fast 

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

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

73 

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

74 

61382  75 
subsection \<open>Quotient Ring Definition\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

76 

45005  77 
definition FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring" 
78 
(infixl "Quot" 65) 

35848
5443079512ea
slightly more uniform definitions  eliminated oldstyle metaequality;
wenzelm
parents:
35847
diff
changeset

79 
where "FactRing R I = 
45005  80 
\<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I, 
81 
one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>" 

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

82 

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

83 

61382  84 
subsection \<open>Factorization over General Ideals\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

85 

61382  86 
text \<open>The quotient is a ring\<close> 
45005  87 
lemma (in ideal) quotient_is_ring: "ring (R Quot I)" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

88 
apply (rule ringI) 
67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

89 
\<comment> \<open>abelian group\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

90 
apply (rule comm_group_abelian_groupI) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

91 
apply (simp add: FactRing_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

92 
apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def']) 
67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

93 
\<comment> \<open>mult monoid\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

94 
apply (rule monoidI) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

95 
apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

96 
a_r_coset_def[symmetric]) 
67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

97 
\<comment> \<open>mult closed\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

98 
apply (clarify) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

99 
apply (simp add: rcoset_mult_add, fast) 
67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

100 
\<comment> \<open>mult \<open>one_closed\<close>\<close> 
45005  101 
apply force 
67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

102 
\<comment> \<open>mult assoc\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

104 
apply (simp add: rcoset_mult_add m_assoc) 
67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

105 
\<comment> \<open>mult one\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

106 
apply clarify 
45005  107 
apply (simp add: rcoset_mult_add) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

108 
apply clarify 
45005  109 
apply (simp add: rcoset_mult_add) 
67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

110 
\<comment> \<open>distr\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

112 
apply (simp add: rcoset_mult_add a_rcos_sum l_distr) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

114 
apply (simp add: rcoset_mult_add a_rcos_sum r_distr) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

116 

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

117 

61382  118 
text \<open>This is a ring homomorphism\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

119 

67399  120 
lemma (in ideal) rcos_ring_hom: "((+>) I) \<in> ring_hom R (R Quot I)" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

121 
apply (rule ring_hom_memI) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

122 
apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

123 
apply (simp add: FactRing_def rcoset_mult_add) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

124 
apply (simp add: FactRing_def a_rcos_sum) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

125 
apply (simp add: FactRing_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

127 

67399  128 
lemma (in ideal) rcos_ring_hom_ring: "ring_hom_ring R (R Quot I) ((+>) I)" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

129 
apply (rule ring_hom_ringI) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

130 
apply (rule is_ring, rule quotient_is_ring) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

131 
apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

132 
apply (simp add: FactRing_def rcoset_mult_add) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

133 
apply (simp add: FactRing_def a_rcos_sum) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

134 
apply (simp add: FactRing_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

136 

61382  137 
text \<open>The quotient of a cring is also commutative\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

138 
lemma (in ideal) quotient_is_cring: 
27611  139 
assumes "cring R" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

140 
shows "cring (R Quot I)" 
27611  141 
proof  
29237  142 
interpret cring R by fact 
45005  143 
show ?thesis 
144 
apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro) 

145 
apply (rule quotient_is_ring) 

146 
apply (rule ring.axioms[OF quotient_is_ring]) 

147 
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric]) 

148 
apply clarify 

149 
apply (simp add: rcoset_mult_add m_comm) 

150 
done 

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

152 

61382  153 
text \<open>Cosets as a ring homomorphism on crings\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

154 
lemma (in ideal) rcos_ring_hom_cring: 
27611  155 
assumes "cring R" 
67399  156 
shows "ring_hom_cring R (R Quot I) ((+>) I)" 
27611  157 
proof  
29237  158 
interpret cring R by fact 
45005  159 
show ?thesis 
160 
apply (rule ring_hom_cringI) 

161 
apply (rule rcos_ring_hom_ring) 

162 
apply (rule is_cring) 

163 
apply (rule quotient_is_cring) 

164 
apply (rule is_cring) 

165 
done 

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

167 

35849  168 

61382  169 
subsection \<open>Factorization over Prime Ideals\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

170 

61382  171 
text \<open>The quotient ring generated by a prime ideal is a domain\<close> 
45005  172 
lemma (in primeideal) quotient_is_domain: "domain (R Quot I)" 
173 
apply (rule domain.intro) 

174 
apply (rule quotient_is_cring, rule is_cring) 

175 
apply (rule domain_axioms.intro) 

176 
apply (simp add: FactRing_def) defer 1 

177 
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarify) 

178 
apply (simp add: rcoset_mult_add) defer 1 

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

179 
proof (rule ccontr, clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

180 
assume "I +> \<one> = I" 
45005  181 
then have "\<one> \<in> I" by (simp only: a_coset_join1 one_closed a_subgroup) 
182 
then have "carrier R \<subseteq> I" by (subst one_imp_carrier, simp, fast) 

183 
with a_subset have "I = carrier R" by fast 

184 
with I_notcarr show False by fast 

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

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

186 
fix x y 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

187 
assume carr: "x \<in> carrier R" "y \<in> carrier R" 
45005  188 
and a: "I +> x \<otimes> y = I" 
189 
and b: "I +> y \<noteq> I" 

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

190 

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

191 
have ynI: "y \<notin> I" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

192 
proof (rule ccontr, simp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

193 
assume "y \<in> I" 
45005  194 
then have "I +> y = I" by (rule a_rcos_const) 
195 
with b show False by simp 

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

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

197 

45005  198 
from carr have "x \<otimes> y \<in> I +> x \<otimes> y" by (simp add: a_rcos_self) 
199 
then have xyI: "x \<otimes> y \<in> I" by (simp add: a) 

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

200 

45005  201 
from xyI and carr have xI: "x \<in> I \<or> y \<in> I" by (simp add: I_prime) 
202 
with ynI have "x \<in> I" by fast 

203 
then show "I +> x = I" by (rule a_rcos_const) 

20318
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 

61382  206 
text \<open>Generating right cosets of a prime ideal is a homomorphism 
207 
on commutative rings\<close> 

67399  208 
lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) ((+>) I)" 
45005  209 
by (rule rcos_ring_hom_cring) (rule is_cring) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

210 

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

211 

61382  212 
subsection \<open>Factorization over Maximal Ideals\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

213 

61382  214 
text \<open>In a commutative ring, the quotient ring over a maximal ideal 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

215 
is a field. 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

216 
The proof follows ``W. Adkins, S. Weintraub: Algebra  
61382  217 
An Approach via Module Theory''\<close> 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

218 
lemma (in maximalideal) quotient_is_field: 
27611  219 
assumes "cring R" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

220 
shows "field (R Quot I)" 
27611  221 
proof  
29237  222 
interpret cring R by fact 
45005  223 
show ?thesis 
224 
apply (intro cring.cring_fieldI2) 

225 
apply (rule quotient_is_cring, rule is_cring) 

226 
defer 1 

227 
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp) 

228 
apply (simp add: rcoset_mult_add) defer 1 

229 
proof (rule ccontr, simp) 

67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

230 
\<comment> \<open>Quotient is not empty\<close> 
45005  231 
assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>" 
232 
then have II1: "I = I +> \<one>" by (simp add: FactRing_def) 

233 
from a_rcos_self[OF one_closed] have "\<one> \<in> I" 

234 
by (simp add: II1[symmetric]) 

235 
then have "I = carrier R" by (rule one_imp_carrier) 

236 
with I_notcarr show False by simp 

237 
next 

67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

238 
\<comment> \<open>Existence of Inverse\<close> 
45005  239 
fix a 
240 
assume IanI: "I +> a \<noteq> I" and acarr: "a \<in> carrier R" 

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

241 

67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

242 
\<comment> \<open>Helper ideal \<open>J\<close>\<close> 
63040  243 
define J :: "'a set" where "J = (carrier R #> a) <+> I" 
45005  244 
have idealJ: "ideal J R" 
245 
apply (unfold J_def, rule add_ideals) 

246 
apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr) 

247 
apply (rule is_ideal) 

248 
done 

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

249 

67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

250 
\<comment> \<open>Showing @{term "J"} not smaller than @{term "I"}\<close> 
45005  251 
have IinJ: "I \<subseteq> J" 
252 
proof (rule, simp add: J_def r_coset_def set_add_defs) 

253 
fix x 

254 
assume xI: "x \<in> I" 

255 
have Zcarr: "\<zero> \<in> carrier R" by fast 

256 
from xI[THEN a_Hcarr] acarr 

257 
have "x = \<zero> \<otimes> a \<oplus> x" by algebra 

258 
with Zcarr and xI show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast 

259 
qed 

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

260 

67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

261 
\<comment> \<open>Showing @{term "J \<noteq> I"}\<close> 
45005  262 
have anI: "a \<notin> I" 
263 
proof (rule ccontr, simp) 

264 
assume "a \<in> I" 

265 
then have "I +> a = I" by (rule a_rcos_const) 

266 
with IanI show False by simp 

267 
qed 

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

268 

45005  269 
have aJ: "a \<in> J" 
270 
proof (simp add: J_def r_coset_def set_add_defs) 

271 
from acarr 

272 
have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra 

273 
with one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup] 

274 
show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast 

275 
qed 

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

276 

45005  277 
from aJ and anI have JnI: "J \<noteq> I" by fast 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

278 

67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

279 
\<comment> \<open>Deducing @{term "J = carrier R"} because @{term "I"} is maximal\<close> 
45005  280 
from idealJ and IinJ have "J = I \<or> J = carrier R" 
281 
proof (rule I_maximal, unfold J_def) 

282 
have "carrier R #> a \<subseteq> carrier R" 

283 
using subset_refl acarr by (rule r_coset_subset_G) 

284 
then show "carrier R #> a <+> I \<subseteq> carrier R" 

285 
using a_subset by (rule set_add_closed) 

286 
qed 

287 

288 
with JnI have Jcarr: "J = carrier R" by simp 

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

289 

67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

290 
\<comment> \<open>Calculating an inverse for @{term "a"}\<close> 
45005  291 
from one_closed[folded Jcarr] 
292 
have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i" 

293 
by (simp add: J_def r_coset_def set_add_defs) 

294 
then obtain r i where rcarr: "r \<in> carrier R" 

295 
and iI: "i \<in> I" and one: "\<one> = r \<otimes> a \<oplus> i" by fast 

296 
from one and rcarr and acarr and iI[THEN a_Hcarr] 

297 
have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra 

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

298 

67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

299 
\<comment> \<open>Lifting to cosets\<close> 
45005  300 
from iI have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>" 
301 
by (intro a_rcosI, simp, intro a_subset, simp) 

302 
with rai1 have "a \<otimes> r \<in> I +> \<one>" by simp 

303 
then have "I +> \<one> = I +> a \<otimes> r" 

304 
by (rule a_repr_independence, simp) (rule a_subgroup) 

305 

306 
from rcarr and this[symmetric] 

307 
show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast 

308 
qed 

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

310 

68551
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

311 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

312 
lemma (in ring_hom_ring) trivial_hom_iff: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

313 
"(h ` (carrier R) = { \<zero>\<^bsub>S\<^esub> }) = (a_kernel R S h = carrier R)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

314 
using group_hom.trivial_hom_iff[OF a_group_hom] by (simp add: a_kernel_def) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

315 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

316 
lemma (in ring_hom_ring) trivial_ker_imp_inj: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

317 
assumes "a_kernel R S h = { \<zero> }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

318 
shows "inj_on h (carrier R)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

319 
using group_hom.trivial_ker_imp_inj[OF a_group_hom] assms a_kernel_def[of R S h] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

320 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

321 
lemma (in ring_hom_ring) non_trivial_field_hom_imp_inj: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

322 
assumes "field R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

323 
shows "h ` (carrier R) \<noteq> { \<zero>\<^bsub>S\<^esub> } \<Longrightarrow> inj_on h (carrier R)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

324 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

325 
assume "h ` (carrier R) \<noteq> { \<zero>\<^bsub>S\<^esub> }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

326 
hence "a_kernel R S h \<noteq> carrier R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

327 
using trivial_hom_iff by linarith 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

328 
hence "a_kernel R S h = { \<zero> }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

329 
using field.all_ideals[OF assms] kernel_is_ideal by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

330 
thus "inj_on h (carrier R)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

331 
using trivial_ker_imp_inj by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

332 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

333 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

334 
lemma (in ring_hom_ring) img_is_add_subgroup: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

335 
assumes "subgroup H (add_monoid R)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

336 
shows "subgroup (h ` H) (add_monoid S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

337 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

338 
have "group ((add_monoid R) \<lparr> carrier := H \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

339 
using assms R.add.subgroup_imp_group by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

340 
moreover have "H \<subseteq> carrier R" by (simp add: R.add.subgroupE(1) assms) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

341 
hence "h \<in> hom ((add_monoid R) \<lparr> carrier := H \<rparr>) (add_monoid S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

342 
unfolding hom_def by (auto simp add: subsetD) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

343 
ultimately have "subgroup (h ` carrier ((add_monoid R) \<lparr> carrier := H \<rparr>)) (add_monoid S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

344 
using group_hom.img_is_subgroup[of "(add_monoid R) \<lparr> carrier := H \<rparr>" "add_monoid S" h] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

345 
using a_group_hom group_hom_axioms.intro group_hom_def by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

346 
thus "subgroup (h ` H) (add_monoid S)" by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

347 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

348 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

349 
lemma (in ring) ring_ideal_imp_quot_ideal: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

350 
assumes "ideal I R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

351 
shows "ideal J R \<Longrightarrow> ideal ((+>) I ` J) (R Quot I)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

352 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

353 
assume A: "ideal J R" show "ideal (((+>) I) ` J) (R Quot I)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

354 
proof (rule idealI) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

355 
show "ring (R Quot I)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

356 
by (simp add: assms(1) ideal.quotient_is_ring) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

357 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

358 
have "subgroup J (add_monoid R)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

359 
by (simp add: additive_subgroup.a_subgroup A ideal.axioms(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

360 
moreover have "((+>) I) \<in> ring_hom R (R Quot I)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

361 
by (simp add: assms(1) ideal.rcos_ring_hom) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

362 
ultimately show "subgroup ((+>) I ` J) (add_monoid (R Quot I))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

363 
using assms(1) ideal.rcos_ring_hom_ring ring_hom_ring.img_is_add_subgroup by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

364 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

365 
fix a x assume "a \<in> (+>) I ` J" "x \<in> carrier (R Quot I)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

366 
then obtain i j where i: "i \<in> carrier R" "x = I +> i" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

367 
and j: "j \<in> J" "a = I +> j" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

368 
unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

369 
hence "a \<otimes>\<^bsub>R Quot I\<^esub> x = [mod I:] (I +> j) \<Otimes> (I +> i)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

370 
unfolding FactRing_def by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

371 
hence "a \<otimes>\<^bsub>R Quot I\<^esub> x = I +> (j \<otimes> i)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

372 
using ideal.rcoset_mult_add[OF assms(1), of j i] i(1) j(1) A ideal.Icarr by force 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

373 
thus "a \<otimes>\<^bsub>R Quot I\<^esub> x \<in> (+>) I ` J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

374 
using A i(1) j(1) by (simp add: ideal.I_r_closed) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

375 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

376 
have "x \<otimes>\<^bsub>R Quot I\<^esub> a = [mod I:] (I +> i) \<Otimes> (I +> j)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

377 
unfolding FactRing_def i j by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

378 
hence "x \<otimes>\<^bsub>R Quot I\<^esub> a = I +> (i \<otimes> j)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

379 
using ideal.rcoset_mult_add[OF assms(1), of i j] i(1) j(1) A ideal.Icarr by force 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

380 
thus "x \<otimes>\<^bsub>R Quot I\<^esub> a \<in> (+>) I ` J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

381 
using A i(1) j(1) by (simp add: ideal.I_l_closed) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

382 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

383 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

384 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

385 
lemma (in ring_hom_ring) ideal_vimage: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

386 
assumes "ideal I S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

387 
shows "ideal { r \<in> carrier R. h r \<in> I } R" (* or (carrier R) \<inter> (h ` I) *) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

388 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

389 
show "{ r \<in> carrier R. h r \<in> I } \<subseteq> carrier (add_monoid R)" by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

390 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

391 
show "\<one>\<^bsub>add_monoid R\<^esub> \<in> { r \<in> carrier R. h r \<in> I }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

392 
by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

393 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

394 
fix a b 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

395 
assume "a \<in> { r \<in> carrier R. h r \<in> I }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

396 
and "b \<in> { r \<in> carrier R. h r \<in> I }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

397 
hence a: "a \<in> carrier R" "h a \<in> I" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

398 
and b: "b \<in> carrier R" "h b \<in> I" by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

399 
hence "h (a \<oplus> b) = (h a) \<oplus>\<^bsub>S\<^esub> (h b)" using hom_add by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

400 
moreover have "(h a) \<oplus>\<^bsub>S\<^esub> (h b) \<in> I" using a b assms 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

401 
by (simp add: additive_subgroup.a_closed ideal.axioms(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

402 
ultimately show "a \<otimes>\<^bsub>add_monoid R\<^esub> b \<in> { r \<in> carrier R. h r \<in> I }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

403 
using a(1) b (1) by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

404 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

405 
have "h (\<ominus> a) = \<ominus>\<^bsub>S\<^esub> (h a)" by (simp add: a) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

406 
moreover have "\<ominus>\<^bsub>S\<^esub> (h a) \<in> I" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

407 
by (simp add: a(2) additive_subgroup.a_inv_closed assms ideal.axioms(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

408 
ultimately show "inv\<^bsub>add_monoid R\<^esub> a \<in> { r \<in> carrier R. h r \<in> I }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

409 
using a by (simp add: a_inv_def) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

410 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

411 
fix a r 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

412 
assume "a \<in> { r \<in> carrier R. h r \<in> I }" and r: "r \<in> carrier R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

413 
hence a: "a \<in> carrier R" "h a \<in> I" by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

414 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

415 
have "h a \<otimes>\<^bsub>S\<^esub> h r \<in> I" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

416 
using assms a r by (simp add: ideal.I_r_closed) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

417 
thus "a \<otimes> r \<in> { r \<in> carrier R. h r \<in> I }" by (simp add: a(1) r) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

418 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

419 
have "h r \<otimes>\<^bsub>S\<^esub> h a \<in> I" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

420 
using assms a r by (simp add: ideal.I_l_closed) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

421 
thus "r \<otimes> a \<in> { r \<in> carrier R. h r \<in> I }" by (simp add: a(1) r) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

422 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

423 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

424 
lemma (in ring) canonical_proj_vimage_in_carrier: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

425 
assumes "ideal I R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

426 
shows "J \<subseteq> carrier (R Quot I) \<Longrightarrow> \<Union> J \<subseteq> carrier R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

427 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

428 
assume A: "J \<subseteq> carrier (R Quot I)" show "\<Union> J \<subseteq> carrier R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

429 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

430 
fix j assume j: "j \<in> \<Union> J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

431 
then obtain j' where j': "j' \<in> J" "j \<in> j'" by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

432 
then obtain r where r: "r \<in> carrier R" "j' = I +> r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

433 
using A j' unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

434 
thus "j \<in> carrier R" using j' assms 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

435 
by (meson a_r_coset_subset_G additive_subgroup.a_subset contra_subsetD ideal.axioms(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

436 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

437 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

438 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

439 
lemma (in ring) canonical_proj_vimage_mem_iff: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

440 
assumes "ideal I R" "J \<subseteq> carrier (R Quot I)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

441 
shows "\<And>a. a \<in> carrier R \<Longrightarrow> (a \<in> (\<Union> J)) = (I +> a \<in> J)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

442 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

443 
fix a assume a: "a \<in> carrier R" show "(a \<in> (\<Union> J)) = (I +> a \<in> J)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

444 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

445 
assume "a \<in> \<Union> J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

446 
then obtain j where j: "j \<in> J" "a \<in> j" by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

447 
then obtain r where r: "r \<in> carrier R" "j = I +> r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

448 
using assms j unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

449 
hence "I +> r = I +> a" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

450 
using add.repr_independence[of a I r] j r 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

451 
by (metis a_r_coset_def additive_subgroup.a_subgroup assms(1) ideal.axioms(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

452 
thus "I +> a \<in> J" using r j by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

453 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

454 
assume "I +> a \<in> J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

455 
hence "\<zero> \<oplus> a \<in> I +> a" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

456 
using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

457 
a_r_coset_def'[of R I a] by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

458 
thus "a \<in> \<Union> J" using a \<open>I +> a \<in> J\<close> by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

459 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

460 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

461 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

462 
corollary (in ring) quot_ideal_imp_ring_ideal: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

463 
assumes "ideal I R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

464 
shows "ideal J (R Quot I) \<Longrightarrow> ideal (\<Union> J) R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

465 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

466 
assume A: "ideal J (R Quot I)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

467 
have "\<Union> J = { r \<in> carrier R. I +> r \<in> J }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

468 
using canonical_proj_vimage_in_carrier[OF assms, of J] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

469 
canonical_proj_vimage_mem_iff[OF assms, of J] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

470 
additive_subgroup.a_subset[OF ideal.axioms(1)[OF A]] by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

471 
thus "ideal (\<Union> J) R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

472 
using ring_hom_ring.ideal_vimage[OF ideal.rcos_ring_hom_ring[OF assms] A] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

473 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

474 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

475 
lemma (in ring) ideal_incl_iff: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

476 
assumes "ideal I R" "ideal J R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

477 
shows "(I \<subseteq> J) = (J = (\<Union> j \<in> J. I +> j))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

478 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

479 
assume A: "J = (\<Union> j \<in> J. I +> j)" hence "I +> \<zero> \<subseteq> J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

480 
using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(2)]] by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

481 
thus "I \<subseteq> J" using additive_subgroup.a_subset[OF ideal.axioms(1)[OF assms(1)]] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

482 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

483 
assume A: "I \<subseteq> J" show "J = (\<Union>j\<in>J. I +> j)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

484 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

485 
show "J \<subseteq> (\<Union> j \<in> J. I +> j)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

486 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

487 
fix j assume j: "j \<in> J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

488 
have "\<zero> \<in> I" by (simp add: additive_subgroup.zero_closed assms(1) ideal.axioms(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

489 
hence "\<zero> \<oplus> j \<in> I +> j" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

490 
using a_r_coset_def'[of R I j] by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

491 
thus "j \<in> (\<Union>j\<in>J. I +> j)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

492 
using assms(2) j additive_subgroup.a_Hcarr ideal.axioms(1) by fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

493 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

494 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

495 
show "(\<Union> j \<in> J. I +> j) \<subseteq> J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

496 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

497 
fix x assume "x \<in> (\<Union> j \<in> J. I +> j)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

498 
then obtain j where j: "j \<in> J" "x \<in> I +> j" by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

499 
then obtain i where i: "i \<in> I" "x = i \<oplus> j" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

500 
using a_r_coset_def'[of R I j] by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

501 
thus "x \<in> J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

502 
using assms(2) j A additive_subgroup.a_closed[OF ideal.axioms(1)[OF assms(2)]] by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

503 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

504 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

505 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

506 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

507 
theorem (in ring) quot_ideal_correspondence: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

508 
assumes "ideal I R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

509 
shows "bij_betw (\<lambda>J. (+>) I ` J) { J. ideal J R \<and> I \<subseteq> J } { J . ideal J (R Quot I) }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

510 
proof (rule bij_betw_byWitness[where ?f' = "\<lambda>X. \<Union> X"]) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

511 
show "\<forall>J \<in> { J. ideal J R \<and> I \<subseteq> J }. (\<lambda>X. \<Union> X) ((+>) I ` J) = J" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

512 
using assms ideal_incl_iff by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

513 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

514 
show "(\<lambda>J. (+>) I ` J) ` { J. ideal J R \<and> I \<subseteq> J } \<subseteq> { J. ideal J (R Quot I) }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

515 
using assms ring_ideal_imp_quot_ideal by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

516 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

517 
show "(\<lambda>X. \<Union> X) ` { J. ideal J (R Quot I) } \<subseteq> { J. ideal J R \<and> I \<subseteq> J }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

518 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

519 
fix J assume "J \<in> ((\<lambda>X. \<Union> X) ` { J. ideal J (R Quot I) })" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

520 
then obtain J' where J': "ideal J' (R Quot I)" "J = \<Union> J'" by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

521 
hence "ideal J R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

522 
using assms quot_ideal_imp_ring_ideal by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

523 
moreover have "I \<in> J'" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

524 
using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF J'(1)]] unfolding FactRing_def by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

525 
ultimately show "J \<in> { J. ideal J R \<and> I \<subseteq> J }" using J'(2) by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

526 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

527 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

528 
show "\<forall>J' \<in> { J. ideal J (R Quot I) }. ((+>) I ` (\<Union> J')) = J'" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

529 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

530 
fix J' assume "J' \<in> { J. ideal J (R Quot I) }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

531 
hence subset: "J' \<subseteq> carrier (R Quot I) \<and> ideal J' (R Quot I)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

532 
using additive_subgroup.a_subset ideal_def by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

533 
hence "((+>) I ` (\<Union> J')) \<subseteq> J'" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

534 
using canonical_proj_vimage_in_carrier canonical_proj_vimage_mem_iff 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

535 
by (meson assms contra_subsetD image_subsetI) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

536 
moreover have "J' \<subseteq> ((+>) I ` (\<Union> J'))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

537 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

538 
fix x assume "x \<in> J'" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

539 
then obtain r where r: "r \<in> carrier R" "x = I +> r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

540 
using subset unfolding FactRing_def A_RCOSETS_def'[of R I] by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

541 
hence "r \<in> (\<Union> J')" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

542 
using \<open>x \<in> J'\<close> assms canonical_proj_vimage_mem_iff subset by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

543 
thus "x \<in> ((+>) I ` (\<Union> J'))" using r(2) by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

544 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

545 
ultimately show "((+>) I ` (\<Union> J')) = J'" by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

546 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

547 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

548 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

549 
lemma (in cring) quot_domain_imp_primeideal: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

550 
assumes "ideal P R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

551 
shows "domain (R Quot P) \<Longrightarrow> primeideal P R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

552 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

553 
assume A: "domain (R Quot P)" show "primeideal P R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

554 
proof (rule primeidealI) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

555 
show "ideal P R" using assms . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

556 
show "cring R" using is_cring . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

557 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

558 
show "carrier R \<noteq> P" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

559 
proof (rule ccontr) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

560 
assume "\<not> carrier R \<noteq> P" hence "carrier R = P" by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

561 
hence "\<And>I. I \<in> carrier (R Quot P) \<Longrightarrow> I = P" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

562 
unfolding FactRing_def A_RCOSETS_def' apply simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

563 
using a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1) by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

564 
hence "\<one>\<^bsub>(R Quot P)\<^esub> = \<zero>\<^bsub>(R Quot P)\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

565 
by (metis assms ideal.quotient_is_ring ring.ring_simprules(2) ring.ring_simprules(6)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

566 
thus False using domain.one_not_zero[OF A] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

567 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

568 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

569 
fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and ab: "a \<otimes> b \<in> P" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

570 
hence "P +> (a \<otimes> b) = \<zero>\<^bsub>(R Quot P)\<^esub>" unfolding FactRing_def 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

571 
by (simp add: a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

572 
moreover have "(P +> a) \<otimes>\<^bsub>(R Quot P)\<^esub> (P +> b) = P +> (a \<otimes> b)" unfolding FactRing_def 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

573 
using a b by (simp add: assms ideal.rcoset_mult_add) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

574 
moreover have "P +> a \<in> carrier (R Quot P) \<and> P +> b \<in> carrier (R Quot P)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

575 
by (simp add: a b FactRing_def a_rcosetsI additive_subgroup.a_subset assms ideal.axioms(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

576 
ultimately have "P +> a = \<zero>\<^bsub>(R Quot P)\<^esub> \<or> P +> b = \<zero>\<^bsub>(R Quot P)\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

577 
using domain.integral[OF A, of "P +> a" "P +> b"] by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

578 
thus "a \<in> P \<or> b \<in> P" unfolding FactRing_def apply simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

579 
using a b assms a_coset_join1 additive_subgroup.a_subgroup ideal.axioms(1) by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

580 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

581 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

582 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

583 
lemma (in cring) quot_domain_iff_primeideal: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

584 
assumes "ideal P R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

585 
shows "domain (R Quot P) = primeideal P R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

586 
using quot_domain_imp_primeideal[OF assms] primeideal.quotient_is_domain[of P R] by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

587 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

588 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

589 
subsection \<open>Isomorphism\<close> 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

590 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

591 
definition 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

592 
ring_iso :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<Rightarrow> 'b) set" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

593 
where "ring_iso R S = { h. h \<in> ring_hom R S \<and> bij_betw h (carrier R) (carrier S) }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

594 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

595 
definition 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

596 
is_ring_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<simeq>" 60) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

597 
where "R \<simeq> S = (ring_iso R S \<noteq> {})" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

598 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

599 
definition 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

600 
morphic_prop :: "_ \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

601 
where "morphic_prop R P = 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

602 
((P \<one>\<^bsub>R\<^esub>) \<and> 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

603 
(\<forall>r \<in> carrier R. P r) \<and> 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

604 
(\<forall>r1 \<in> carrier R. \<forall>r2 \<in> carrier R. P (r1 \<otimes>\<^bsub>R\<^esub> r2)) \<and> 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

605 
(\<forall>r1 \<in> carrier R. \<forall>r2 \<in> carrier R. P (r1 \<oplus>\<^bsub>R\<^esub> r2)))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

606 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

607 
lemma ring_iso_memI: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

608 
fixes R (structure) and S (structure) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

609 
assumes "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

610 
and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

611 
and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

612 
and "h \<one> = \<one>\<^bsub>S\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

613 
and "bij_betw h (carrier R) (carrier S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

614 
shows "h \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

615 
by (auto simp add: ring_hom_memI assms ring_iso_def) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

616 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

617 
lemma ring_iso_memE: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

618 
fixes R (structure) and S (structure) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

619 
assumes "h \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

620 
shows "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

621 
and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

622 
and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

623 
and "h \<one> = \<one>\<^bsub>S\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

624 
and "bij_betw h (carrier R) (carrier S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

625 
using assms unfolding ring_iso_def ring_hom_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

626 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

627 
lemma morphic_propI: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

628 
fixes R (structure) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

629 
assumes "P \<one>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

630 
and "\<And>r. r \<in> carrier R \<Longrightarrow> P r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

631 
and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<otimes> r2)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

632 
and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<oplus> r2)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

633 
shows "morphic_prop R P" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

634 
unfolding morphic_prop_def using assms by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

635 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

636 
lemma morphic_propE: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

637 
fixes R (structure) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

638 
assumes "morphic_prop R P" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

639 
shows "P \<one>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

640 
and "\<And>r. r \<in> carrier R \<Longrightarrow> P r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

641 
and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<otimes> r2)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

642 
and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<oplus> r2)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

643 
using assms unfolding morphic_prop_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

644 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

645 
lemma ring_iso_restrict: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

646 
assumes "f \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

647 
and "\<And>r. r \<in> carrier R \<Longrightarrow> f r = g r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

648 
and "ring R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

649 
shows "g \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

650 
proof (rule ring_iso_memI) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

651 
show "bij_betw g (carrier R) (carrier S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

652 
using assms(12) bij_betw_cong ring_iso_memE(5) by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

653 
show "g \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

654 
using assms ring.ring_simprules(6) ring_iso_memE(4) by force 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

655 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

656 
fix x y assume x: "x \<in> carrier R" and y: "y \<in> carrier R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

657 
show "g x \<in> carrier S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

658 
using assms(12) ring_iso_memE(1) x by fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

659 
show "g (x \<otimes>\<^bsub>R\<^esub> y) = g x \<otimes>\<^bsub>S\<^esub> g y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

660 
by (metis assms ring.ring_simprules(5) ring_iso_memE(2) x y) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

661 
show "g (x \<oplus>\<^bsub>R\<^esub> y) = g x \<oplus>\<^bsub>S\<^esub> g y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

662 
by (metis assms ring.ring_simprules(1) ring_iso_memE(3) x y) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

663 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

664 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

665 
lemma ring_iso_morphic_prop: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

666 
assumes "f \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

667 
and "morphic_prop R P" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

668 
and "\<And>r. P r \<Longrightarrow> f r = g r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

669 
shows "g \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

670 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

671 
have eq0: "\<And>r. r \<in> carrier R \<Longrightarrow> f r = g r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

672 
and eq1: "f \<one>\<^bsub>R\<^esub> = g \<one>\<^bsub>R\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

673 
and eq2: "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> f (r1 \<otimes>\<^bsub>R\<^esub> r2) = g (r1 \<otimes>\<^bsub>R\<^esub> r2)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

674 
and eq3: "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> f (r1 \<oplus>\<^bsub>R\<^esub> r2) = g (r1 \<oplus>\<^bsub>R\<^esub> r2)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

675 
using assms(23) unfolding morphic_prop_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

676 
show ?thesis 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

677 
apply (rule ring_iso_memI) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

678 
using assms(1) eq0 ring_iso_memE(1) apply fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

679 
apply (metis assms(1) eq0 eq2 ring_iso_memE(2)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

680 
apply (metis assms(1) eq0 eq3 ring_iso_memE(3)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

681 
using assms(1) eq1 ring_iso_memE(4) apply fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

682 
using assms(1) bij_betw_cong eq0 ring_iso_memE(5) by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

683 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

684 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

685 
lemma (in ring) ring_hom_imp_img_ring: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

686 
assumes "h \<in> ring_hom R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

687 
shows "ring (S \<lparr> carrier := h ` (carrier R), one := h \<one>, zero := h \<zero> \<rparr>)" (is "ring ?h_img") 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

688 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

689 
have "h \<in> hom (add_monoid R) (add_monoid S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

690 
using assms unfolding hom_def ring_hom_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

691 
hence "comm_group ((add_monoid S) \<lparr> carrier := h ` (carrier R), one := h \<zero> \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

692 
using add.hom_imp_img_comm_group[of h "add_monoid S"] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

693 
hence comm_group: "comm_group (add_monoid ?h_img)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

694 
by (auto intro: comm_monoidI simp add: monoid.defs) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

695 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

696 
moreover have "h \<in> hom R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

697 
using assms unfolding ring_hom_def hom_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

698 
hence "monoid (S \<lparr> carrier := h ` (carrier R), one := h \<one> \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

699 
using hom_imp_img_monoid[of h S] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

700 
hence monoid: "monoid ?h_img" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

701 
unfolding monoid_def by (simp add: monoid.defs) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

702 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

703 
show ?thesis 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

704 
proof (rule ringI, simp_all add: comm_group_abelian_groupI[OF comm_group] monoid) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

705 
fix x y z assume "x \<in> h ` carrier R" "y \<in> h ` carrier R" "z \<in> h ` carrier R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

706 
then obtain r1 r2 r3 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

707 
where r1: "r1 \<in> carrier R" "x = h r1" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

708 
and r2: "r2 \<in> carrier R" "y = h r2" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

709 
and r3: "r3 \<in> carrier R" "z = h r3" by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

710 
hence "(x \<oplus>\<^bsub>S\<^esub> y) \<otimes>\<^bsub>S\<^esub> z = h ((r1 \<oplus> r2) \<otimes> r3)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

711 
using ring_hom_memE[OF assms] by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

712 
also have " ... = h ((r1 \<otimes> r3) \<oplus> (r2 \<otimes> r3))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

713 
using l_distr[OF r1(1) r2(1) r3(1)] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

714 
also have " ... = (x \<otimes>\<^bsub>S\<^esub> z) \<oplus>\<^bsub>S\<^esub> (y \<otimes>\<^bsub>S\<^esub> z)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

715 
using ring_hom_memE[OF assms] r1 r2 r3 by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

716 
finally show "(x \<oplus>\<^bsub>S\<^esub> y) \<otimes>\<^bsub>S\<^esub> z = (x \<otimes>\<^bsub>S\<^esub> z) \<oplus>\<^bsub>S\<^esub> (y \<otimes>\<^bsub>S\<^esub> z)" . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

717 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

718 
have "z \<otimes>\<^bsub>S\<^esub> (x \<oplus>\<^bsub>S\<^esub> y) = h (r3 \<otimes> (r1 \<oplus> r2))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

719 
using ring_hom_memE[OF assms] r1 r2 r3 by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

720 
also have " ... = h ((r3 \<otimes> r1) \<oplus> (r3 \<otimes> r2))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

721 
using r_distr[OF r1(1) r2(1) r3(1)] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

722 
also have " ... = (z \<otimes>\<^bsub>S\<^esub> x) \<oplus>\<^bsub>S\<^esub> (z \<otimes>\<^bsub>S\<^esub> y)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

723 
using ring_hom_memE[OF assms] r1 r2 r3 by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

724 
finally show "z \<otimes>\<^bsub>S\<^esub> (x \<oplus>\<^bsub>S\<^esub> y) = (z \<otimes>\<^bsub>S\<^esub> x) \<oplus>\<^bsub>S\<^esub> (z \<otimes>\<^bsub>S\<^esub> y)" . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

725 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

726 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

727 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

728 
lemma (in ring) ring_iso_imp_img_ring: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

729 
assumes "h \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

730 
shows "ring (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

731 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

732 
have "ring (S \<lparr> carrier := h ` (carrier R), one := h \<one>, zero := h \<zero> \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

733 
using ring_hom_imp_img_ring[of h S] assms unfolding ring_iso_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

734 
moreover have "h ` (carrier R) = carrier S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

735 
using assms unfolding ring_iso_def bij_betw_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

736 
ultimately show ?thesis by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

737 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

738 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

739 
lemma (in cring) ring_iso_imp_img_cring: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

740 
assumes "h \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

741 
shows "cring (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" (is "cring ?h_img") 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

742 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

743 
note m_comm 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

744 
interpret h_img?: ring ?h_img 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

745 
using ring_iso_imp_img_ring[OF assms] . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

746 
show ?thesis 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

747 
proof (unfold_locales) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

748 
fix x y assume "x \<in> carrier ?h_img" "y \<in> carrier ?h_img" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

749 
then obtain r1 r2 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

750 
where r1: "r1 \<in> carrier R" "x = h r1" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

751 
and r2: "r2 \<in> carrier R" "y = h r2" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

752 
using assms image_iff[where ?f = h and ?A = "carrier R"] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

753 
unfolding ring_iso_def bij_betw_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

754 
have "x \<otimes>\<^bsub>(?h_img)\<^esub> y = h (r1 \<otimes> r2)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

755 
using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

756 
also have " ... = h (r2 \<otimes> r1)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

757 
using m_comm[OF r1(1) r2(1)] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

758 
also have " ... = y \<otimes>\<^bsub>(?h_img)\<^esub> x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

759 
using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

760 
finally show "x \<otimes>\<^bsub>(?h_img)\<^esub> y = y \<otimes>\<^bsub>(?h_img)\<^esub> x" . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

761 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

762 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

763 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

764 
lemma (in domain) ring_iso_imp_img_domain: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

765 
assumes "h \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

766 
shows "domain (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" (is "domain ?h_img") 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

767 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

768 
note aux = m_closed integral one_not_zero one_closed zero_closed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

769 
interpret h_img?: cring ?h_img 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

770 
using ring_iso_imp_img_cring[OF assms] . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

771 
show ?thesis 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

772 
proof (unfold_locales) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

773 
show "\<one>\<^bsub>?h_img\<^esub> \<noteq> \<zero>\<^bsub>?h_img\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

774 
using ring_iso_memE(5)[OF assms] aux(34) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

775 
unfolding bij_betw_def inj_on_def by force 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

776 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

777 
fix a b 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

778 
assume A: "a \<otimes>\<^bsub>?h_img\<^esub> b = \<zero>\<^bsub>?h_img\<^esub>" "a \<in> carrier ?h_img" "b \<in> carrier ?h_img" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

779 
then obtain r1 r2 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

780 
where r1: "r1 \<in> carrier R" "a = h r1" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

781 
and r2: "r2 \<in> carrier R" "b = h r2" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

782 
using assms image_iff[where ?f = h and ?A = "carrier R"] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

783 
unfolding ring_iso_def bij_betw_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

784 
hence "a \<otimes>\<^bsub>?h_img\<^esub> b = h (r1 \<otimes> r2)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

785 
using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

786 
hence "h (r1 \<otimes> r2) = h \<zero>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

787 
using A(1) by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

788 
hence "r1 \<otimes> r2 = \<zero>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

789 
using ring_iso_memE(5)[OF assms] aux(1)[OF r1(1) r2(1)] aux(5) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

790 
unfolding bij_betw_def inj_on_def by force 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

791 
hence "r1 = \<zero> \<or> r2 = \<zero>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

792 
using aux(2)[OF _ r1(1) r2(1)] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

793 
thus "a = \<zero>\<^bsub>?h_img\<^esub> \<or> b = \<zero>\<^bsub>?h_img\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

794 
unfolding r1 r2 by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

795 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

796 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

797 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

798 
lemma (in field) ring_iso_imp_img_field: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

799 
assumes "h \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

800 
shows "field (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" (is "field ?h_img") 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

801 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

802 
interpret h_img?: domain ?h_img 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

803 
using ring_iso_imp_img_domain[OF assms] . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

804 
show ?thesis 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

805 
proof (unfold_locales, auto simp add: Units_def) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

806 
interpret field R using field_axioms . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

807 
fix a assume a: "a \<in> carrier S" "a \<otimes>\<^bsub>S\<^esub> h \<zero> = h \<one>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

808 
then obtain r where r: "r \<in> carrier R" "a = h r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

809 
using assms image_iff[where ?f = h and ?A = "carrier R"] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

810 
unfolding ring_iso_def bij_betw_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

811 
have "a \<otimes>\<^bsub>S\<^esub> h \<zero> = h (r \<otimes> \<zero>)" unfolding r(2) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

812 
using ring_iso_memE(2)[OF assms r(1)] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

813 
hence "h \<one> = h \<zero>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

814 
using r(1) a(2) by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

815 
thus False 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

816 
using ring_iso_memE(5)[OF assms] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

817 
unfolding bij_betw_def inj_on_def by force 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

818 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

819 
interpret field R using field_axioms . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

820 
fix s assume s: "s \<in> carrier S" "s \<noteq> h \<zero>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

821 
then obtain r where r: "r \<in> carrier R" "s = h r" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

822 
using assms image_iff[where ?f = h and ?A = "carrier R"] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

823 
unfolding ring_iso_def bij_betw_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

824 
hence "r \<noteq> \<zero>" using s(2) by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

825 
hence inv_r: "inv r \<in> carrier R" "inv r \<noteq> \<zero>" "r \<otimes> inv r = \<one>" "inv r \<otimes> r = \<one>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

826 
using field_Units r(1) by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

827 
have "h (inv r) \<otimes>\<^bsub>S\<^esub> h r = h \<one>" and "h r \<otimes>\<^bsub>S\<^esub> h (inv r) = h \<one>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

828 
using ring_iso_memE(2)[OF assms inv_r(1) r(1)] inv_r(34) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

829 
ring_iso_memE(2)[OF assms r(1) inv_r(1)] by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

830 
thus "\<exists>s' \<in> carrier S. s' \<otimes>\<^bsub>S\<^esub> s = h \<one> \<and> s \<otimes>\<^bsub>S\<^esub> s' = h \<one>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

831 
using ring_iso_memE(1)[OF assms inv_r(1)] r(2) by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

832 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

833 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

834 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

835 
lemma ring_iso_same_card: "R \<simeq> S \<Longrightarrow> card (carrier R) = card (carrier S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

836 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

837 
assume "R \<simeq> S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

838 
then obtain h where "bij_betw h (carrier R) (carrier S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

839 
unfolding is_ring_iso_def ring_iso_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

840 
thus "card (carrier R) = card (carrier S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

841 
using bij_betw_same_card[of h "carrier R" "carrier S"] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

842 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

843 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

844 
lemma ring_iso_set_refl: "id \<in> ring_iso R R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

845 
by (rule ring_iso_memI) (auto) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

846 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

847 
corollary ring_iso_refl: "R \<simeq> R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

848 
using is_ring_iso_def ring_iso_set_refl by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

849 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

850 
lemma ring_iso_set_trans: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

851 
"\<lbrakk> f \<in> ring_iso R S; g \<in> ring_iso S Q \<rbrakk> \<Longrightarrow> (g \<circ> f) \<in> ring_iso R Q" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

852 
unfolding ring_iso_def using bij_betw_trans ring_hom_trans by fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

853 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

854 
corollary ring_iso_trans: "\<lbrakk> R \<simeq> S; S \<simeq> Q \<rbrakk> \<Longrightarrow> R \<simeq> Q" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

855 
using ring_iso_set_trans unfolding is_ring_iso_def by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

856 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

857 
lemma ring_iso_set_sym: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

858 
assumes "ring R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

859 
shows "h \<in> ring_iso R S \<Longrightarrow> (inv_into (carrier R) h) \<in> ring_iso S R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

860 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

861 
assume h: "h \<in> ring_iso R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

862 
hence h_hom: "h \<in> ring_hom R S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

863 
and h_surj: "h ` (carrier R) = (carrier S)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

864 
and h_inj: "\<And> x1 x2. \<lbrakk> x1 \<in> carrier R; x2 \<in> carrier R \<rbrakk> \<Longrightarrow> h x1 = h x2 \<Longrightarrow> x1 = x2" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

865 
unfolding ring_iso_def bij_betw_def inj_on_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

866 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

867 
have h_inv_bij: "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

868 
using bij_betw_inv_into h ring_iso_def by fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

869 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

870 
show "inv_into (carrier R) h \<in> ring_iso S R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

871 
apply (rule ring_iso_memI) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

872 
apply (simp add: h_surj inv_into_into) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

873 
apply (auto simp add: h_inv_bij) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

874 
apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

875 
ring.ring_simprules(5) ring_hom_closed ring_hom_mult) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

876 
apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

877 
ring.ring_simprules(1) ring_hom_add ring_hom_closed) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

878 
by (metis (no_types, hide_lams) assms f_inv_into_f h_hom h_inj 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

879 
imageI inv_into_into ring.ring_simprules(6) ring_hom_one) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

880 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

881 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

882 
corollary ring_iso_sym: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

883 
assumes "ring R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

884 
shows "R \<simeq> S \<Longrightarrow> S \<simeq> R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

885 
using assms ring_iso_set_sym unfolding is_ring_iso_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

886 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

887 
lemma (in ring_hom_ring) the_elem_simp [simp]: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

888 
"\<And>x. x \<in> carrier R \<Longrightarrow> the_elem (h ` ((a_kernel R S h) +> x)) = h x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

889 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

890 
fix x assume x: "x \<in> carrier R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

891 
hence "h x \<in> h ` ((a_kernel R S h) +> x)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

892 
using homeq_imp_rcos by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

893 
thus "the_elem (h ` ((a_kernel R S h) +> x)) = h x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

894 
by (metis (no_types, lifting) x empty_iff homeq_imp_rcos rcos_imp_homeq the_elem_image_unique) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

895 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

896 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

897 
lemma (in ring_hom_ring) the_elem_inj: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

898 
"\<And>X Y. \<lbrakk> X \<in> carrier (R Quot (a_kernel R S h)); Y \<in> carrier (R Quot (a_kernel R S h)) \<rbrakk> \<Longrightarrow> 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

899 
the_elem (h ` X) = the_elem (h ` Y) \<Longrightarrow> X = Y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

900 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

901 
fix X Y 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

902 
assume "X \<in> carrier (R Quot (a_kernel R S h))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

903 
and "Y \<in> carrier (R Quot (a_kernel R S h))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

904 
and Eq: "the_elem (h ` X) = the_elem (h ` Y)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

905 
then obtain x y where x: "x \<in> carrier R" "X = (a_kernel R S h) +> x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

906 
and y: "y \<in> carrier R" "Y = (a_kernel R S h) +> y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

907 
unfolding FactRing_def A_RCOSETS_def' by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

908 
hence "h x = h y" using Eq by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

909 
hence "x \<ominus> y \<in> (a_kernel R S h)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

910 
by (simp add: a_minus_def abelian_subgroup.a_rcos_module_imp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

911 
abelian_subgroup_a_kernel homeq_imp_rcos x(1) y(1)) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

912 
thus "X = Y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

913 
by (metis R.a_coset_add_inv1 R.minus_eq abelian_subgroup.a_rcos_const 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

914 
abelian_subgroup_a_kernel additive_subgroup.a_subset additive_subgroup_a_kernel x y) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

915 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

916 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

917 
lemma (in ring_hom_ring) quot_mem: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

918 
"\<And>X. X \<in> carrier (R Quot (a_kernel R S h)) \<Longrightarrow> \<exists>x \<in> carrier R. X = (a_kernel R S h) +> x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

919 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

920 
fix X assume "X \<in> carrier (R Quot (a_kernel R S h))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

921 
thus "\<exists>x \<in> carrier R. X = (a_kernel R S h) +> x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

922 
unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (simp add: a_r_coset_def) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

923 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

924 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

925 
lemma (in ring_hom_ring) the_elem_wf: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

926 
"\<And>X. X \<in> carrier (R Quot (a_kernel R S h)) \<Longrightarrow> \<exists>y \<in> carrier S. (h ` X) = { y }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

927 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

928 
fix X assume "X \<in> carrier (R Quot (a_kernel R S h))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

929 
then obtain x where x: "x \<in> carrier R" and X: "X = (a_kernel R S h) +> x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

930 
using quot_mem by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

931 
hence "\<And>x'. x' \<in> X \<Longrightarrow> h x' = h x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

932 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

933 
fix x' assume "x' \<in> X" hence "x' \<in> (a_kernel R S h) +> x" using X by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

934 
then obtain k where k: "k \<in> a_kernel R S h" "x' = k \<oplus> x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

935 
by (metis R.add.inv_closed R.add.m_assoc R.l_neg R.r_zero 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

936 
abelian_subgroup.a_elemrcos_carrier 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

937 
abelian_subgroup.a_rcos_module_imp abelian_subgroup_a_kernel x) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

938 
hence "h x' = h k \<oplus>\<^bsub>S\<^esub> h x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

939 
by (meson additive_subgroup.a_Hcarr additive_subgroup_a_kernel hom_add x) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

940 
also have " ... = h x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

941 
using k by (auto simp add: x) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

942 
finally show "h x' = h x" . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

943 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

944 
moreover have "h x \<in> h ` X" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

945 
by (simp add: X homeq_imp_rcos x) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

946 
ultimately have "(h ` X) = { h x }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

947 
by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

948 
thus "\<exists>y \<in> carrier S. (h ` X) = { y }" using x by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

949 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

950 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

951 
corollary (in ring_hom_ring) the_elem_wf': 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

952 
"\<And>X. X \<in> carrier (R Quot (a_kernel R S h)) \<Longrightarrow> \<exists>r \<in> carrier R. (h ` X) = { h r }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

953 
using the_elem_wf by (metis quot_mem the_elem_eq the_elem_simp) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

954 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

955 
lemma (in ring_hom_ring) the_elem_hom: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

956 
"(\<lambda>X. the_elem (h ` X)) \<in> ring_hom (R Quot (a_kernel R S h)) S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

957 
proof (rule ring_hom_memI) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

958 
show "\<And>x. x \<in> carrier (R Quot a_kernel R S h) \<Longrightarrow> the_elem (h ` x) \<in> carrier S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

959 
using the_elem_wf by fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

960 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

961 
show "the_elem (h ` \<one>\<^bsub>R Quot a_kernel R S h\<^esub>) = \<one>\<^bsub>S\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

962 
unfolding FactRing_def using the_elem_simp[of "\<one>\<^bsub>R\<^esub>"] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

963 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

964 
fix X Y 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

965 
assume "X \<in> carrier (R Quot a_kernel R S h)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

966 
and "Y \<in> carrier (R Quot a_kernel R S h)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

967 
then obtain x y where x: "x \<in> carrier R" "X = (a_kernel R S h) +> x" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

968 
and y: "y \<in> carrier R" "Y = (a_kernel R S h) +> y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

969 
using quot_mem by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

970 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

971 
have "X \<otimes>\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \<otimes> y)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

972 
by (simp add: FactRing_def ideal.rcoset_mult_add kernel_is_ideal x y) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

973 
thus "the_elem (h ` (X \<otimes>\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \<otimes>\<^bsub>S\<^esub> the_elem (h ` Y)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

974 
by (simp add: x y) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

975 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

976 
have "X \<oplus>\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \<oplus> y)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

977 
using ideal.rcos_ring_hom kernel_is_ideal ring_hom_add x y by fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

978 
thus "the_elem (h ` (X \<oplus>\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \<oplus>\<^bsub>S\<^esub> the_elem (h ` Y)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

979 
by (simp add: x y) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

980 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

981 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

982 
lemma (in ring_hom_ring) the_elem_surj: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

983 
"(\<lambda>X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h)) = (h ` (carrier R))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

984 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

985 
show "(\<lambda>X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h) \<subseteq> h ` carrier R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

986 
using the_elem_wf' by fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

987 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

988 
show "h ` carrier R \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

989 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

990 
fix y assume "y \<in> h ` carrier R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

991 
then obtain x where x: "x \<in> carrier R" "h x = y" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

992 
by (metis image_iff) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

993 
hence "the_elem (h ` ((a_kernel R S h) +> x)) = y" by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

994 
moreover have "(a_kernel R S h) +> x \<in> carrier (R Quot (a_kernel R S h))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

995 
unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (auto simp add: x a_r_coset_def) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

996 
ultimately show "y \<in> (\<lambda>X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h))" by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

997 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

998 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

999 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1000 
proposition (in ring_hom_ring) FactRing_iso_set_aux: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1001 
"(\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot (a_kernel R S h)) (S \<lparr> carrier := h ` (carrier R) \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1002 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1003 
have "bij_betw (\<lambda>X. the_elem (h ` X)) (carrier (R Quot a_kernel R S h)) (h ` (carrier R))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1004 
unfolding bij_betw_def inj_on_def using the_elem_surj the_elem_inj by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1005 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1006 
moreover 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1007 
have "(\<lambda>X. the_elem (h ` X)): carrier (R Quot (a_kernel R S h)) \<rightarrow> h ` (carrier R)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1008 
using the_elem_wf' by fastforce 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1009 
hence "(\<lambda>X. the_elem (h ` X)) \<in> ring_hom (R Quot (a_kernel R S h)) (S \<lparr> carrier := h ` (carrier R) \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1010 
using the_elem_hom the_elem_wf' unfolding ring_hom_def by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1011 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1012 
ultimately show ?thesis unfolding ring_iso_def using the_elem_hom by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1013 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1014 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1015 
theorem (in ring_hom_ring) FactRing_iso_set: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1016 
assumes "h ` carrier R = carrier S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1017 
shows "(\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot (a_kernel R S h)) S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1018 
using FactRing_iso_set_aux assms by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1019 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1020 
corollary (in ring_hom_ring) FactRing_iso: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1021 
assumes "h ` carrier R = carrier S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1022 
shows "R Quot (a_kernel R S h) \<simeq> S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1023 
using FactRing_iso_set assms is_ring_iso_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1024 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1025 
lemma (in ring_hom_ring) img_is_ring: "ring (S \<lparr> carrier := h ` (carrier R) \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1026 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1027 
let ?the_elem = "\<lambda>X. the_elem (h ` X)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1028 
have FactRing_is_ring: "ring (R Quot (a_kernel R S h))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1029 
by (simp add: ideal.quotient_is_ring kernel_is_ideal) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1030 
have "ring ((S \<lparr> carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \<rparr>) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1031 
\<lparr> one := ?the_elem \<one>\<^bsub>(R Quot (a_kernel R S h))\<^esub>, 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1032 
zero := ?the_elem \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub> \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1033 
using ring.ring_iso_imp_img_ring[OF FactRing_is_ring, of ?the_elem 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1034 
"S \<lparr> carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \<rparr>"] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1035 
FactRing_iso_set_aux the_elem_surj by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1036 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1037 
moreover 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1038 
have "\<zero> \<in> (a_kernel R S h)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1039 
using a_kernel_def'[of R S h] by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1040 
hence "\<one> \<in> (a_kernel R S h) +> \<one>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1041 
using a_r_coset_def'[of R "a_kernel R S h" \<one>] by force 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1042 
hence "\<one>\<^bsub>S\<^esub> \<in> (h ` ((a_kernel R S h) +> \<one>))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1043 
using hom_one by force 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1044 
hence "?the_elem \<one>\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \<one>\<^bsub>S\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1045 
using the_elem_wf[of "(a_kernel R S h) +> \<one>"] by (simp add: FactRing_def) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1046 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1047 
moreover 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1048 
have "\<zero>\<^bsub>S\<^esub> \<in> (h ` (a_kernel R S h))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1049 
using a_kernel_def'[of R S h] hom_zero by force 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1050 
hence "\<zero>\<^bsub>S\<^esub> \<in> (h ` \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1051 
by (simp add: FactRing_def) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1052 
hence "?the_elem \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \<zero>\<^bsub>S\<^esub>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1053 
using the_elem_wf[OF ring.ring_simprules(2)[OF FactRing_is_ring]] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1054 
by (metis singletonD the_elem_eq) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1055 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1056 
ultimately 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1057 
have "ring ((S \<lparr> carrier := h ` (carrier R) \<rparr>) \<lparr> one := \<one>\<^bsub>S\<^esub>, zero := \<zero>\<^bsub>S\<^esub> \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1058 
using the_elem_surj by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1059 
thus ?thesis 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1060 
by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1061 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1062 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1063 
lemma (in ring_hom_ring) img_is_cring: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1064 
assumes "cring S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1065 
shows "cring (S \<lparr> carrier := h ` (carrier R) \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1066 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1067 
interpret ring "S \<lparr> carrier := h ` (carrier R) \<rparr>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1068 
using img_is_ring . 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1069 
show ?thesis 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1070 
apply unfold_locales 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1071 
using assms unfolding cring_def comm_monoid_def comm_monoid_axioms_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1072 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1073 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1074 
lemma (in ring_hom_ring) img_is_domain: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1075 
assumes "domain S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1076 
shows "domain (S \<lparr> carrier := h ` (carrier R) \<rparr>)" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1077 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1078 
interpret cring "S \<lparr> carrier := h ` (carrier R) \<rparr>" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1079 
using img_is_cring assms unfolding domain_def by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1080 
show ?thesis 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1081 
apply unfold_locales 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1082 
using assms unfolding domain_def domain_axioms_def apply auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1083 
using hom_closed by blast 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1084 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1085 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1086 
proposition (in ring_hom_ring) primeideal_vimage: 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1087 
assumes "cring R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1088 
shows "primeideal P S \<Longrightarrow> primeideal { r \<in> carrier R. h r \<in> P } R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1089 
proof  
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1090 
assume A: "primeideal P S" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1091 
hence is_ideal: "ideal P S" unfolding primeideal_def by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1092 
have "ring_hom_ring R (S Quot P) (((+>\<^bsub>S\<^esub>) P) \<circ> h)" (is "ring_hom_ring ?A ?B ?h") 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1093 
using ring_hom_trans[OF homh, of "(+>\<^bsub>S\<^esub>) P" "S Quot P"] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1094 
ideal.rcos_ring_hom_ring[OF is_ideal] assms 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1095 
unfolding ring_hom_ring_def ring_hom_ring_axioms_def cring_def by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1096 
then interpret hom: ring_hom_ring R "S Quot P" "((+>\<^bsub>S\<^esub>) P) \<circ> h" by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1097 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1098 
have "inj_on (\<lambda>X. the_elem (?h ` X)) (carrier (R Quot (a_kernel R (S Quot P) ?h)))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1099 
using hom.the_elem_inj unfolding inj_on_def by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1100 
moreover 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1101 
have "ideal (a_kernel R (S Quot P) ?h) R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1102 
using hom.kernel_is_ideal by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1103 
have hom': "ring_hom_ring (R Quot (a_kernel R (S Quot P) ?h)) (S Quot P) (\<lambda>X. the_elem (?h ` X))" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1104 
using hom.the_elem_hom hom.kernel_is_ideal 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1105 
by (meson hom.ring_hom_ring_axioms ideal.rcos_ring_hom_ring ring_hom_ring_axioms_def ring_hom_ring_def) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1106 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1107 
ultimately 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1108 
have "primeideal (a_kernel R (S Quot P) ?h) R" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1109 
using ring_hom_ring.inj_on_domain[OF hom'] primeideal.quotient_is_domain[OF A] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1110 
cring.quot_domain_imp_primeideal[OF assms hom.kernel_is_ideal] by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1111 

b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1112 
moreover have "a_kernel R (S Quot P) ?h = { r \<in> carrier R. h r \<in> P }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1113 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1114 
show "a_kernel R (S Quot P) ?h \<subseteq> { r \<in> carrier R. h r \<in> P }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1115 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1116 
fix r assume "r \<in> a_kernel R (S Quot P) ?h" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1117 
hence r: "r \<in> carrier R" "P +>\<^bsub>S\<^esub> (h r) = P" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1118 
unfolding a_kernel_def kernel_def FactRing_def by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1119 
hence "h r \<in> P" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1120 
using S.a_rcosI R.l_zero S.l_zero additive_subgroup.a_subset[OF ideal.axioms(1)[OF is_ideal]] 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1121 
additive_subgroup.zero_closed[OF ideal.axioms(1)[OF is_ideal]] hom_closed by metis 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1122 
thus "r \<in> { r \<in> carrier R. h r \<in> P }" using r by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1123 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1124 
next 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1125 
show "{ r \<in> carrier R. h r \<in> P } \<subseteq> a_kernel R (S Quot P) ?h" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1126 
proof 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1127 
fix r assume "r \<in> { r \<in> carrier R. h r \<in> P }" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1128 
hence r: "r \<in> carrier R" "h r \<in> P" by simp_all 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1129 
hence "?h r = P" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1130 
by (simp add: S.a_coset_join2 additive_subgroup.a_subgroup ideal.axioms(1) is_ideal) 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1131 
thus "r \<in> a_kernel R (S Quot P) ?h" 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1132 
unfolding a_kernel_def kernel_def FactRing_def using r(1) by auto 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1133 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1134 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1135 
ultimately show "primeideal { r \<in> carrier R. h r \<in> P } R" by simp 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1136 
qed 
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset

1137 

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

1138 
end 